z3 treats power different than multiplication for nonlinear integer problems

Question

I am using the z3 C++ API and have some problems regarding nonlinear integer arithmetic where z3 seems to treat power and multiplication differently.

E.g. x*x*x > y*y is sat, but x^3 > y^2 is unknown:

#include <z3++.h>
#include <iostream>
using namespace std;

int main() {
    z3::context c;
    auto x = c.int_const("x");
    auto y = c.int_const("y");

    z3::solver sol(c);
    sol.add(x*x*x > y*y);
    cout << sol << " : " << sol.check() << endl;

    sol.reset();
    sol.add(z3::pw(x,3) > z3::pw(y,2));
    cout << sol << " : " << sol.check() << endl;
}

I've already read about some python issues (Z3 python treats x**2 different than x*x?), but I use version 4.4.0 of z3 where that should be fixed.

I came across this problem when trying to solve x^51 > y^17. I know that nonlinear integer arithmetic is undecidable in general, but I was a bit surprised that z3 found no solution for this (even if rewritten as multiplication). So I would like to know if the above is a bug, or if there is any way to get better results from z3 in C++ for these examples.

score 1 · Accepted Answer · edited May 23 '17 at 11:44

That's not a bug, Z3 just does not have good support for non-linear integer problems; see also How does Z3 handle non-linear integer arithmetic?

This example is not solved by any of the actual non-linear arithmetic solvers, but by a pre-processing step that translates everything into bit-vectors, then bit-blasts, and runs a pure SAT solver; see nla2bv_tactic. This tactic does not support exponentiation and thus in the second solver call, it goes all the way through to the (most general) SMT solver, which promptly gives up.

The general problem remains even if we add support for exponentiation to nla2bv, and it would also produce very large SAT formulas for large exponents so I think there is limited value in adding that.

Thanks for your answer. I was not aware of the details of the tactic that is used. So I guess I'll try how well it works for me when I use multiplication instead of exponents for my project, at least for squares/cubics ;) — swad, Oct 29 '15 at 19:00

z3 treats power different than multiplication for nonlinear integer problems

1 Answers1