Talk:Satisfiability modulo theories

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)

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. 194.39.218.10 (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

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

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)

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)

I realise that I am gravedigging here, but this is an excellent question that should be answered by the article. My take on this is that constraint programming is used rather confusingly both to describe constraint problems, of which SMT is a formalisation I would say (though it may also be seen as a formalisation of other things I guess), and to describe a family of historically and culturally different but similar technologies (MiniZinc and friends) which typically operate on discrete variable domains. I am planning to "keep with the trouble" and try to faithfully describe this at some point, but haven't gotten to it yet. AFAICT there are also no good sociological sources to verify this sort of thing. --Planetwrench (talk) 09:49, 20 October 2020 (UTC)

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)

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)

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)

CVC4 redirect

@Jochen Burghardt: I think the anonymous user is an example of why the bold face here is highly confusing. I doubt readers understand what it is indicating in this case, whether they followed the redirect to get to this page or not.

I think it would make sense to follow MOS:BOLDREDIRECT if we had a specific subsection titled CVC4, dedicated to the solver. I wouldn't be opposed to adding such a section. Caleb Stanford (talk) 16:42, 9 December 2021 (UTC)

Another option would be to bold CVC4 in the lead to the article, currently it's plain text, and to move the redirect there. But I think I would favor adding a small subsection on CVC4. Caleb Stanford (talk) 16:53, 9 December 2021 (UTC)

If you have sufficient information to write about CVC4, this would be the best. Could you put your text at CVC4, thus turning the redirect into a stub? - Jochen Burghardt (talk) 19:22, 9 December 2021 (UTC)

I'm not sure I personally have enough info to write about it. Also, it seems that there was previously an article on CVC:

https://wiki.riteme.site/w/index.php?title=CVC_(theorem_prover)&action=history that got deleted/merged. (See talk section above.) Caleb Stanford (talk) 05:04, 11 December 2021 (UTC)