Which answer in this list is the correct answer to this question? (2017)

Post by Recursing » Mon, Nov 18, 2019, 9:07 PM UTC

krasi0 wrote: post #130

Recursing wrote: post #107

Earlier quoted context omitted.

I can't edit, but you're right, implications should be bidirectional (expressed in z3 using == instead of z3.Implies) You can limit the number of true answers with "atMost" "atLeast" and "PbEq" I mostly wanted to show off how cool z3 is (especially with python imho), the subtleties of the wording of the problem itself don't seem too important

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

Post by krasi0 » Thu, Nov 21, 2019, 7:14 PM UTC

Recursing wrote: post #131

krasi0 wrote: post #130

Earlier quoted context omitted.

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

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 co…

Post by krasi0 » Mon, Nov 25, 2019, 12:25 PM UTC

Recursing wrote: post #134

krasi0 wrote: post #133

Earlier quoted context omitted.

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 automaticall…

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…

Post by krasi0 » Mon, Nov 25, 2019, 6:23 PM UTC

Recursing wrote: post #136

krasi0 wrote: post #135

Earlier quoted context omitted.

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?

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