Ich interessiere mich für MAX-SAT und hatte gehofft, dass Z3 dies als eingebautes Feature haben würde. Gibt es Pläne, dies in naher Zukunft zu tun?

In Ermangelung des oben Genannten habe ich versucht, die Beispielanwendung maxsat von der Befehlszeile aus zu verwenden. Leider erhalte ich immer die folgende Antwort, wenn ich exec.sh "filename.z3" mache: "überprüfe, ob harte Bedingungen erfüllbar sind ... Ergebnis: 0". Was mache ich falsch? Ich versichere Ihnen, dass diese Antwort völlig unabhängig vom tatsächlichen Inhalt der Datei zu sein scheint.

Schließlich geben die Kommentare im Beispiel "maxsat" nicht eindeutig an, wie Einschränkungen als hart oder weich gekennzeichnet werden sollen. Eine harte Einschränkung soll eine Formel sein, der Folgendes vorausgeht: Formel, und eine weiche Einschränkung eine Formel, der Folgendes vorausgeht: Annahme. Um "(assert (> x 0))" als weich zu markieren, wo genau setzen wir die ": Annahme"? (Ich habe die Abfrage zu harten und weichen Einschränkungen gelesen, aber die Frage / Antwort schien eher im Zusammenhang mit dem Auffinden nicht erfüllbarer Kerne zu stehen als mit "maximal erfüllbaren Kernen" nicht erfüllbarer Formeln.)