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 a few SAT solvers, some of which are jointly developed with Chuan Luo. The codes and information of some selected solvers are provided below.

SAT Solvers based on Configuration Checking

Configuration Checking is a general idea for dealing with the cycling problem of local search, by considering the circumstance information (formally defined as configuration) of the variables. It prevents a variable to change its value if its configuration has not changed since the last time it changed value. This idea has witnessed great success in local search for SAT, and most of my SAT solvers use this idea.

CSCCSat is ranked 3rd in the random SAT track of SAT Competition 2014, and particularly gives the best performance for phase-transition instances.
It is a hybrid solver combining FrwCB (for huge k-SAT instances) and DCCASat (for phase-transition k-SAT instances).
FrwCB is a focused random walk solver that uses clause state based configuration checking and break minimum strategies.
DCCASat utitlizes double configuration chekcing and second level score based functions hscore and hscore2.
---Reference:
Chuan Luo, Shaowei Cai, Kaile Su, Wei Wu: Clause States Based Configuration Checking in Local Search for Satisfiability, IEEE Trans. on Cybernetics 45(5):1014-1027(2015) (for FrwCB).
Chuan Luo, Shaowei Cai, Wei Wu, Kaile Su: Double Configuration Checking in Stochastic Local Search for Satisfiability, Proc. of AAAI-2014: 2703-2709 (for DCCASat)
Shaowei Cai, Chuan Luo, Kaile Su: Scoring Functions Based on Second Level Score for k-SAT with Long Clauses, J. Artif. Intell. Res. 51, pp. 413-441 (2014) (for hscore and hscore2)
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).
  • Swcca Shaowei Cai, Kaile Su: Configuration Checking with Aspiration in Local Search for SAT, Proc. of AAAI-2012, pp. 434-440.

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.