SAT問題ってもっとシンプルに書けない?

SATって,こう言い換えられるよね?NAND

SATを言い換えたい

\(n\)個のbool型変数 \(x_1, x_2, …, x_n\) と演算NAND \(\uparrow\) で表される論理式\(f(x_1, x_2, …, x_n)\)に対して,\(f=\mathrm{TRUE}\)とする真理値の組 \(x_1, x_2, …, x_n\) が存在するか?

だってANDとNOTとOR (とIMPとEQ) は,全部NANDで書き換えることが出来るもんね.もちろん演算はたかだか \(\mathcal{O}(1)\) 個しか増えない.このほうが問題がシンプルに記述できる気がするんだけど,そうしないのって歴史的経緯とかあるのかな.それとも「NANDで記述するほうが汚くね?」って意見のほうが多数派なのかな…

論理演算のNAND表示

NANDの記号は \(\uparrow\) で書くらしいので,それに従って書くよ.

NAND (否定論理積)

\(A\) \(B\) \(A\uparrow B\)
0 0 1
0 1 1
1 0 1
1 1 0

\(A\uparrow B\)

NOT (否定)

\(A\) \(\lnot A\)
0 1
1 0

\(\lnot A = A\uparrow A\)

AND (論理積)

\(A\) \(B\) \(A\land B\)
0 0 0
0 1 0
1 0 0
1 1 1

\(\begin{eqnarray}A\land B &=& \lnot\,(A\uparrow B)\\&=&(A\uparrow B)\uparrow (A\uparrow B)\end{eqnarray}\)

OR (論理和)

\(A\) \(B\) \(A\lor B\)
0 0 0
0 1 1
1 0 1
1 1 1

\(\begin{eqnarray}A\lor B &=& \lnot A\uparrow\lnot B\\&=&(A\uparrow A)\uparrow (B\uparrow B)\end{eqnarray}\)

IMP (含意)

\(A\) \(B\) \(A\to B\)
0 0 1
0 1 1
1 0 0
1 1 1

\(\begin{eqnarray}A\to B &=& \lnot A\lor B\\&=&A\uparrow \lnot B\\&=&A\uparrow (B\uparrow B)\end{eqnarray}\)

これだけAとBが非対称 (交換不可能) なの,特徴的.

XOR (排他論理和)

\(A\) \(B\) \(A\oplus B\)
0 0 0
0 1 1
1 0 1
1 1 0

\(\begin{eqnarray}A\oplus B &=& (A\lor B)\land(\lnot A\lor \lnot B)\\&=&(\lnot A\uparrow \lnot B)\land (A\uparrow B)\\&=&\lnot\Bigl[(\lnot A\uparrow \lnot B)\uparrow(A\uparrow B)\Bigr]\\&=&\Bigl[(\lnot A\uparrow \lnot B)\uparrow(A\uparrow B)\Bigr]\uparrow\Bigl[(\lnot A\uparrow \lnot B)\uparrow(A\uparrow B)\Bigr]\\&=&\biggl[\Bigl(\{A\uparrow A\}\uparrow \{B\uparrow B\}\Bigr)\uparrow\Bigl(A\uparrow B\Bigr)\biggr]\uparrow \biggl[\Bigl(\{A\uparrow A\}\uparrow \{B\uparrow B\}\Bigr)\uparrow\Bigl(A\uparrow B\Bigr)\biggr]\end{eqnarray}\)

EQ (同値)

\(A\) \(B\) \(A\Leftrightarrow B\)
0 0 1
0 1 0
1 0 0
1 1 1

\(\begin{eqnarray}A\Leftrightarrow B &=& \lnot\, (A\oplus B)\\&=&(A\oplus B)\uparrow(A\oplus B)\end{eqnarray}\)

書き下すには長すぎる…笑

コメントを残す

Powered by WordPress.com. テーマ: Baskerville 2 by Anders Noren

ページ先頭へ ↑

%d人のブロガーが「いいね」をつけました。