Local Search for Satisfiability

Boolean Satisfiability (also referred to as Propositional Satisfiability and abbreviated as SAT) asks whether the variables of a given Boolean formula can be assigned in such a way as to make the formula evaluate to TRUE. Local search is an effective approach to finding models (i.e., satisfying assignments) of satisfiable formulas.

I have developed several solvers for SAT, based on the local search method. I maintain the important ones below, and provide their source codes or executable binaries.
The solvers on this page can only be used for research and education purpose.

CScoreSAT utilizes cscore function which is a linear combination of score and the second level score, and has very good performance for random k-SAT with long clauses near phase transition..
This version uses CScoreSAT for all k-SAT instances with k>3, but calls WalkSAT for 3-SAT. It was ranked 4th in the random SAT category, solving only one instance less than the 3rd solver.
---Reference:
Shaowei Cai, Kaile Su: Comprehensive Score: Towards Efficient Local Search for SAT with Long Clauses, Proc. of IJCAI-2013, pp.489-495.
CCAnr is a CCA based local search solver for non-random SAT instances, and it is a state of the art local search solver for solving structured SAT instances.
CCAnr+CP3 uses a preprocessor CP3 before running CCAnr.
CCAnr+glucose (v2014) combines CCAnr with a complete solver glucose, and is ranked 2nd in "sequential, Hard-combinatorial SAT" track of SAT Competition 2014.
---Reference:
Shaowei Cai, Chuan Luo, Kaile Su: CCAnr: A Configuration Checking Based Local Search Solver for Non-random Satisfiability, Proceedings of SAT 2015
Shaowei Cai, Kaile Su: Configuration Checking with Aspiration in Local Search for SAT, Proc. of AAAI-2012, pp. 434-440.
CCASat adopts the heuristic of Configuration Checking with Aspiration, and utilizes the second level score to break ties for k-SAT with k>3.
CCASat won the random track of SAT Challenge 2012 with large margin.
---Reference:
Shaowei Cai, Kaile Su: Local search for Boolean Satisfiability with configuration checking and subscore, Artif. Intell. 204, pp. 75-98 (2013).

SAT Solvers Improved from WalkSAT

I re-implemented the WalkSAT/SKC algorithm, which is twice as fast as the latest implementation version V50 on WalkSAT homepage for solving random 3-SAT instances, based on experiments with 1 million variables.
This is a non-caching based implementation, and there are two additional techniques: 1) it separates positive and negative literals for each variable; 2) it abandons the calculation of the break value once it exceeds the minimum break value.
---Reference:
Shaowei Cai: Faster Implementation for WalkSAT, Technique Report 2013, http://lcs.ios.ac.cn/~caisw/SAT.html.
Shaowei Cai, Chuan Luo, Kaile Su: Improving WalkSAT By Effective Tie-breaking and Efficient Implementation, Comput. J. 58(11): 2864-2875 (2015), Oxford Press.
WalkSATlm is improved from the famous WalkSAT(SKC) algorithm, by only replacing the random tie-breaking mechanism with a linear make function.
WalkSATlm outperforms WalkSAT by orders of magnitudes on random k-SAT with k>3.
The WalkSATlm2013 adopts WalkSAT to solve random 3-SAT instances, and adopts WalkSATlm to solve instances with k>3.
---Reference:
Shaowei Cai, Kaile Su, Chuan Luo: Improving WalkSAT for Random k-Satisfiability Problem with k>3, Proc. of AAAI-2013, pp. 145-151.
Shaowei Cai, Chuan Luo, Kaile Su: Improving WalkSAT By Effective Tie-breaking and Efficient Implementation, Comput. J. 58(11): 2864-2875 (2015), Oxford Press.

Links


Return to homepage.