Constraint programming boolean solver

Question

Huey, Dewey and Louie are being questioned by their uncle. These are the statements they make:

• Huey: “Dewey and Louie had equal share in it; if one is guilty, so is the other.”

• Dewey: “If Huey is guilty, then so am I.”

• Louie: “Dewey and I are not both guilty.”

Their uncle, knowing that they are scouts realizes that they cannot tell a lie.

My solution.

var bool :D; var bool :L; var bool :H;
    constraint D <->L;
    constraint H -> D;
    constraint D!=L;
    solve satisfy;
    output[show(D), "\n", show(L),"\n", show(H)];

Minizinc can't solve it.

score 3 · Answer 1 · answered Mar 12 '14 at 17:07

3

Here's my (old) version of this problem: http://www.hakank.org/minizinc/huey_dewey_louie.mzn

 var bool: huey;
 var bool: dewey;
 var bool: louie;

 constraint
   %  Huey: Dewey and Louie has equal share in it; if one is quitly, so is the other.
   (dewey <-> louie)

   %  Dewey: If Huey is guilty, then so am I.
   /\
   (huey -> dewey)

   %  Louie: Dewey and I are not both quilty.
   /\
   (not (dewey /\ louie))
;

answered Mar 12 '14 at 17:07

hakank

6,629
1
17
27

I see why can't i write dewey != louie? gives =====UNSATISFIABLE===== . but not (dewey and louie) works – user2975699 Mar 12 '14 at 18:10
2

"Dewey and I are not both guilty" might been that neither is guilty. The constraint "dewey != louise" means that one of them is guilty (and the other is not guilty). – hakank Mar 12 '14 at 18:12

score 2 · Answer 2 · answered Mar 12 '14 at 22:48

For this kind of problems I prefer to use Boolean Satisfiability (SAT) directly. Your problem can obviously be formulated as a propositional logic formula as follows (using the DIMACS format) :

Atom 1 : Dewey is guilty (i.e. will be associated to the literals -1 and 1 in the CNF) Atom 2 : Louie is guilty (i.e. will be associated to the literals -2 and 2 in the CNF) Atom 3 : Huey is guilty (i.e. will be associated to the literals -3 and 3 in the CNF)

The CNF file is then :

p cnf 4 3
-1 2 0
-2 1 0
-3 1 0
-1 -2 0

And here the solution using an 'online' SAT Solver : http://boolsat.com/show/5320e18a0148a30002000002

score 2 · Answer 3 · answered Nov 04 '14 at 13:00

Yet another solution, using CLP(B) (constraint logic programming over Boolean variables) with SICStus Prolog or SWI:

:- use_module(library(clpb)).

guilty(H, D, L) :-
    sat(D =:= L), % Huey
    sat(H =< D),  % Dewey
    sat(~(D*L)).  % Louie

Example query and its result:

?- guilty(H, D, L).
D = H, H = L, L = 0.

Axel Kemper · Answer 4 · 2014-03-13T19:02:26.480

1

Another option is to ask WolframAlpha:

not (L xor D) and (H implies D) and not (L and D)

As suggested by Hakan, the following equivalent expression is also possible:

(L equivalent D) and (H implies D) and not (L and D)

Result is a truth table which has only (!D !H !L) as solution.

enter image description here

edited Mar 13 '14 at 19:02

answered Mar 13 '14 at 16:55

Axel Kemper

10,544
2
31
54

Shouldn't L be included? I.e. something like "(D equivalent L) and (H implies D) and not (D and L)"? This give (!L !D !H). – hakank Mar 13 '14 at 17:39
@Hakan: Thank you for your friendly correction. I've fixed my answer. – Axel Kemper Mar 13 '14 at 18:55

Constraint programming boolean solver

4 Answers4