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.

[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

    Awards of our MaxSAT solvers

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

    Return to homepage.