Obere/untere Schranke für Variablen in einer beliebigen Satzformel bestimmen

Question

Wie kann man bei einer beliebigen Aussagenformel PHI (lineare Beschränkungen für einige Variablen) am besten die (ungefähre) obere und untere Grenze für jede Variable bestimmen?

Einige Variablen können unbegrenzt sein. In diesem Fall sollte ein Algorithmus zu dem Schluss kommen, dass es für diese Variablen keine obere/untere Grenze gibt.

z. B. PHI = (x=3 UND y>=1). Die obere und untere Schranke für x sind beide 3. Die untere Schranke für y ist 1, und y hat keine obere Schranke.

Dies ist ein sehr einfaches Beispiel, aber gibt es eine allgemeine Lösung (vielleicht mit dem SMT-Solver)?

Answer 1

Dabei wird davon ausgegangen, dass der SAT/UNSAT-Bereich jeder Variablen kontinuierlich ist.

1. Verwenden Sie einen SMT-Löser, um eine Lösung für die Formel zu finden. Wenn es keine Lösung gibt, bedeutet das, dass es keine oberen/unteren Grenzen gibt, also hören Sie auf.
2. Führen Sie für jede Variable in der Formel zwei binäre Suchvorgänge über den Bereich der Variablen durch, wobei Sie einmal nach der unteren und einmal nach der oberen Schranke suchen. Der Startwert der Suche für jede Variable ist der Wert für die Variable in der in Schritt 1 gefundenen Lösung. Verwenden Sie den SMT-Löser, um jeden Suchwert auf Erfüllbarkeit zu prüfen und die Schranken für jede Variable methodisch zu klammern.

Pseudocode für die Suchfunktionen, unter der Annahme ganzzahliger Domänenvariablen:

lower_bound(variable, start, formula)
{
    lo = -inf;
    hi = start;
    last_sat = start;
    incr = 1;
    do {
        variable = (lo + hi) / 2;
        if (SMT(formula) == UNSAT) {
            lo = variable + incr;
        } else {
            last_sat = variable;
            hi = variable - incr;
        }
    } while (lo <= hi);
    return last_sat;
}

et

upper_bound(variable, start, formula)
{
    lo = start;
    hi = +inf;
    last_sat = start;
    do {
        variable = (lo + hi) / 2;
        if (SMT(formula) == SAT) {
            last_sat = variable;
            lo = variable + incr;
        } else {
            hi = variable - incr;
        }
    } while (lo <= hi);
    return last_sat;
}

-inf/+inf sind die kleinsten/größten Werte, die im Bereich der jeweiligen Variablen darstellbar sind. Wenn lower_bound -inf zurückgibt, hat die Variable keine untere Grenze. Wenn upper_bound +inf zurückgibt, hat die Variable keine obere Grenze.

Answer 2

In der Praxis erfordern die meisten dieser Optimierungsprobleme eine Art von Iteration bis zum Maximum/Minimum, die zusätzlich zum SMT-Solver eingesetzt wird. Es sind auch quantifizierte Ansätze möglich, die die besonderen Fähigkeiten des SMT-Solvers ausnutzen, aber in der Praxis erweisen sich solche Einschränkungen als zu schwierig für den zugrunde liegenden Solver. Siehe insbesondere diese Diskussion: Wie optimiert man einen Teil des Codes in Z3 (PI_NON_NESTED_ARITH_WEIGHT)?

Die meisten Hochsprachenbindungen enthalten jedoch die notwendigen Funktionen, um Ihnen das Leben zu erleichtern. Wenn Sie zum Beispiel die Haskell-SBV-Bibliothek verwenden, um z3 zu skripten, können Sie das tun:

Prelude> import Data.SBV
Prelude Data.SBV> maximize Quantified head 2 (\[x, y] -> x.==3 &&& y.>=1) 
Just [3,1]
Prelude Data.SBV> maximize Quantified (head . tail) 2 (\[x, y] -> x.==3 &&& y.>=1) 
Nothing
Prelude Data.SBV> minimize Quantified head 2 (\[x, y] -> x.==3 &&& y.>=1) 
Just [3,1]
Prelude Data.SBV> minimize Quantified (head . tail) 2 (\[x, y] -> x.==3 &&& y.>=1) 
Just [3,1]

Das erste Ergebnis lautet x=3, y=1 und maximiert x in Bezug auf das Prädikat x==3 && y>=1. Das zweite Ergebnis besagt, dass es keinen Wert gibt, der y in Bezug auf das gleiche Prädikat maximiert. Der dritte Aufruf besagt, dass x=3, y=1 das Prädikat in Bezug auf x minimiert. Der vierte Aufruf besagt, dass x=3,y=1 das Prädikat in Bezug auf y minimiert. (Siehe http://hackage.haskell.org/packages/archive/sbv/0.9.24/doc/html/Data-SBV.html#g:34 für Details).

Sie können auch die Option "Iterativ" (anstelle von quantifiziert) verwenden, damit die Bibliothek die Optimierung iterativ durchführt, anstatt Quantifizierer zu verwenden. Diese beiden Techniken sind no äquivalent, da letztere in einem lokalen Minima/Maxima stecken bleiben kann, aber iterative Ansätze könnten Probleme lösen, bei denen die quantifizierte Version für den SMT-Löser viel zu viel ist.