パズルはブール方程式の連立系
真実を話す人を1、嘘つきを0とします。発言者の文の値が自身の役割ビットと一致するとき整合します。
SX(R) = RX
ラボは各 X で S_X(R) = R_X を確認します。全方程式が同じ役割ベクトル R を共有し、同時に成立する必要があります。
各文は完全な役割割り当てのブール関数です。
1つの矛盾が可能世界全体を消去する
役割割り当てを仮定し、各文を評価して発言者の役割と比較します。
SX(R) ≠ RX ⇒ reject R
1つでも不一致なら割り当て全体を棄却できます。ヒントは仮定と、その分岐を不可能にする方程式を示します。
矛盾は世界が規則を満たせないことを証明します。
解けるだけでは不十分：答えは一意であるべき
整合するパズルでも、有効な割り当てが複数ある場合があります。
|{R : ∀X, SX(R)=RX}| = 1
生成した各パズルを全探索し、残る世界がちょうど1つの場合だけ採用します。
緑の世界が論理系の唯一のモデルです。
強い手掛かりは多くの世界を消す
有用な文は候補を分けます。弱い文はほぼ全候補で同じ値かもしれません。
candidates: 2n → … → 1
ヒントは未適用のうち最も多くの世界を消す方程式を選び、答えへ飛ばずに不確実性を減らします。
情報量の多い方程式で候補数が減ります。
自己言及が必ず役立つとは限らない
「私は真実を話す」は両方の役割と整合し、新しい情報を与えません。
SX(R) = RX
「私は嘘をついている」は厳密な規則ではどちらの役割でも整合しません。生成器は両方を除外し、参加者間の関係を使います。
一方は恒真な自己主張、他方は充足不能な方程式です。