犯人は誰だ SAT encoding
solver
制約
- A:「B, Cの少なくとも一方は犯人」
st1 := (!A) == (B || C)- CNFfy
(A || B || C) && (!A || !B) && (!A || !C)
- B:「Dは犯人ではない」
st2 := (!B) == (!D)- CNFfy
st2 := (B || !D) && (!B || D)
- C:「AもDも犯人」
st3 := (!C) == (A && D)- CNFfy
(!A || !C || !D) && (A || C) && (C || D)
- D:「Aは犯人ではない」
st4 := (!D) == (!A)- CNFfy
(A || !D) && (!A || D)
- st:
st1 && st2 && st3 && st4
- solve:
(A, B, C, D) = (false, false, true, false)
- これ以外に解がないか検証したい -> 解の否定
!(!A && !B && C && !D) => A || B || !C || D を加えて解くと解なしなので唯一解
参考文献