An Effective Learnt Clause Minimization Approach for CDCL SAT Solvers

An Effective Learnt Clause Minimization Approach for CDCL SAT Solvers

Mao Luo, Chu-Min Li, Fan Xiao, Felip Manyà, Zhipeng Lü

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence
Main track. Pages 703-711. https://doi.org/10.24963/ijcai.2017/98

Learnt clauses in CDCL SAT solvers often contain redundant literals. This may have a negative impact on performance because redundant literals may deteriorate both the effectiveness of Boolean constraint propagation and the quality of subsequent learnt clauses. To overcome this drawback, we define a new inprocessing SAT approach which eliminates redundant literals from learnt clauses by applying Boolean constraint propagation. Learnt clause minimization is activated before the SAT solver triggers some selected restarts, and affects only some learnt clauses during the search process. Moreover, we conducted an empirical evaluation on instances coming from the hard combinatorial and application categories of recent SAT competitions. The results show that a remarkable number of additional instances are solved when the approach is incorporated into five of the best performing CDCL SAT solvers (Glucose, TC_Glucose, COMiniSatPS, MapleCOMSPS and MapleCOMSPS_LRB).
Keywords:
Constraints and Satisfiability: Constraints and Satisfiability
Constraints and Satisfiability: Solvers and Tools
Constraints and Satisfiability: Satisfiability