Exactly what quantifiers require SMT?

Question

I reviewed various SMT solvers, mainly Z3, CVC4 and VeriT. All of them have vague descriptions of their ability to solve SMT problems with the help of quantifiers. Their documentation is mainly based on examples (Z3) or consists of scientific articles describing possible changes that may or may not be implemented.

I know that there are solvable fragments of first-order logic, such as:

• Defined Limited Quantifiers
• First order monadic logic

What would I like to know which classes (if any) of FOL are the various SMT solvers guaranteed to be complete? How can I find out if there is a problem I'm looking for in the fragments that they fill in?

Answer 1

There are two categories of quantized formulas for which CVC4 is complete.

(1) Quantitative formulas with final domains.

CVC4 is the final model for quantifiers for uninterpreted genera, which means that if there is a model where all uninterpreted varieties are interpreted as final, then CVC4 will eventually find it. For more information, you can see this article:
http://homepage.divms.uiowa.edu/~ajreynol/tplp17.pdf
which summarizes the work of the conference:
http://homepage.divms.uiowa.edu/~ajreynol/cav13.pdf
http://homepage.divms.uiowa.edu/~ajreynol/cade24.pdf
Please note that these methods combine with any theory supported by CVC4. Provided that the theory is decidable and the quantitative assessment does not include (infinite) interpreted varieties, then the guarantee of the final model - completeness - remains.

The approach is also a rebuttal for some fragments, such as the Bernays-Schönfinkel-Ramsey (EPR) fragment, which means that for any unsatisfactory problem in this fragment, CVC4 will ultimately respond with "unsat".

If you are interested in this feature, CVC4 will by default not use the final search model for input problem. The command line option "--finite-model-find" allows you to use these methods.

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

For example, CVC4 is complete for (pure) quantitative linear arithmetic. See this article for more details:
http://homepage.divms.uiowa.edu/~ajreynol/fmsd17-instla.pdf
which builds on an earlier conference document:
http://homepage.divms.uiowa.edu/~ajreynol/cav15a.pdf

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

Answer 2

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

The connection between the choice and “can actually solve my specific problem in a certain time, I’m ready to wait,” is not so strong. So often, examples, test suites, and experimental results are the best indicator (and therefore presented).

In addition, most solvers perform heuristic rewriting and task manipulation before attempting to solve. Thus, the classical, syntactic ways of expressing defined fragments are not always applicable, since other problems can be rewritten as decibel (I hope not the other way around, but I could not promise that this would never happen!).

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