An Effective Learnt Clause Minimization Approach for CDCL SAT Solvers
Authors: Mao Luo, Chu-Min Li, Fan Xiao, Felip Manyà, Zhipeng Lü
IJCAI 2017 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | 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, COMini Sat PS, Maple COMSPS and Maple COMSPS LRB). |
| Researcher Affiliation | Academia | 1School of Computer Science, Huazhong University of Science and Technology, Wuhan, China 2MIS, University of Picardie Jules Verne, Amiens, France 3Artificial Intelligence Research Institute (IIIA-CSIC), Barcelona, Spain |
| Pseudocode | Yes | Algorithm 1: minimization(F, L, nb New Learnts, σ) Algorithm 2: minimize L(F, L) |
| Open Source Code | Yes | 1Available at http://home.mis.u-picardie.fr/ cli/ |
| Open Datasets | Yes | The test instances include the application and hard combinatorial tracks of the 2014 and 2016 SAT competitions, and the community attachment formulas proposed in [Gir aldez Cru and Levy, 2015]. |
| Dataset Splits | No | The paper references predefined benchmark instances from SAT competitions and a generator for community attachment formulas, which are used for testing and evaluation. However, it does not explicitly provide details about training/validation/test dataset splits in terms of percentages or absolute sample counts for a single dataset. |
| Hardware Specification | Yes | The experiments were performed on a computer with Intel Westmere Xeon E7-8837 processors at 2.66 GHz and 10 GB of memory under Linux. |
| Software Dependencies | Yes | We implemented the learnt clause minimization approach described in Section 4 in solvers Glucose 3.0, TC Glucose, COMini Sat PS (COMSPS for short), Maple COMSPS (Maple for short) and Maple COMSPS LRB (Maple LRB for short). |
| Experiment Setup | Yes | We used Glucose 3.0, in which the reduction process is fired once the number of clauses learnt since the last reduction reaches first + 2 inc σ, where first = 2000 and inc = 300 are parameters, and σ is the number of database reductions performed so far. Function live Restart(nb New Learnts, σ) returns true iff nb New Learnts, the number of clauses learnt since the last learnt clause minimization, is greater than or equal to α+2 β σ. We empirically fixed α=1000, β=1000 for the three solvers. The cutoff time is 5000 seconds for each instance and each solver. |