7 ms·
A less clever solution, using the wonderful z3 import z3 answers = [z3.Bool(f"answer{i}") for i in range(1,7)] implications = [ z3.And(answers[1:])
by Recursing 7y ago
A less clever solution, using the wonderful z3
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
constraints = [z3.Implies(ans, impl) for ans,impl in zip(answers, implications)]
z3.solve(constraints)
- colanderman 7y agoNot enough constraints. You must (EDIT: should? see discussion below) also constrain that there is exactly one `answer{i}` which is true, and all the implications should be equalities (else, for example, 6 is a valid answer, even though that would imply 5 is true and thus contradict 6). It just so happens that the first result Z3 finds is the correct one. But if you exclude that result with an additional constraint, it will find another. (This is general is a good way to check your work.) (I just did the same exact exercise with Z3 and CVC4, but using SMTLIBv2 syntax.)
- arcatek 7y agoI don't think there is any constraint that a single answer is true, otherwise the exercise wouldn't list "All of them" as a possibility.
- colanderman 7y agoI feel like it's implied by the question itself? "Which answer [singular] is the [definite article] correct answer" But you may be right. I detest word puzzles for exactly this type of ambiguity. Same goes for implication vs. equality. Why "should" 5 being true contradict 6 being correct? Just because 5 happens to be true doesn't necessarily mean it is "the" "correct" answer. The "real" answer depends on an interpretation of the English-language formulation that most people will apply, but not all.
- mafuy 7y agoThe puzzle itself contains enough contradictions that a single answer is forced. So it is unclear from the question, but the result is definite: There is exactly one answer. (Of course, that fact is not obvious.)
- Recursing 7y agoI 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
- krasi0 7y agoCould you please post the `fixed` solution in a separate gist? Thanks!
- Recursing 7y agoSure! 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 agoSorry 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?
- mannykannot 7y ago> It just so happens that the first result Z3 finds is the correct one. But if you exclude that result with an additional constraint, it will find another. Having an additional constraint would be a different question, would it not?
- philshem 7y agoHad to look up z3 https://github.com/Z3Prover/z3 https://github.com/Z3Prover/z3