講義日程-2007年度冬学期
これ以前はhttp://wiki.livedoor.jp/tzik/d/%b7%d7%bb%bb%ce%cc%cd%fd%cf%c0へ。
- NTM(Oracle版)
- Guessing Module付きのDTM
- 入力xがセル1からセル|x|まで与えられている。
「Advice」をGuessing Moduleがセル(-1)から左に書く。
Guessing Moduleを停止してDTMとして起動。処理。停止。
- NTMでどの分岐をすべきかをあらかじめ外部から与えたもの。
- NTMを使うと多項式時間で解ける問題は、DTMで多項式時間で正解を検証できる問題。
- 命題論理の充足可能性判定問題(SAT,Satisfiability)
- 入力:CNF命題論理式(CNF,Conjunctive Normal Form,∧標準形)
- 出力:入力の論理式を満たす真偽値の組み合わせがあればTrue,なければFalse
- 入力は論理変数をn個持った論理式で、論理変数と¬と∨からなる節(Clause)を∧で連ねた形に標準化されたもの。
うまく論理変数の値を選んだとき、論理式全体を真にできるとき、その論理式は充足可能。
どの組み合わせを選んでも真にできないとき、恒偽、充足不可能と呼ぶ。
- この充足可能正門第