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]

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.


Return to homepage.