5 ms·

Could you please post the `fixed` solution in a separate gist? Thanks!

• Recursing 7y ago
  Sure! 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 https://gist.github.com/Recursing/e09edb6b52f093022d90c662984c8a76 https://gist.github.com/Recursing/e09edb6b52f093022d90c66298...
  • krasi0 7y ago
    Sorry for the late reply. I don't get notified on replies to my posts. Thanks for the posted solution. It seems to work fine. 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?
    • Recursing 7y ago
      The * operator is a argument unpacking operator in python (see https://docs.python.org/3/tutorial/controlflow.html#unpacking-argument-lists https://docs.python.org/3/tutorial/controlflow.html#unpackin... ) z3.Or(*answers[:4]) is the same as z3.Or(answers[0], answers[1], answers[2], answers[3]) 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]))
      • krasi0 7y ago
        The trick with the `while` loop is smart! ;) Exactly what I wanted to achieve. Thanks! 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?
        • Recursing 7y ago
          "Less clever" was used with a positive connotation, as in "simpler"
          • krasi0 7y ago
            Ah, gotcha. That makes sense. I really appreciate your help with the above code. I've been meaning to get deeper into the wonderful world of Z3 for a while now and it seems like the time has come :)