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.


Introduction: 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.
Codes :
  • CCAnr (version 2.0)
  • CCAnr (version 1.0)
  • 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).
    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.


    Introduction: 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.
    Codes : CCASat
    Shaowei Cai, Kaile Su: Local search for Boolean Satisfiability with configuration checking and subscore, Artif. Intell. 204, pp. 75-98 (2013).


    Introduction: 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.
    Codes : CScoreSAT2013
    Shaowei Cai, Kaile Su: Comprehensive Score: Towards Efficient Local Search for SAT with Long Clauses, Proc. of IJCAI-2013, pp.489-495.

    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.
    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.
    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.


    Return to homepage.