Reputation: 44386
Here I found a charming, if fairly easy logic problem:
Which answer in this list is the correct answer to this question?
- All of the below.
- None of the below.
- All of the above.
- One of the above.
- None of the above.
- None of the above.
It would be fairly easy to re-write these propositions as statements in some programing language:
def p1 = p2 && p3 && p4 && p5 && p6
def p2 = !p3 && !p4 && !p5 && !p6
def p3 = p1 && p2
and so on. What's more difficult is to actually run such a program without getting into an infinite loop.
Is there a language or library (or something) that solve this more-or-less natively? I'm thinking Prolog, because all I know about Prolog is it's used for solving "problems like this".
What would the code look like?
Upvotes: 1
Views: 329
Reputation: 40768
It is indeed trivial to solve such logic puzzles with Prolog.
For example, one approach is to use CLP(B), which stands for Constraint Logic Programming over Boolean variables and has its own tag, clpb.
Several Prolog systems ship with a CLP(B) solver. SICStus Prolog is one very prominent example.
The core idea of such an approach is to formulate the task as a constraint satisfaction problem (CSP) over Boolean variables.
In this concrete case, we can for example use the propositional variables A1, A2, ..., A6 to represent the different ways to answer the question. Each answer relates one of these variables to several others, reflecting what the answer states about other answers.
Using SICStus Prolog, a declarative description of what each answer means could look like this:
:- use_module(library(clpb)). solution([A1,A2,A3,A4,A5,A6]) :- sat(A1 =:= A2*A3*A4*A5*A6), sat(A2 =:= ~(A2+A3+A4+A5+A6)), sat(A3 =:= A1*A2), sat(A4 =:= card([1],[A1,A2,A3])), sat(A5 =:= ~(A1+A2+A3+A4)), sat(A6 =:= ~(A1+A2+A3+A4+A5)).
From the following query, we see that only one answer is logically admissible subject to these constraints:
?- solution(Vs). Vs = [0, 0, 0, 0, 1, 0].
Thus, answer 5 is the only one that can be chosen while keeping all statements consistent.
An infinite loop cannot arise in such a formulation, since each of the individual constraints always terminates, and the whole program consists only of a sequence of such constraints.
The constraint solver has automatically deduced the single admissible solution, using a process called constraint propagation.
Upvotes: 4