2-SAT

蟻本p.288

SAT…充足可能性問題(SATisfiability 英語で充足可能性)

論理式が与えられた時に、変数に適切な値をうまく割り振ることで、全体の値を真にできるか？

というのがSAT。用語が多いので

(a∨ b∨ …) ∧ (c∨ d∨…）∧…

のように一番外側の計算が∧だけで作られていたりする論理式を乗法標準形と言います。

a,b,c…のそれぞれをリテラルと言います。(a∨ b∨ …)の部分をクロージャと言い、クロージャ内のリテラルの数が最大でも2つまでしかない乗法標準形に対する充足可能性問題(SAT)を2-SATと言います。3-SATもある。

「または」を「ならば」に変換する

ならば ⇒ とは

まず、論理記号で「ならば(⇒)」というのがあります。表にすると

table:⇒

A B 出

1 1 1

1 0 0

0 1 1

0 0 1

という風になるやつです。A⇒Bみたいな感じです。

「日本人なら日本語が話せる」という命題が偽になるのは、「日本人なのに(A=1)日本語が話せない(B=0)」という時

というふうに考えると挙動に納得がいきやすいです。

変換する

A∨B は、 (¬A⇒B)∧(¬B⇒A) という風に変換できます。紙に描くと分かりやすいかも。

これをグラフで表します。すると¬BとかAとかが色々につながったグラフができます。

https://gyazo.com/863dda06a3d100b532e2da599097f5ef

強連結の部分は1,0だとどちらかで偽が発生してしまうので、強連結成分は全て同じ真偽値を取る必要があります。

つまり、強連結成分にAと¬Aがあると確実に不可能なことがわかります。可能判定はこうしたらできるそう。

ここから後はよくわからないです。後々ググります。