Ich bin neu in der Verwendung von Z3py, und meine Aufgabe ist es, Gegenbeispiele für beide Lösungen (gesättigt und ungesättigt) zu generieren.
Gibt es eine Funktion, um ein Gegenbeispiel für eine ungesättigte Lösung zu erzeugen?Beweisen Sie eine boolesche Formel unter einigen Imples-Bedingungen in z3py
unsat bedeutet, dass es kein Modell gibt, das die angegebenen Zusicherungen erfüllt. Sie können ein Modell nur extrahieren, wenn das Problem sat ist. Also, um Ihre Frage zu beantworten, wie Sie es gestellt haben, können Sie keine Modelle aus einer unsat Lösung erstellen: Es existiert einfach nicht.
Ein typischer Ansatz besteht darin, die negation der Formel zu bestätigen, die Sie zu beweisen versuchen; und wenn diese Formel erfüllbar ist, dann ist Ihre ursprüngliche Formel falsifizierbar; d.h. es gibt ein Gegenbeispiel dafür. Vielleicht versuchen Sie das? Das heißt: Wenn die Negation der Formel ein zufriedenstellendes Modell hat, dann ist dieses Modell ein Gegenbeispiel für die ursprüngliche Formel. So arbeiten die meisten Prüfer, die auf SMT-Lösern aufbauen, indem sie die Negation dessen, was sie zu beweisen versuchen und zurückgeben, senden. unsat. Wenn der Prüfer ein Modell zurückgibt, dann ist es ein Gegenbeispiel.