What are the limits of reasoning in quantified ari

问题:

I have tried several SMT solvers (CVC3, CVC4 and Z3) on the following seemingly trivial benchmark:

(set-logic LIA)
(set-info :smt-lib-version 2.0)
(assert (forall (( x Int)) (forall ((y Int)) (= y x))))
(check-sat)
(exit)

The solvers all return unknown. I understand that this is an undecidable fragment (well non-linear) but I was expecting there would be some simple instantiation heuristics that could solve it. I also tried adding some extra assertions with constants but it didn't help.

Is there a way to attack these problems and what are the limits of reasoning in quantified arithmetic in SMT?

回答1:

Pad is correct, the qe preprocessor can be quite expensive. Moreover, it is not effective in formulas coming from software verification tools such as VCC, Poirot, Dafny, VeriFast, Why3, and ESCJava2. It is not effective because the formulas produced by these applications also contain uninterpreted functions, arrays, etc.

As Pad's answer suggests, Z3 is a collection of engines. It provides APIs and commands that allow users to select which engine (or combination of engines) will be used to solve a problem. When the user just says (check-sat) is tries to guess what is the best engine for solving the input formula. The guess is based on the structure of input formula and annotations provided by the user (example: the set-logic command). We are continuously expanding the set of fragments that are automatically detected, and the set of engines we provide.

That being said, it is embarrassing that Z3 missed a fragment such as LIA and did not automatically applied the qe procedure to it. For LIA formulas, qe is usually the best option. Alternatives based on E-matching or MBQI are not effective since they are meant for completely different fragments.

I just committed code that detects LIA (even when set-logic is not used). The change is already available in the unstable (working-in-progress) branch. It will be available tomorrow in the nightly builds, and in the next official release.

回答2:

Your example falls into Linear Integer Arithmetic (LIA) category.

LIA i.e. Presburger Arithmetic admits quantifier elimination (qe) though time complexity of qe procedures is prohibitively high.

I'm not sure that CVC3 and CVC4 support quantifier elimination for LIA, but in Z3 you can do

(set-logic LIA)
(set-info :smt-lib-version 2.0)
(assert (forall (( x Int)) (forall ((y Int)) (= y x))))
(check-sat-using (then qe smt))

From Rise4Fun execution, I've got unsat result.

Here the qe tactic is a preprocessing step before applying end-game tactic smt.