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]
Local Search MaxSAT Solvers
SATLike is a state of the art local search solver for solving (weighted) Partial MaxSAT instances. It is the first local search solver that competes well with the modern SAT-based MaxSAT solvers on industrial instances.
Codes :
SATLike (this version participated in MaxSAT Evaluation 2018)
SATLike3.0 (updated 2020)
CCLS is a local search solver for weighted (non-partial) MaxSAT based on the configuration checking (CC) strategy.
Running CCLS under Linux 64bit OS: ./CCLS "instance" "seed" "cutoff_time"
LinearLS is a local search solver for Pure MaxSAT problems.
Pure MaxSAT is an important subclass of Partial MaxSAT, where all hard clauses are pure clauses (a clause is pure if the literals in it are all of the same polarity, either positive or negative) and are with the same polarity, while all soft clauses are pure clauses with the opposite polarity
Selected Papers
- Shaowei Cai, Xindi Zhang: Pure MaxSAT and Its Applications to Combinatorial Optimization via Linear Local Search. CP 2020: 90-106 [LinearLS solver]
- Shaowei Cai, Zhendong Lei: Old techniques in new ways: Clause weighting, unit propagation and hybridization for maximum satisfiability. Artif. Intell. 287: 103354 (2020) [SATLike journal paper, v1.0-v3.0, and also the hybrid solvers LinSBPS* and OpenWBO*]
- Zhendong Lei, Shaowei Cai: Solving (Weighted) Partial MaxSAT by Dynamic Local Search for SAT. IJCAI 2018: 1346-1352 [SATLike conference paper, v1.0]
- Chuan Luo, Shaowei Cai, Kaile Su, Wenxuan Huang: CCEHC: An efficient local search algorithm for weighted partial maximum satisfiability. Artif. Intell. 243: 26-44 (2017)
- Shaowei Cai, Chuan Luo, Haochen Zhang: From Decimation to Local Search and Back: A New Approach to MaxSAT. IJCAI 2017: 571-577
- Shaowei Cai, Chuan Luo, Jinkun Lin, Kaile Su: New local search methods for partial MaxSAT. Artif. Intell. 240: 1-18 (2016) [Dist]
- Chuan Luo, Shaowei Cai, Wei Wu, Zhong Jie, Kaile Su: CCLS: An Efficient Local Search Algorithm for Weighted Maximum Satisfiability. IEEE Trans. Computers 64(7): 1830-1843 (2015)
Awards of our MaxSAT solvers
In MaxSAT Evaluation 2021 complete solvers track (2 categories ,1 unweighted,1 weighted), our solver placed 1st in weighted category and 2nd in unweighted category.
In MaxSAT Evaluation 2021 incomplete solvers track (4 categories , 2 unweighted and 2 weighted), our solver placed 1st in both 2 unweighted categories,and 1st in weighted with 60s timeout.
In MaxSAT Evaluation 2020 incomplete solvers track (totally 4 categories, 2 unweighted and 2 weighted),
SATLike-c placed 1st in
both 2 unweighted categories, and 2nd in both 2 weighted category.
In MaxSAT Evaluation 2018 incomplete solvers track,
SATLike-c placed 1st in
2 categories (out of 4).
In MaxSAT Evaluation 2016
incomplete solvers track, our solvers placed 1st in 3 categories (out of 9).
In MaxSAT Evaluation 2015
incomplete solvers track , our solvers placed 1st in 5 categories (out of 9).
[2014.7.18]: In MaxSAT Evaluation 2014
incomplete solvers track, our solvers placed 1st in 5 categories (out of 9).
In MaxSAT Evaluation
2013 incomplete solvers track, our solver placed 1st
in 4 categories (out of 9).
Applications of our MaxSAT solvers
- Solving Ising model in materials research at MIT
[Wenxuan Huang, Daniil A. Kitchaev, Stephen T. Dacek, Ziqin Rong, Alexander Urban, Shan Cao, Chuan Luo, and Gerbrand Ceder: Finding and proving the exact ground state of a generalized Ising model by convex optimization and MAX-SAT, Physical Review B 94, 134424 (2016)]
- Our constraint weighting methods have been used to deal with the multiple priority level optimization problems in the Tencent Digital Map by the Tencent Company, which improves the performance of the navigation system.
- Our MaxSAT solvers have been used to deal with the wirless sensors location problem in the China Construction Bank.