Wie behandelt Z3 nichtlineare Ganzzahlarithmetik?

Question

Ich bin mir bewusst, dass die Theorie der Ganzzahlen mit Multiplikation generisch unentscheidbar ist. In bestimmten Fällen gibt Z3 jedoch ein Modell zurück. Ich bin neugierig zu wissen, wie das gemacht wird. Hat es etwas mit dem neuen Entscheidungsverfahren für nichtlineare Arithmetik über Real zu tun? Welche spezifischen Instanzen (zB: Integer unter endlichem Modulus usw.) wurden erkannt, für die Z3 ein Modell für eine Multiplikationsabfrage zurückgibt? Jede Hilfe wird sehr geschätzt.

Answer 1

Ja, das Entscheidungsproblem für nichtlineare Ganzzahlarithmetik ist unentscheidbar. Wir können das Halting-Problem für Turing-Maschinen in nichtlinearer Ganzzahlarithmetik codieren. Ich empfehle dringend das schöne Buch Hilbert's tenth problem für alle an diesem Problem interessiert.

Beachten Sie, dass, wenn eine Formel eine Lösung hat, wir sie immer mit roher Gewalt finden können. Das heißt, wir führen alle möglichen Zuordnungen auf und prüfen, ob sie der Formel entsprechen oder nicht. Dies ist nicht anders als zu versuchen, das Halting-Problem zu lösen, indem Sie einfach das Programm ausführen und prüfen, ob es nach einer bestimmten Anzahl von Schritten beendet wird.

Z3 führt keine naive Aufzählung durch. Bei einer Nummer k codiert es jede Integer-Variable unter Verwendung von k Bits und reduziert alles in die Anweisungslogik. Dann wird ein SAT-Löser verwendet, um eine Lösung zu finden. Wenn eine Lösung gefunden wird, konvertiert sie sie zurück in eine Ganzzahllösung für die ursprüngliche Formel. Wenn es keine Lösung für die formale Aussage gibt, versucht es, k zu erhöhen, oder wechselt zu einer anderen Strategie. Diese Reduktion auf Aussagenlogik ist im Wesentlichen ein Modell/Lösungsfindungsprozedur. Es kann nicht zeigen, dass ein Problem keine Lösung hat. Für Probleme, bei denen jede Integer-Variable eine untere und eine obere Grenze hat, kann sie dies tun. Also muss Z3 andere Strategien verwenden, um zu zeigen, dass keine Lösung existiert.

Darüber hinaus funktioniert die Reduktion in die propositionale Logik nur, wenn es eine sehr kleine Lösung gibt (eine Lösung, die eine kleine Anzahl von zu codierenden Bits benötigt). Ich diskutiere, dass im folgenden Beitrag:

• Need help understanding the equation

Z3 nicht gute Unterstützung hat für nichtlineare Integer-Arithmetik. Der oben beschriebene Ansatz ist sehr einfach. Meiner Meinung nach, scheint Mathematica das umfassendste Portfolio an Techniken zu haben:

http://reference.wolfram.com/legacy/v5_2/functions/AdvancedDocumentationDiophantinePolynomialSystems

Schließlich ist der nichtlineare reale Arithmetik (NLSat) Solver nicht standardmäßig für nicht-lineare Integer-Probleme verwendet wird. Bei ganzzahligen Problemen ist es normalerweise sehr ineffektiv. Trotzdem können wir Z3 zwingen, NLSat auch für ganzzahlige Probleme zu verwenden. Wir müssen einfach ersetzen:

(check-sat) 

Mit

(check-sat-using qfnra-nlsat) 

Wenn dieser Befehl verwendet wird, Z3 wird das Problem als ein echtes Problem lösen. Wenn keine echte Lösung gefunden wird, wissen wir, dass es keine ganzzahlige Lösung gibt. Wenn eine Lösung gefunden wird, prüft Z3, ob die Lösung Integer-Variablen tatsächlich ganzzahlige Werte zuweist. Wenn dies nicht der Fall ist, wird unknown zurückgegeben, um anzuzeigen, dass das Problem nicht behoben wurde.