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]

**SATLike**

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.

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"

- Zhendong Lei, Shaowei Cai: Solving (Weighted) Partial MaxSAT by Dynamic Local Search for SAT.
*IJCAI*2018: 1346-1352 [SATLike conference paper, v1.0] - Kenji Kanazawa, Shaowei Cai: FPGA Acceleration to Solve Maximum Clique Problems Encoded into Partial MaxSAT. MCSoC 2018: 217-22
- 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] - Shohei Sassa, Kenji Kanazawa, Shaowei Cai, Moritoshi Yasunaga: An FPGA Solver for Partial MaxSAT Problems Based on Stochastic Local Search. SIGARCH Computer Architecture News 44(4): 32-37 (2016)
- Shaowei Cai, Zhong Jie, Kaile Su: An effective variable selection heuristic in SLS for weighted Max-2-SAT. J. Heuristics 21(3): 433-456 (2015)
- 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)

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

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

Return to homepage.