约束编程布尔求解器答案

【问题标题】：Constraint programming boolean solver约束编程布尔求解器
【发布时间】：2014-03-12 15:28:29
【问题描述】：

休伊、杜威和路易被他们的叔叔盘问。以下是他们的声明：

• 休伊：“杜威和路易平分秋色；如果一个人有罪，那么另一个人也有罪。”

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

• 路易：“杜威和我都没有罪。”

他们的叔叔知道他们是侦察兵，知道他们不能说谎。

我的解决方案。

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

【问题讨论】：

标签： constraint-programming minizinc clpb

【解决方案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))
;

【讨论】：

我明白为什么我不能写 dewey != louie？给出 =====UNSATISFIABLE===== 。但不是（杜威和路易）作品
“杜威和我都没有罪”可能是两者都没有罪。约束“dewey != louise”意味着其中一个是有罪的（另一个是无罪的）。

【解决方案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 Solver 的解决方案：http://boolsat.com/show/5320e18a0148a30002000002

【讨论】：

【解决方案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.

【讨论】：

【解决方案4】：

另一种选择是询问WolframAlpha：

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

按照 Hakan 的建议，以下equivalent expression 也是可能的：

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

结果是一个真值表，只有(!D !H !L) 作为解。

【讨论】：

不应该包括L吗？ IE。像“（D等价L）和（H暗示D）而不是（D和L）”之类的东西？这给了 (!L !D !H)。
@Hakan：感谢您的友好指正。我已经确定了答案。