相転移

充足可能性問題 (satisfiability problem, SAT) 「与えられた論理式を真にする真偽値$x_1, x_2 \dots$が存在するか？」という問題を充足可能性問題という。 この問題の最も一般的な形は、NP 完全であることが知られている。 例: $(x_1 \lor x_2) \land (x_1 \lor \bar{x_2}) \land (\bar{x_1} \lor \bar{x_2})$ 解: $x_1=\text{True}$, $x_2=\text{False}$ この例のように$\bigwedge_i \bigvee_j x_{i,j}$で表される論理式を連言標準形といい、その各項の変数の数が 2 以下であるとき 2-SAT と呼ばれる。 2-SAT は多項式時間で解けるアルゴリズムが存在する。 一方で項の変数の数が 3 以下の 3-SAT は NP 完全であることが知られている。 問題の生成 3-SAT 問題は DIMACS CNF で記述される。 c example DIMACS-CNF 3-SAT p cnf 3 5 -1 -2 -3 0 1 -2 3 0 1 2 -3 0 1 -2 -3 0 -1 2 3 0 行頭がcの行はコメントである。 行頭がpの行には変数が 3 つで項数が 5 項である。 また、 -1 -2 -3 0は$\bar{x_1} \lor \bar{x_2} \lor \bar{x_3}$を示している。...