2-SAT
(math/two-sat.hpp)
2-SAT
2-SATを$\mathrm{O}(N + M)$($N$は論理変数の個数、$M$は節の個数)で計算するライブラリ。
概要
SAT(充足可能性問題,satisfiability problem)とは、論理変数$x_1,x_2,\ldots x_n$からなる論理式が与えられたときに、変数に真か偽かを割り当てることで式全体を真にできるかを判定する問題である。
SATは一般にはNP困難であることが知られているが、連言標準形に直したときに節内の変数の数が2以下であるものを2-SATと呼び、多項式時間で解くことが出来る。
使い方
-
two_sat(n)
: $n$頂点のSATを初期化する。
-
add_clause(s, t)
: $(s \wedge t)$を条件に加える。ただし$\lnot x$は引数では~x
で表す。
-
if_then(s, t)
: $s \to t$を条件に加える。
-
set_val(s)
: $s$を条件に加える。
-
at_most_one(nodes)
: 「$n_1,\dots,n_L$のうち真である条件が高々1つである」という条件を加える。
-
answer()
: 2-SATを解く。条件を満たす組み合わせが存在するときは各変数の値が格納されたvector<bool>
の配列を、存在しないときは空の配列を返す。
Verified with
Code
Back to top page