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

SATって，こう言い換えられるよね？

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}\)

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