Hacker News Reader

Comment by lovasoa | Hacker News Reader

Here is a single python statement that solves the problem:

    print([
        q for q in itertools.product((True, False), repeat=6)
        if q == (
            all(q[1:]),  # 1. All of the below.
            not any(q[2:]),  # 2. None of the below.
            all(q[:2]),  # 3. All of the above.
            any(q[:3]),  # 4. One of the above.
            not any(q[:4]),  # 5. None of the above.
            not any(q[:5]),  # 6. None of the above.
        )
    ])

https://gist.github.com/lovasoa/f2b4ed93e755bf4172583d28f206...

View on HN

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)

Not 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.)

I 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.

I 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.

The 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.)

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!

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/e09edb6b52f093022d90c66298...

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?

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

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"

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

> 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?

Had to look up z3

https://github.com/Z3Prover/z3

Slight variation:

    import itertools

    def below(n):
        return slice(n+1, None)

    def above(n):
        return slice(None, n)

    print([
        q for q in itertools.product((True, False), repeat=6)
        if q == tuple(
            f(i) for i, f in enumerate([
                lambda n: all(q[below(n)]),  # 1. All of the below.
                lambda n: not any(q[below(n)]),  # 2. None of the below.
                lambda n: all(q[above(n)]),  # 3. All of the above.
                lambda n: any(q[above(n)]),  # 4. One of the above.
                lambda n: not any(q[above(n)]),  # 5. None of the above.
                lambda n: not any(q[above(n)]),  # 6. None of the above.
            ])
        )
    ])

I see what you are doing here! Pushing it one step further, one could even do this: https://repl.it/repls/CourteousCreepyAdaware

Run it online here: https://onlinegdb.com/rkZhWVniH

Thanks for posting this, because I'm a Python n00b and I had no idea what this line was doing:

itertools.product((True, False), repeat=6)

The site made it easy for me to spend 30 seconds figuring it out. My interpretation is that that line generates what I'll call a truth table (not sure if that's what it formally is) then brute force searches for rows that satisfy all of the listed constraints.

I'd also hazard that the fact that there's only one answer is engineered into the question and not a natural product of this search.

The product of two iterables is a list of pairs of each item in the first iterable and each item in the second iterable (same as set product in math):

[a, b] × [c, d] = [(a, b), (a, c), (b, c), (b, d)]

The number of elements of the product of two iterables is the product of the number of elements of each. You can similarly have a product of 3, 4, etc. iterables.

The repeat keyword argument to product specifies that we want not a product of several different iterables, but the product of an iterable with itself N times. So we pass a tuple of all possible boolean values (True, False) and ask that it be raised to the 6th power, giving us all possible 6-tuples of all possible boolean values.

I think you have the general idea down. But as you suspected it's not a truth table. It's all cross-product permutations (hence the name `product`) of six items from the set {True, False}. So that line is creating a iterator that looks like this:

    (True, True, True, True, True, True)
    (True, True, True, True, True, False)
    (True, True, True, True, False, True)
    (True, True, True, True, False, False)
    (True, True, True, False, True, True)

Though not necessarily in this order... I'm unfamiliar with the actual implementation. Since the values are bits, they could have achieved the same effect by incrementing a six-bit integer. Which is a nice proof that the number of permutations here is 2^6. (Generally it's s^n, where s is the set size and n is the count of elements.)

Awesome thank you!

wouldn't any(q[:3]) (the 4th sentence) return true even if 2 or 3 of the above were correct? If I understand correctly, it should be true if exactly one of the above is correct, not at least one.

Although, I'm probably wrong, since the question says "which answer is correct", implying only one can be correct.

> wouldn't any(q[:3]) (the 4th sentence) return true even if 2 or 3 of the above were correct?

Yes it would !

> If I understand correctly, it should be true if exactly one of the above is correct, not at least one.

In logic, "one proposition is correct" is true even if two propositions are correct.

Reply on news.ycombinator.com