Talk:Satisfiability modulo theories: Difference between revisions

Content deleted Content added

Inline

Revision as of 21:11, 11 June 2011

Basic terminology

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)[reply]

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)[reply]

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. 194.39.218.10 (talk) 13:16, 9 October 2008 (UTC)[reply]

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)[reply]

CVC merge

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)[reply]

relation to constraint programming?

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)[reply]

MiniSmt

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

Relation to answer set programming ?

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)[reply]

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)[reply]

Revision as of 19:35, 9 June 2011 edit Linas (talk \| contribs) Autopatrolled 25,539 edits →Relation to answer set programming ?: new section ← Previous edit		Revision as of 21:11, 11 June 2011 edit undo Clconway (talk \| contribs) Extended confirmed users 1,134 edits →Relation to answer set programming ?: resp Next edit →
Line 25:		Line 25:

	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? [[User:Linas\|linas]] ([[User talk:Linas\|talk]]) 19:35, 9 June 2011 (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? [[User:Linas\|linas]] ([[User talk: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 ''S''atisfiability, 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 ''M''odulo ''T''heories: the solvers incorporate special-purpose procedures for interpreted functions and constants from [[theory (mathematical logic)\|background theories]]. AFAICT, ASP works strictly on uninterpreted predicate logic formulas. [[User:Clconway\|Clconway]] ([[User talk:Clconway\|talk]]) 21:11, 11 June 2011 (UTC)