Exactly what quantifiers is SMT complete for?

Question

I've been looking at various SMT solvers, mainly Z3, CVC4, and VeriT. They all have vague descriptions of their ability to solve SMT problems with quantifiers. Their documentation is primarily example based (Z3), or consists of academic papers, describing possible changes that may or may not actually be implemented.

I know that there are decidable fragments of First-order logic, such as:

• Finitely-bounded quantifiers
• Monadic first-order logic

What I'd like to know is, which (if any) classes of FOL are the various SMT solvers guaranteed to be complete for? How can I know whether a problem I'm looking at is in the fragments they are complete for?

Answer 1

There are two categories of quantified formulas that CVC4 is complete for.

(1) Quantified formulas with finite domains.

CVC4 is finite-model-complete on quantifiers over uninterpreted sorts, meaning that if there is a model where all uninterpreted sorts are interpreted as finite, then CVC4 will eventually find it. For details, you can see this paper:
http://homepage.divms.uiowa.edu/~ajreynol/tplp17.pdf
which summarizes the conference papers here:
http://homepage.divms.uiowa.edu/~ajreynol/cav13.pdf
http://homepage.divms.uiowa.edu/~ajreynol/cade24.pdf
Notice that these techniques combine with any theory supported by CVC4. Provided that the theory is decidable and the quantification does not involve (infinite) interpreted sorts, then the finite-model-completeness guarantee remains.

The approach is also refutation-complete for certain fragments, such as the Bernays-Schoenfinkel-Ramsey fragment (EPR), meaning that for any unsatisfiable problem in this fragment, CVC4 will eventually answer "unsat".

If you are interested in this feature, CVC4 will not by default use finite model finding on an input problem. The command-line option "--finite-model-find" will enable these techniques.

(2) Quantified formulas in some theories that emit quantifier elimination.

For example, CVC4 is complete for (pure) quantified linear arithmetic. For details you can see this paper:
http://homepage.divms.uiowa.edu/~ajreynol/fmsd17-instla.pdf
which builds upon an earlier conference paper:
http://homepage.divms.uiowa.edu/~ajreynol/cav15a.pdf

This is similar in spirit to other approaches, for instance in Z3:
https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-qplay-lpar20.pdf

Answer 2

At the risk of unhelpfully not answering the question, there are reasons why this material is hard to find.

The link between decideability and "actually can solve my specific problem in an amount of time I am willing to wait" is not that strong. So often examples, sets of benchmarks and experimental results are a better indicator (and thus are presented).

Also, most solvers do an amount of heuristic rewriting and problem manipulation before trying to solve. So classical, syntactic ways of expressing decideable fragments aren't always applicable as other problems can be rewritten into decieable ones (hopefully not the other way around but I couldn't promise it never happens!).

Finally, many solvers use heuristic semi-decision procedures which work well but are hard to describe in something more formal than code. Thus there are things that may not appear in any known decideable fragment, but for which answers can be found.