This article is within the scope of WikiProject Computer science, a collaborative effort to improve the coverage of Computer science related articles on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.
I think the article should be more precise on what formulas can be instances of a SMT. For example, satisfiability of formulas in first order predicate logic is undecidable. The same is true for first-order arithmetic over N. --Borishollas (talk) 16:28, 7 October 2008 (UTC)
I don't think the decidability of the underlying theories is relevant to whether a formula is or is not an SMT instance. SMT solvers like Simplify and CVC incorporate semidecision procedures for quantified arithmetic formulas. Clconway (talk) 16:53, 8 October 2008 (UTC)
I see. I got confused because further down is written "Most of the common SMT approaches support decidable theories". So I'm interested in what these theories are, apart from SAT. 188.8.131.52 (talk) 13:16, 9 October 2008 (UTC)
I think that the first 2 sentences in the section titled "SMT Solver Approaches" are misplaced. The approach described is decidedly NOT SMT - its how you would solve the problem if you didnt have an SMT solver. I think it belongs under a motivation section or perhaps in the introduction — Preceding unsigned comment added by 184.108.40.206 (talk) 23:05, 1 January 2013 (UTC)
The section that defines "basic terms" makes SMT sound a whole lot like answer set programming (ASP)(actually, identical, after my quick skim). However, ASP doesn't have quantifiers. But then we read that many SMT solvers don't support/have quantifiers either. So at least, this level, ASP and SMT have a lot of similarity, in terms of both expressiveness, and presumably also in speed/performance (as they get based on the same/similar algos). So .. what, precisely is the difference? linas (talk) 19:35, 9 June 2011 (UTC)
There's a connection, but there's two big differences with ASP: S and MT. :-) First, SMT is about Satisfiability, a "yes" or "no" decision problem, whereas ASP is about finding a set of satisfying models. Some SMT solvers can produce models for satisfiable formulas, but this is a rare, experimental feature. Second, SMT is Modulo Theories: the solvers incorporate special-purpose procedures for interpreted functions and constants from background theories. AFAICT, ASP works strictly on uninterpreted predicate logic formulas. Clconway (talk) 21:11, 11 June 2011 (UTC)
Hmm, yes. Many of the SMT solvers focus on bitvectors and arrays & etc. so that they can be used for formal verification in hardware/software. From what I can tell, though, the theories of bitvectors & arrays, etc. can be reduced to uninterpreted predicate logic formulas (I'd really like to know if I'm wrong or right on this). If so, then I'd expect comparable performance (for satisfiability) for both ASP and SMT when working on hardware/software design verification... linas (talk) 21:00, 15 June 2011 (UTC)