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]

We have developed a SMT solver for bit-vectors and arrays, which has participated in SMT competition 2018. It is being improved.

this page is to be built...

Return to homepage.