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]
SMT Solvers
YicesLS is dedicated for SMT on Integer Difference Logic. It is a hybrid solver combinging Yices with a local search solver that works diretcly on variables.
Integer Difference Logic(IDL) contains arithmetic atomicformulas constraining the difference between the values of pairs of integer variables in the form of a-b ≤ k, where a,b are integer variables and k is integer constant. IDL can naturally express various problems involving timing-related constraints including scheduling, circuit timing analysis, and bounded checking of timed automata.
Award:
>
YicesLS won the 1st place in the Single-Query and Model Validation track in SMT-COMP2021 on IDL theory.
Links
- SMT-LIB: The Satisfiability Modulo Theories Library