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