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.

The solvers on this page can only be used for research and education purpose.

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.

---Reference:

Shaowei Cai, Kaile Su: Local search for Boolean Satisfiability with configuration checking and subscore, Artif. Intell. 204, pp. 75-98 (2013).

---Reference:

Shaowei Cai, Kaile Su: Comprehensive Score: Towards Efficient Local Search for SAT with Long Clauses, Proc. of IJCAI-2013, pp.489-495.

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.