SMT-LIB does not have an "check-all-sat" mode.
The format is describe on: http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.0-r12.09.09.pdf
You can interact with SMT-LIB using a file pipe to parse/print your way to get all answers in a way that is suitable to your problem. The programmatic APIs, such as the python API, are much more flexible.
How to solve a liars/truth-tellers instance using Z3Py and Z3 SMT-LIB
Pregunta
Example Problem:
Suppose that liars always speak what is false, and truth-tellers always speak what is true. Further suppose that Amy, Bob, Cal, Dan, Erny and Francis are each either a liar or truth-teller.
Amy says, “Bob is a liar.”
Bob says, “Cal is a liar.”
Cal says, “Dan is a liar”
Dan says, “Erny is a liar”
Erny says, “Francis is a liar”
Francis says, “Amy, Bob, Cal, Dan and Erny are liars ”
Which, if any, of these people are truth-tellers?
Solution:
Interpretations:
A : Amy is a truth-teller (X[0])
B : Bob is a truth-teller (X[1])
C : Cal is a truth-teller (X[2])
D : Dan is a truth-teller (X[3])
E : Erny is a truth-teller (X[4])
F : Francis is truth-teller (X[5])
Code:
def add_constraints(s, model):
X = BoolVector('x', 6)
s.add(Implies(X[0], Not(X[1])),Implies(Not(X[1]),X[0]),
Implies(X[1],Not(X[2])), Implies(Not(X[2]),X[1]),
Implies(X[2],Not(X[3])), Implies(Not(X[3]),X[2]),
Implies(X[3],Not(X[4])), Implies(Not(X[4]),X[3]),
Implies(X[4],Not(X[5])), Implies(Not(X[5]),X[4]),
Implies(X[5], And(Not(X[0]),Not(X[1]),Not(X[2]),Not(X[3]),Not(X[4]))),
Implies(And(Not(X[0]),Not(X[1]),Not(X[2]),Not(X[3]),Not(X[4])), X[5]))
notAgain = []
i = 0
for val in model:
notAgain.append(X[i] != model[X[i]])
i = i + 1
if len(notAgain) > 0:
s.add(Or(notAgain))
return s
s = Solver()
i = 0
add_constraints(s, [])
while s.check() == sat:
print s.model()
i = i + 1
add_constraints(s, s.model())
print i # solutions
Output:
[x1 = False,
x5 = False,
x0 = True,
x3 = False,
x4 = True,
x2 = True]
1
Intepretation:
Amy is a truth-teller
Bob is a liar
Cal is a truth-teller
Dan is a liar
Erny is a truth-teller
Francis is a liar
Run this example online here
Please let me know what do you think and if it is possible to solve this problem using Z3-SMT-LIB. Many thanks.
Solución
Otros consejos
Using Vampire and Prover 9:
fof(axio1,axiom,( (truthteller(amy))
<=> (~ truthteller(bob) ) )).
fof(axio2,axiom,
( ( truthteller(bob)
<=> (~ truthteller(cal)) ) )).
fof(axio3,axiom,
( ( truthteller(cal)
<=> (~ truthteller(dan)) ) )).
fof(axio4,axiom,
( ( truthteller(dan)
<=> (~ truthteller(erny)) ) )).
fof(axio5,axiom,
( ( truthteller(erny)
<=> (~ truthteller(francis)) ) )).
fof(axio6,axiom,
( ( truthteller(francis)
<=> ( (~ truthteller(amy)) & (~ truthteller(bob)) & (~ truthteller(cal))
& (~ truthteller(dan)) & (~ truthteller(erny)) ) ) )).
fof(goal1,conjecture,
(~ truthteller(francis) )).
We obtain:
% END OF SYSTEM OUTPUT
% RESULT: SOT_LlryEw - Prover9---1109a says Theorem - CPU = 0.00 WC = 0.28 Given = 0 Generated = 18 Kept = 14
% OUTPUT: SOT_LlryEw - Prover9---1109a says Refutation - CPU = 0.00 WC = 0.28
% END OF SYSTEM OUTPUT
% RESULT: SOT_LlryEw - Vampire---4.2 says Theorem - CPU = 0.00 WC = 0.01
% OUTPUT: SOT_LlryEw - Vampire---4.2 says Refutation - CPU = 0.00 WC = 0.01
Such output shows that "Francis is a liar".
Licenciado bajo: CC-BY-SA con atribución
No afiliado a StackOverflow