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