Is there a way to retrieve all satisfying assignments using SMTLIB2 syntax?
The solvers I am using are Z3 and CVC4.
Asked
Active
Viewed 149 times
1 Answers
0
Although there is no way to do this in "pure" SMTLIB2, i.e. just with a single file and no external input, if you have an application that can interact with the solver, there's a standard trick to doing this. You run the solver in interactive mode, where you can send it SMTLIB2 commands one at a time, and then interact with it in the following way (pseudocode):
def get_all_assignments(instance):
create solver in interactive mode
for each declaration, assertion, etc. in instance:
send assertion to solver
let response := None
while response is not UNSAT:
send command '(check-sat)' to solver and get response
if response is SAT:
send command '(get-model)' to solver and get model
print model
send the solver a new assertion which is the negation of the model
Effectively, every time you find a satisfying assignment, you add a new constraint to your model that prevents the solver from finding that assignment again, and ask it to re-solve. When the solver returns UNSAT you know that you have found every satisfying assignment.
For further reading on this topic and implementations for Z3, refer to Z3: finding all satisfying models and Z3py: checking all solutions for equation.
