CODEWITHSUNDEEP
constraint-programmingminizincclpb
user2975699
user2975699

Reputation: 595

Constraint programming boolean solver

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.

Upvotes: 3

Views: 529

Answers (4)

mat
mat

Reputation: 40768

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.

Upvotes: 2

Axel Kemper
Axel Kemper

Reputation: 11322

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

Upvotes: 1

Med
Med

Reputation: 176

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

Upvotes: 2

hakank
hakank

Reputation: 6854

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

Upvotes: 3

Related Questions