Ограниченное программирование булева решателя

Question

Хьюи, Дьюи и Луи допрашиваются их дядей. Вот заявления, которые они делают:

• Хьюи: "Дьюи и Луи имели равную долю в этом; если один виновен, значит и другой ".

• Дьюи: "Если Хьюи виновен, то и я тоже".

• Луи: "Мы с Дьюи не виноваты"

Их дядя, зная, что они разведчики, понимает, что не может сказать неправду.

Мое решение.

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

Миницинк не может решить это.

Answer 1

Вот моя (старая) версия этой проблемы: 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))
;

Answer 2

Еще одно решение, использующее CLP(B) (программирование логики ограничений над булевыми переменными) с SICStus Prolog или SWI:

:- use_module(library(clpb)).

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

Пример запроса и его результат:

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

Answer 3

Для такого рода проблем я предпочитаю использовать булево соответствие (SAT) напрямую. Ваша проблема, очевидно, может быть сформулирована как логическая формула высказывания следующим образом (с использованием формата DIMACS):

Атом 1: Дьюи виновен (т.е. будет связан с литералами -1 и 1 в CNF) Атом 2: Луи виновен (т.е. будет связан с литералами -2 и 2 в CNF) Атом 3: Хьюи виноват (т.е. будет связан с литералами -3 и 3 в CNF)

Файл CNF тогда:

пнф 4 3
-1 2 0
-2 1 0
-3 1 0
-1 -2 0

И вот решение с использованием "онлайн" SAT Solver: http://boolsat.com/show/5320e18a0148a30002000002

Answer 4

Другой вариант - спросить WolframAlpha:

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

Как предположил Хакан, также возможно следующее эквивалентное выражение:

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

Результатом является таблица истинности, которая имеет только (!D !H !L) как решение.