1
$\begingroup$

SMT solvers use first-order logic on top of SAT solvers with boolean logic. For example, CVC4 is an SMT solver able to accept a rich set of mixed constraints over strings, integers, reals, arrays, and algebraic datatypes.

My question is what advancements in SMT solvers have significant impacts to progress in the field of theoretical computer science? If we want to analyze the complexity of an SAT solver vs an SMT solver, is there a uniform way to deal with it? Or their components must be treated separately?

Some reference questions related between SAT/SMT solvers and TCS:

Theoretical explanations for practical success of SAT solvers?

SAT Solvers and their applications

Theoretical explanations for practical success of SAT solvers?

Ways to think formally about Satisfiability Modulo Theories

Improve this question
$\endgroup$
6
  • $\begingroup$ The question is a bit vague. SMT solvers have an extreme impact on verification of hardware and software. Maybe you can sharpen your question? I found the text Solving SAT and SAT Modulo Theories: from an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T) very helpful for understanding how SMT solvers are combining SAT- and theory solvers. $\endgroup$
    – Martin Berger
    Jan 29 at 20:02
  • $\begingroup$ @MartinBerger Thanks for the pointer. I guess a subquestion of mine is that suppose we have two formulas, one is within propositional logic and the other one is first-order logic/the logic required by a specific theory, how to uniformly analyze their complexity? Since everything has to be broken down into SAT formulas. Another situation would be harder for me to digest, between different theories, how to analyze/compare their complexity? What if there are multiple theories used? Sorry for the vagueness. Feel free to edit the question. $\endgroup$
    – hddmss
    Jan 30 at 4:54
  • $\begingroup$ There are many different notions of complexity: space, time, worst case, average case, best case, number of quantifier changes, proof complexity, number of cache misses etc. The complexity of the SAT and the theory solvers together depends on exactly what complexity you have in mind $\endgroup$
    – Martin Berger
    Jan 30 at 16:04
  • 1
    $\begingroup$ Theory composition is an important research field, pioneered by G. Nelson, D. Oppen, Simplification by cooperating decision procedures from nearly half a century ago. In practise, as far as I am aware, theory solvers are monolithic and not built up compositionally. $\endgroup$
    – Martin Berger
    Jan 30 at 16:06
  • $\begingroup$ @MartinBerger That was very helpful. I'm particularly interested in the worst case parts. If the theory solvers can be built up compositionally, it would be very interesting to see their complexity analysis. One last question, are there any research groups dedicated to or actively conducting theory composition research nowadays? $\endgroup$
    – hddmss
    Jan 30 at 19:22

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Browse other questions tagged or ask your own question.