z3 traite la puissance différente de la multiplication pour les problèmes entiers non linéaires

Question

J'utilise l'API z3 C++ et j'ai quelques problèmes concernant l'arithmétique des entiers non linéaires où z3 semble traiter différemment le pouvoir et la multiplication.

E.g. x*x*x > y*y est sat, mais x^3 > y^2 est 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; 
} 

Je l'ai déjà lu sur certains problèmes de python (Z3 python treats x**2 different than x*x?), mais j'utilise la version 4.4.0 de z3 où cela devrait être fixé.

J'ai rencontré ce problème en essayant de résoudre x^51> y^17. Je sais que l'arithmétique des entiers non linéaires est indécidable en général, mais j'étais un peu surpris que z3 n'ait trouvé aucune solution pour cela (même si elle était réécrite en tant que multiplication). Donc, je voudrais savoir si ce qui précède est un bug, ou s'il y a un moyen d'obtenir de meilleurs résultats de z3 en C++ pour ces exemples.

Answer 1

Ce n'est pas un bug, Z3 n'a tout simplement pas un bon support pour les problèmes entiers non-linéaires; voir aussi How does Z3 handle non-linear integer arithmetic?

Cet exemple n'est résolu par aucun des solveurs arithmétiques réels non linéaires, mais par une étape de pré-traitement qui traduit tout en vecteurs binaires, puis en bit-blasts, et exécute un solveur SAT pur; voir . Cette tactique ne supporte pas l'exponentiation et donc dans le second appel de solveur, elle va jusqu'au solveur SMT (le plus général), qui abandonne rapidement. Le problème général demeure même si nous ajoutons le support de l'exponentiation à nla2bv, et il produirait aussi de très grandes formules SAT pour les grands exposants, donc je pense qu'il y a une valeur limitée à l'ajouter.