z3 - Quantifier Elimination - More questions

Question

Many thanks Josh and Leonardo for answering the previous question.

I have few more questions.

<1> Consider another example.

(exists k) i * k > = 4 and k > 1.

This has a simple solution i > 0. (both for Int and Real case)

However, when I tried following,

(declare-const i Int)
(assert (exists ((k Int)) (and (>= (* i k)  4) (> k 1))))
(apply (using-params qe :qe-nonlinear true))

Z3 Could not eliminate quantifier here.

However, it could eliminate for a Real case. (when i and k are both reals) Is Quantifier Elimination more difficult for integers?

<2> I am using Z3 C API in my system. I am adding some non-linear constraints on Integers with quantifiers in my system. Z3 currently checks for satisfiability and gives me a correct model when the system is satisfiable.

I know that after quantifier elimination, these constraints get reduced to linear constraints.

I thought that z3 does quantifier elimination automatically before checking satisfiability. But since, it couldn't do that in case 1 above, I now think, that it usually finds a model without Quantifier Elimination. Am I correct?

Currently z3 can solve the constraints in my system. But it may fail on complex systems. In such case, is it a good idea to do quantifier elimination by some other method without z3 and add constraints to z3 later?

<3> I can think of adding Real non-linear constraints instead of Integer non-linear constraints in my system. In that case, how can I enforce z3 to do Quantifier Elimination using C-API ?

<4> Finally, is this a good idea to enforce z3 to do Quantifier Elimination? Or it usually finds a model more intelligently without doing Quantifier Elimination?

Thanks.

Answer 1

<1> The theory of nonlinear integer arithmetic does not admit quantifier elimination (qe). Moreover, the decision problem for nonlinear integer arithmetic is undecidable.

Recall that, Z3 has limited support for quantifier elimination of nonlinear real arithmetic formulas. The current procedure is based on virtual term substitution. Future versions, may have full support for nonlinear real arithmetic.

<2> Quantifier elimination is not enabled by default. The user must request it. Z3 may find models for satisfiable formulas even when quantifier elimination is not enabled. It uses a technique called model-based quantifier instantiation (MBQI). The Z3 online tutorial has several examples describing capabilities and limitations of this technique.

<3> You have to enable it when you create the Z3_context object. Any option that is set in the command line, can be provided during Z3_context object creation. Here is an example, that enables model construction and quantifier elimination:

Z3_config cfg = Z3_mk_config();
Z3_context ctx;
Z3_set_param_value(cfg, "MODEL", "true");
Z3_set_param_value(cfg, "ELIM_QUANTIFIERS", "true");
Z3_set_param_value(cfg, "ELIM_NLARITH_QUANTIFIERS", "true");
ctx = mk_context_custom(cfg, throw_z3_error);
Z3_del_config(cfg);

After that, ctx is pointing to a Z3 context object that supports model construction and quantifier elimination.

<4> The MBQI module is not complete even for the linear arithmetic fragment. The Z3 online tutorial describes the fragments it is complete. MBQI module is a good option for problems that contain uninterpreted functions. If your problems only use arithmetic, then quantifier elimination is usually better and more efficient. That being said, several problems can be quickly solved using MBQI.