# Symbolically formulate the two guard problem so it can be solved by a computer

Take the classic two guard riddle (I don't know where the origin of this riddle is, so I'll take the version from http://www.calpoly.edu/~mcarlton/riddles.html):

You stand at a fork in the road. Next to each of the two forks, there stands a guard. You know the following things: 1. One path leads to Paradise, the other to Death. From where you stand, you cannot distinguish between the two paths. Worse, once you start down a path, you cannot turn back. 2. One of the two guards always tells the truth. The other guard always lies. Unfortunately, it is impossible for you to distinguish between the two guards. You have permission to ask one guard one question to ascertain which path leads to Paradise. Remember that you do not know which guard you're asking -- the truth-teller or the liar -- and that this single question determines whether you live or die. The question is: What one question asked of one guard guarantees that you are led onto the path to Paradise, regardless of which guard you happen to ask?

The solution given by that site, which is the one that's usually given, is

"If I asked the other guard, which door would he indicate leads to Paradise?" Take the door opposite to what's indicated! Regardless of whom you ask, they'll point to the wrong door.

My question is, how could I formulate the puzzle symbolically, so that I could give it to a SAT solver or some other kind of logic solver, and get a "solution" (the solution should be a query for a guard that allow you to deduce which path leads to Paradise)?

• I don't know much about automated theorem proving but having studied some logic, I can at least say this. The most difficult problem I have is trying to formally qualify what a "question" is. All I know for now is that at least the concept of an answer can be formalized as a set, {Paradise, Death}. At the very least, a "question" should be paired with an element of this set (call it the "correct answer" if you will) and a "lie" relative to the question is just the other element. – 0XLR Jul 8 '15 at 2:12
• As you've mentioned a SAT solver: is this question limited to propositional logic? – aphorisme Jul 8 '15 at 10:13
• I'm actually skeptical whether this can be solve with propositional logic, given the nature of the "answer", but it would obviously be nice, since SAT solvers are common and fast. – asmeurer Jul 9 '15 at 20:12