24 comments

[ 3.2 ms ] story [ 30.6 ms ] thread
Either e or f, I can't think of a reason why it can't be f...
Because e == f, and if f is true then e is true, in which case f is false, hence a contradiction, hence it cannot be f.
>Because e == f, and if f is true then e is true, in which case f is false

e != f, because they produce different results. You could say e() == f(), each having the previous answer choices as arguments and each requiring them to be false. But since e() evaluates to true, f() can't be true.

A better way to phrase it would be that, f implies e, but e doesn't imply f. In fact e implies 'not f'.
Aaaaah, I understand now. Thanks :3
E A very interesting mental brute force process to work it out though. How did other people work it out, is there a more elegant method?
(comment deleted)
Spoiler alert. View the question before reading answers posted here.
How does knowing the answer help you solve the problem?
It doesn't. Knowing the answer means you can't solve it without being influenced of other people's answers/thoughts.
Simple solution:

* A and B can't both be true, which means that C is false.

* If C is false, A must be false.

* B and D have a paradoxical relationship, given the others - if B were true, D would be true, which would make B false, so B must be false.

* D is false, given A, B, C are false.

* E is true, given A, B, C, D are false.

* F is false because E is true (typo corrected as per comment)

F is false because D is true.

F is false because E is true.

That's a fun quick brainteaser! Reminds me of those old puzzles where you'd have a list of facts -- like there are 7 houses in a row, all different colors and with different species of pets in the yard, the blue house is next to the orange house, the green house has a pet with 2 legs, etc. etc., and they provide just enough info that you can logically chain together the order of colors and pets.

They're a bit like the word-problem version of working out sudoku (vs. guessing at it, which is a different game).

This is a perfect use case for a SAT solver. Here is a solution using the Python Z3 bindings:

  from z3 import *

  def all(vars):
      result = BoolVal(True) 
      for var in vars:
          result = And(result, var)
      return result

  def any(vars):
      result = BoolVal(False)
      for var in vars:
          result = Or(result, var)
      return result

  def none(vars):
      return Not(any(vars))

  def oneof(vars):
      result = any(vars)
      for i, a in enumerate(vars):
          for b in vars[i + 1:]:
              result = And(result, Not(And(a, b)))
      return result

  vars = [Bool(c) for c in "abcdef"]

  def above(i):
      return vars[:i]

  def below(i):
      return vars[i + 1:]

  s = Solver()

  s.add(vars[0] == all(below(0)))
  s.add(vars[1] == none(below(1)))
  s.add(vars[2] == all(above(2)))
  s.add(vars[3] == oneof(above(3)))
  s.add(vars[4] == none(above(4)))
  s.add(vars[5] == none(above(5)))

  s.check()

  print(s.model())
For what it's worth, the answer is E. :)
Yup, I agree! After figuring it out by hand I was having fun encoding it for sat via this horrible pipeline:

  step 1 : write it out by hand in PBL [alpha]
  step 2 : convert it to CNF format using [beta]
  step 3 : hand-reformat it tediously to produce [gamma]
  step 4 : plug machine readable CNF into [delta]
  step 5 : receive a feasible solution! [epsilon]
[alpha]

  Main_Exp : ((a <=> (b & c & d & e & f)) & (b <=> (~c & ~d & ~e & ~f)) & (c <=> (a & b)) & (d <=> (a | b | c)) & (e <=> (~a & ~b & ~c & ~d)) & (f  <=> (~a & ~b & ~c & ~d & ~e)))
[beta] http://formal.cs.utah.edu:8080/pbl/PBL.php

... find replace, find replace, ...

[gamma]

  c multiple choice
  p cnf 6 29
  -1 2 0
  -1 3 0
  -1 4 0
  -1 5 0
  -1 6 0
  -2 -3 -4 -5 -6 1 0
  -2 -3 0
  -2 -4 0
  -2 -5 0
  -2 -6 0
  3 4 5 6 2 0
  -3 1 0
  -3 2 0
  -1 -2 3 0
  -4 1 2 3 0
  -1 4 0
  -2 4 0
  -3 4 0
  -5 -1 0
  -5 -2 0
  -5 -3 0
  -5 -4 0
  1 2 3 4 5 0
  -6 -1 0
  -6 -2 0
  -6 -3 0
  -6 -4 0
  -6 -5 0
  1 2 3 4 5 6 0
[delta] http://www.msoos.org/2013/09/minisat-in-your-browser/

[epsilon]

  This is MiniSat 2.0 beta
  ============================[ Problem Statistics ]=============================
  | |
  | Number of variables: 6 |
  | Number of clauses: 29 |
  | Parsing time: 0.00 s |
  ============================[ Search Statistics ]==============================
  | Conflicts | ORIGINAL | LEARNT | Progress |
  | | Vars Clauses Literals | Limit Clauses Lit/Cl | |
  ===============================================================================
  | 0 | 6 29 75 | 9 0 nan | 0.000 % |
  ===============================================================================
  Verified 29 original clauses.
  restarts : 1
  conflicts : 2 (2 /sec)
  decisions : 5 (0.00 % random) (5 /sec)
  propagations : 10 (10 /sec)
  conflict literals : 5 (28.57 % deleted)
  CPU time : 1 s
  
  SATISFIABLE
  v -1 -2 -3 -4 5 -6 0
5 is true, aka e.

edit: I think I am someone who interprets "one of the above" as "at least one of the above but possibly more" not "exactly one of the above". not that the interpretation makes a difference for this problem.

I just went down one by one and ruled them out, I'm surprised that people have harder ways to do it. My reasoning for ruling out each one:

a) b contradicts it.

b) cde encompass all the choices, so you can't have none of those.

c) a contradicts b.

d) abc have already been rejected.

e) works.

f) e already works.

Absolutely - thanks for sharing; you were far more concise than how I was going to explain my solution. :)