Satisfiability Solving
In this project, we focus on the satisfiability (decision) and related optimization problems of Boolean logical formulas and first order logical formulas with respect to certain background theories.
SAT/MaxSAT solvers have been used in a broad range of applications.
- 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.
SAT is the first NP complete problem and SAT solvers usually serve as a core engine in many industrial applications, particularly in formal verification and resource allocations.
- Maximum Satisfiability (MaxSAT) concerns about finding an assignment to satisfy the most constraints (clauses).
Particularly, people are often interested in solving Partial MaxSAT, where the constraints are divided into hard constraints and soft constraints, and the goal is to satisfy all hard constraints and maximize the number (or the total weight) of satisfied soft constraints. Many real world problems can be modelled as MaxSAT problems naturally.
- Satisfiability Modulo Theories (SMT) concerns about the satisfiability of formulas with respect to some background theory, such as bit-vectors, arrays, arithmetic as well as more complex theories.
[SAT solving] [MaxSAT solving] [SMT solving]
Incomplete SAT Solvers
CCAnr is a state of the art local search solver for solving non-random (structured) SAT instances.
Codes :
CCAnr (version 1.1)
CCAnr (version 1.0)
CCAnr+CP3 (uses a preprocessor CP3 before running CCAnr).
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(v1) This version accelerates the initialization procedure which used to be slow when solving large instances.
- Faster WalkSAT and WalkSATlm
WalkSATlm is improved from the famous WalkSAT(SKC) algorithm, by replacing the random tie-breaking mechanism with a linear make function, and performs particularly well for random k-SAT with k>3. For 3-SAT, it uses WalkSAT/SKC, but with a more efficient implementation.
Codes :
A Fast Implementation of WalkSAT/SKC (v2013.6.17): 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.
WalkSATlm
Complete SAT Solver
ReasonLS: this is the version in SAT Competition 2018 (1st in Non-limit Track)
RelaxedNewTech: this is the version in SAT Competition 2020 (1st in Main Track SAT)
RelaxedNuTech-tidy: this is a simplified version which has similar results to the above version, and was studied in our paper "Deep Cooperation of CDCL and Local Search" [SAT 2021 Best paper].
lstechMaple: this is the version in SAT Competition 2021 (2nd in Main Track SAT)
Kissat_bonus: this is the version in SAT Competition 2021 (2nd in Main Track UNSAT)
Selected Papers
- Shaowei Cai, Xindi Zhang: Deep Cooperation of CDCL and Local Search, Proceedings of SAT 2021 [best paper award] [hybrid solvers]
- Shaowei Cai, Chuan Luo, Kaile Su: CCAnr: A Configuration Checking Based Local Search Solver for Non-random Satisfiability, Proceedings of SAT 2015 [CCAnr]
- Chuan Luo, Shaowei Cai, Wei Wu, Kaile Su: Double Configuration Checking in Stochastic Local Search for Satisfiability, Proceedings of AAAI 2014:2703-2709 [DCCASat]
- Shaowei Cai, Kaile Su: Local search for Boolean Satisfiability with configuration checking and subscore, Artif. Intell. 204, pp. 75-98 (2013). [CCASat]
- Shaowei Cai, Kaile Su: Comprehensive Score: Towards Efficient Local Search for SAT with Long Clauses, Proc. of IJCAI-2013, pp.489-495.
- 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, Fast WalkSAT/SKC]
- Shaowei Cai, Kaile Su, Chuan Luo: Improving WalkSAT for Random k-Satisfiability Problem with k>3, Proc. of AAAI-2013, pp. 145-151. [WalkSATlm]
- Shaowei Cai: Faster Implementation for WalkSAT, Technique Report 2013, http://lcs.ios.ac.cn/~caisw/SAT.html.
Awards
- Second Place Award in Main track SAT, Second Place Award in Main track UNSAT, SAT Competition 2021.
- First Place Award in Main track SAT, Second Place Award in Main track ALL, SAT Competition 2020.
- Second Place Award in Planning track, SAT Competition 2020.
- Gold Medal in FLoC (Federated Logic Conference) Olympics 2018.
- First Place Award in No-Limits track, SAT Competition 2018.
- Second Place Award in Sparkle SAT Challenge 2018.
- Third Place Award in Random track, SAT Competition 2017.
- Second Place Award in Random track, SAT Competition 2016.
- Second Place Award in Hard-combinatorial SAT track, SAT Competition 2014.
- Third Place Award in Random SAT track, SAT Competition 2014.
- Best Solver Award in Random SAT track, SAT Challenge 2012.
Applications of our SAT solvers
- Spectrum Repacking:
Our CCASat solver (the DCCA version) has been used by the US Federal Communication Commission (FCC) for spectrum repacking in the context of bandwidth auction which resulted in about 7 billion dollar revenue. In the project, our solver is one of the core SAT solvers.
[Alexandre Fréchette, Neil Newman, Kevin Leyton-Brown: Solving the Station Repacking Problem. AAAI 2016: 702-709]
- Configuring Software Product Lines:
Our faster WalkSAT solver was used in Configuring Software Product Lines.
[Yi Xiang, Yuren Zhou, Zibin Zheng, Miqing Li: Configuring Software Product Lines by Combining Many-Objective Optimization and SAT Solvers. ACM Trans. Softw. Eng. Methodol. 26(4): 14:1-14:46 (2018)]
- Filtering benchmarks in SAT Competition:
Our CCASat solver was one of the two benchmarking solvers that were used to filter the benchmarks in random track of SAT Competition 2013. Those instances where the benchmarking solvers failed to find a solution in 600 seconds were considered to be unsatisfiable.
[Adrian Balint, Anton Belov, Marijn J.H. Heule, Matti J¨arvisalo: Generating the Uniform Random Benchmarks for SAT Competition 2013. Proceedings of SAT Competition 2013, pp.97-98]
- Computational argumentation :
Our CCASat solver used in a state of the art method for computing preferred extensions of abstract argumentation.
[Dangdang Niu, Lei Liu, Shuai Lü: New stochastic local search approaches for computing preferred extensions of abstract argumentation, AI Communications 31(4), pp. 369-382, 2018]