Talk:Satisfiability modulo theories

From Wikipedia, the free encyclopedia
Jump to: navigation, search
WikiProject Computer science (Rated Start-class, Low-importance)
WikiProject icon 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.
Start-Class article Start  This article has been rated as Start-Class on the project's quality scale.
 Low  This article has been rated as Low-importance on the project's importance scale.
edit·history·watch·refresh Stock post message.svg To-do list for Satisfiability modulo theories:

Here are some tasks awaiting attention:
  • Expand : Add more information about the SMT-LIB language, which is only briefly mentioned in this article

Basic terminology[edit]

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. (talk) 13:16, 9 October 2008 (UTC)
Take a look at the SMT-LIB list of logics for a sample of what kinds of formulas SMT solver can work with. Clconway (talk) 03:24, 11 October 2008 (UTC)

Misplaced description[edit]

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 (talk) 23:05, 1 January 2013 (UTC)

CVC merge[edit]

I think we should probably just delete the CVC article and information rather than copy-and-paste it into this one. It's out of place where it is now. Clconway (talk) 14:15, 6 June 2008 (UTC)

relation to constraint programming?[edit]

How is SMT related to constraint programming? Is it the same thing invented by a different community? Eclecticos (talk) 01:33, 15 March 2010 (UTC)


Another SMT solver, which should listed there is MiniSmt. Here is the external link: MiniSmt —Preceding unsigned comment added by (talk) 08:47, 22 February 2011 (UTC)

Relation to answer set programming ?[edit]

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)