[Recursing]

The * operator is a argument unpacking operator in python (see 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]

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]

"Less clever" was used with a positive connotation, as in "simpler"

[krasi0]

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 :)