Could you please post the `fixed` solution in a separate gist? Thanks!
import z3
answers = [z3.Bool(f"answer{i}") for i in range(1,7)]
implications = [
z3.And(answers[1:]), # All of the below
z3.Not(z3.Or(answers[2:])), # None of the below
z3.And(answers[:2]), # All of the above
z3.Or(answers[:3]), # Any of the above
z3.Not(z3.Or(answers[:4])), # None of the above
z3.Not(z3.Or(answers[:5]))] # None of the above
# An answer should be True if and only if its "implication" is true
constraints = [ans == impl for ans, impl in zip(answers, implications)]
z3.solve(constraints) # Prints the right solution
# Try to find another solution by rejecting the previous one
constraints.append(z3.Or(*answers[:4], z3.Not(answers[4]), answers[5]))
z3.solve(constraints) # no solution
I am trying to understand what is happening on line 18 (what's the * operator in front of `answers[:4]` for?) and wondering if it could be re-written more generically based on the output of line 14 (i.e. by saving the result from the first `.solve(constraints)` call on line 14 and automatically appending it as a constraint of something to reject on line 18. Does that make sense?
z3.Or(*answers[:4])Of course it can be re-written more generically, but I thought it would be less explicit in this example
import z3
answers = [z3.Bool(f"answer{i}") for i in range(1,7)]
implications = [
z3.And(answers[1:]), # All of the below
z3.Not(z3.Or(answers[2:])), # None of the below
z3.And(answers[:2]), # All of the above
z3.Or(answers[:3]), # Any of the above
z3.Not(z3.Or(answers[:4])), # None of the above
z3.Not(z3.Or(answers[:5]))] # None of the above
# An answer should be True if and only if its "implication" is true
constraints = [ans == impl for ans, impl in zip(answers, implications)]
solver = z3.Solver()
solver.add(constraints)
# Print all solutions
while solver.check() == z3.sat:
solution = solver.model()
print(solution)
solver.add(z3.Or([variable() != solution[variable] for variable in solution]))In your first post, you mentioned that the Z3 (which I agree with you is awesome!) solution is less clever than the generic Python one. What additional changes would you implement in order to make it more clever or did you mean something else entirely?