Z3: Finden aller befriedigenden Modelle

Question

Ich versuche, alle möglichen Modelle für einige Theorie erster Ordnung mit Z3, einem von Microsoft Research entwickelten SMT-Löser, zu erhalten. Hier ist ein minimales Arbeitsbeispiel:

(declare-const f Bool) 
(assert (or (= f true) (= f false))) 

In diesem propositionalen Fall gibt es zwei erfüllenden Belegungen: f->true und f->false. Da Z3 (und SMT-Solver im Allgemeinen) nur versuchen werden, ein befriedigendes Modell zu finden, ist es nicht direkt möglich, alle Lösungen zu finden. Here Ich fand einen nützlichen Befehl namens (next-sat), aber es scheint, dass die neueste Version von Z3 dies nicht mehr unterstützt. Das ist etwas unglücklich für mich, und im Allgemeinen finde ich den Befehl sehr nützlich. Gibt es eine andere Möglichkeit, dies zu tun?

Answer 1

Eine Möglichkeit, dies zu erreichen, ist die Verwendung einer der APIs zusammen mit der Modellgenerierungsfunktion. Sie können dann das generierte Modell aus einer Erfüllbarkeitsprüfung verwenden, um Einschränkungen hinzuzufügen, um zu verhindern, dass frühere Modellwerte in nachfolgenden Erfüllbarkeitsprüfungen verwendet werden, bis keine zufrieden stellenden Zuordnungen mehr vorhanden sind. Natürlich müssen Sie endliche Sortierungen verwenden (oder einige Einschränkungen haben, die dies gewährleisten), aber Sie können dies auch mit unendlichen Sortierungen verwenden, wenn Sie nicht alle möglichen Modelle finden möchten (dh, nachdem Sie einen Haufen erzeugen) .

Hier ist ein Beispiel unter Verwendung von z3py (Link Skript z3py: http://rise4fun.com/Z3Py/a6MC):

a = Int('a') 
b = Int('b') 

s = Solver() 
s.add(1 <= a) 
s.add(a <= 20) 
s.add(1 <= b) 
s.add(b <= 20) 
s.add(a >= 2*b) 

while s.check() == sat: 
    print s.model() 
    s.add(Or(a != s.model()[a], b != s.model()[b])) # prevent next model from using the same assignment as a previous model 

Im Allgemeinen sollten die disjunct aller beteiligten Konstanten arbeiten (zum Beispiel a und b hier). Dies führt alle Ganzzahlzuweisungen für a und b (zwischen 1 und 20) auf, die a >= 2b erfüllen. Zum Beispiel, wenn wir a und b beschränken, anstatt zwischen 1 und 5 liegen, ist der Ausgang:

[b = 1, a = 2] 
[b = 2, a = 4] 
[b = 1, a = 3] 
[b = 2, a = 5] 
[b = 1, a = 4] 
[b = 1, a = 5]