<p>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.</p>
<p>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?</p>
<p>Some reference questions related between SAT/SMT solvers and TCS:</p>
<p><a href="https://cstheory.stackexchange.com/questions/37886/theoretical-explanations-for-practical-success-of-sat-solvers">Theoretical explanations for practical success of SAT solvers?</a></p>
<p><a href="https://cstheory.stackexchange.com/questions/42072/sat-solvers-and-their-applications">SAT Solvers and their applications</a></p>
<p><a href="https://cstheory.stackexchange.com/questions/37886/theoretical-explanations-for-practical-success-of-sat-solvers">Theoretical explanations for practical success of SAT solvers?</a></p>
<p><a href="https://cstheory.stackexchange.com/questions/40725/ways-to-think-formally-about-satisfiability-modulo-theories">Ways to think formally about Satisfiability Modulo Theories</a></p>

CC BY-SA 4.0
2023-01-29T20:02:20.587Z
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)](https://homepage.cs.uiowa.edu/~tinelli/papers/NieOT-JACM-06.pdf) very helpful for understanding how SMT solvers are combining SAT- and theory solvers.
Martin Berger
CC BY-SA 4.0
2023-01-30T04:54:39.800Z
@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.
Zunchen Huang
CC BY-SA 4.0
2023-01-30T16:04:39.480Z
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
Martin Berger
CC BY-SA 4.0
2023-01-30T16:06:38.670Z
Theory composition is an important research field, pioneered by [G. Nelson, D. Oppen, Simplification by cooperating decision procedures](https://dl.acm.org/doi/pdf/10.1145/357073.357079) from nearly half a century ago. In practise, as far as I am aware, theory solvers are monolithic and not built up compositionally.
Martin Berger
CC BY-SA 4.0
2023-01-30T19:22:55.480Z
@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?
Zunchen Huang
CC BY-SA 4.0
2023-01-31T23:29:28.067Z
I'm afraid theory solvers are far from my area of expertise. Maybe the authors or reviewers of this book on [Decision Procedures](https://www.decision-procedures.org/) would be able to offer advice?
Martin Berger
<sat>
What advancements in SMT solvers have contributed to progress in the field of theoretical computer science?
Zunchen Huang
# What advancements in SMT solvers have contributed to progress in the field of theoretical computer science?

(Asked by: username_0 on 2023-01-28)

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?](https://cstheory.stackexchange.com/questions/37886/theoretical-explanations-for-practical-success-of-sat-solvers)

[SAT Solvers and their applications](https://cstheory.stackexchange.com/questions/42072/sat-solvers-and-their-applications)

[Theoretical explanations for practical success of SAT solvers?](https://cstheory.stackexchange.com/questions/37886/theoretical-explanations-for-practical-success-of-sat-solvers)

[Ways to think formally about Satisfiability Modulo Theories](https://cstheory.stackexchange.com/questions/40725/ways-to-think-formally-about-satisfiability-modulo-theories)

**Tags:** sat
> **Comments:**
> **username_1**: 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)](https://homepage.cs.uiowa.edu/~tinelli/papers/NieOT-JACM-06.pdf) very helpful for understanding how SMT solvers are combining SAT- and theory solvers.  
> **username_0**: @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.  
> **username_1**: 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  
> **username_1**: Theory composition is an important research field, pioneered by [G. Nelson, D. Oppen, Simplification by cooperating decision procedures](https://dl.acm.org/doi/pdf/10.1145/357073.357079) from nearly half a century ago. In practise, as far as I am aware, theory solvers are monolithic and not built up compositionally.  
> **username_0**: @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?  
> **username_1**: I'm afraid theory solvers are far from my area of expertise. Maybe the authors or reviewers of this book on [Decision Procedures](https://www.decision-procedures.org/) would be able to offer advice?  

---

## 0 answers

