Ich versuche, den z3-Solver für ein Minimierungsproblem zu verwenden. Ich habe versucht, eine Auszeit zu bekommen und die bisher beste Lösung zurückzugeben. Ich benutze die Python-API und die Timeout-Option "smt.timeout" mit

set_option("smt.timeout", 1000) # 1s timeout

Dieses Timeout dauert ca. 1 Sekunde. Ein größeres Timeout liefert jedoch kein kleineres Ziel. Am Ende drehte ich die Ausführlichkeit mit

set_option("verbose", 2)

Und ich denke, dass z3 sukzessive größere Werte meines Ziels bewertet, bis das Problem befriedigbar ist:

(opt.maxres [0:6117664])
(opt.maxres [175560:6117664])
(opt.maxres [236460:6117664])
(opt.maxres [297360:6117664])
...
(opt.maxres [940415:6117664])
(opt.maxres [945805:6117664])
...

Ich habe also die beiden Fragen:

Kann ich z3 im Gegensatz dazu anweisen, mit der oberen Schranke zu beginnen und nacheinander Modelle mit einem kleineren Wert für meine Zielfunktion zurückzugeben (wie zum Beispiel Minizinc-Annotationenindomain_max http: //www.minizinc.org/2.0/doc-lib/doc-annotations-search.htm) Es sieht immer noch so aus, als würde der Solver eine befriedigende Instanz meines Problems zurückgeben. Wie ist es gefunden? Wenn versucht wird, größere Werte meines Ziels nacheinander auszuwerten, sollte es zum Zeitpunkt der Zeitüberschreitung noch keine zufriedenstellende Instanz gefunden haben ...

bearbeite: Im opt.maxres-Protokoll wird die Obergrenze niemals verkleinert.

Für die Aufzeichnung fand ich eine ausführlichere Beschreibung der Optionen in der Quelle hier opt_params.pyg

Bearbeite Tut mir leid, ich habe mich in letzter Zeit wieder damit beschäftigt. Jedenfalls denke ich, dass dies für andere nützlich sein könnte. Ich habe festgestellt, dass ich tatsächlich das @ anrufen muOptimize.upper -Methode, um die Obergrenze zu erhalten, und das Modell ist immer noch nicht das Modell, das dieser Obergrenze entspricht. Ich konnte es als neue Einschränkung hinzufügen und einen Solver aufrufen (ohne Optimierung, nur SAT), aber das ist wahrscheinlich nicht die beste Idee. Durch LesenDie Ich fühle mich wie ich @ anrufen sollOptimize.update_upper, nachdem der Solver das Zeitlimit überschritten hat, aber das Python-Interface hat keine solche Methode (?). Zumindest kann ich jetzt die obere Schranke und das entsprechende Modell erhalten (auf Kosten unnötiger Berechnungen, denke ich).