constraint-programming - 约束编程布尔求解器

Question

休伊、杜威和路易正在接受他们叔叔的盘问。这些是他们所做的声明：

• 休伊：“杜威和路易在其中占有同等份额；如果一个人有罪，那么另一个人也有罪。”</p>

• 杜威：“如果休伊有罪，那我也是。”</p>

• Louie：“杜威和我都没有罪。”</p>

他们的叔叔知道他们是童子军，意识到他们不能说谎。

我的解决方案。

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 解决不了。

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

对于这类问题，我更喜欢直接使用布尔可满足性（SAT）。您的问题显然可以表述为如下命题逻辑公式（使用 DIMACS 格式）：

Atom 1：Dewey 有罪（即与 CNF 中的文字 -1 和 1 相关联） Atom 2：Louie 有罪（即将与 CNF 中的文字 -2 和 2 相关联） Atom 3：Huey 有罪（即将与 CNF 中的文字 -3 和 3 相关联）

CNF 文件是：

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

这里使用“在线”SAT求解器的解决方案：http: //boolsat.com/show/5320e18a0148a30002000002

Answer 3

另一个解决方案是使用 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 4

另一种选择是询问WolframAlpha：

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

正如 Hakan 所建议的，以下等价表达式也是可能的：

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

(!D !H !L)结果是一个仅作为解决方案的真值表。