恒真式判定は co-NP 完全

コメント欄で id:qnighy が「ソース読んでないけど、たしかisTautってco-NP完全でしたよね」と言っていたのだけどその辺を勉強していないボクとしては何を意図しているのかわけわかめな感じになったので Wikipedia の記事をざっくり読んでみた．まあそれでもどういう意図なんだろう…という疑問は晴れなかったので得たばかりの拙い知識を使って予想してみると，まず充足可能性問題は NP 完全な問題なのでその補題である恒真式判定は co-NP 完全，つまりこの問題は多項式時間では判定できないはずだから式変形で解けるわけがない! ということで良いのかなあ．
まあやぱり式変形での判定は難しそうだなーというのはよく分かっていてたぶんこのプログラムを使っても判定できない論理式もたくさんあると思いますよ．というかさっき自分が試した限りでも (Not (And (And (Or (Var 'x') (Var 'y')) (Or (Not (Var 'x')) (Var 'y'))) (And (Or (Var 'x') (Not (Var 'y'))) (Or (Not (Var 'x')) (Not (Var 'y')))))) がちゃんと判定されなかったりしたので残念ながら昨日のプログラムは不完全のようです．