约束编程布尔求解器

休伊，杜威和路易被他们的叔叔质疑。这些是他们的陈述：约束编程布尔求解器

•休伊：“杜威和路易在这方面有相同的份额;如果一个人是有罪的，所以是其他“

•杜威：‘如果休伊是有罪的，那么我也是。’

•路易：‘杜威和我不都无罪’

。

他们的叔叔知道他们是侦察员，他们意识到他们无法说谎。

我的解决方案。

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无法解决它。

来源

2014-03-12 user2975699

这里的这个问题我的（旧）版本：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)) 
;

来源

2014-03-12 17:07:18 hakank

我明白了为什么我不能写杜威！=路易？给出 =====不合格===== 。但不是（杜威和路易）作品 – user2975699

“杜威和我都不是两个有罪”可能是因为这两个都不是有罪。约束“dewey！= louise”意味着其中一个是有罪的（另一个是无罪的）。 – hakank

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

原子1：杜威有罪（即将与CNF中的文字-1和1相关）原子2： Louie有罪（即将与CNF中的文字-2和2相关）原子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

来源

2014-03-12 22:48:20 Med

另一种选择是要求WolframAlpha：

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

正如所建议的哈坎，以下equivalent expression也是可能的：

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

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

enter image description here

来源

2014-03-13 16:55:17

不应该包括在内吗？即像“（D当量L）和（H暗示D）而不是（D和L）”？这给（！L！D！H）。 – hakank

@Hakan：谢谢你的友好改正。我已经解决了我的答案。 –

又一解决方案，使用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.

来源

2014-11-04 13:00:19 mat

约束编程布尔求解器

回答

相关问题