約束編程布爾求解器

休伊，杜威和路易被他們的叔叔質疑。這些是他們的陳述：約束編程布爾求解器

•休伊：「杜威和路易在這方面有相同的份額;如果一個人是有罪的，所以是其他「

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

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

。

他們的叔叔知道他們是偵察員，他們意識到他們無法說謊。

我的解決方案。

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

約束編程布爾求解器

回答

相關問題