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)
  • 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"

    Selected Papers


    Awards of our MaxSAT solvers

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