2-SAT
2-SATを解きます。
変数 $x_0, x_1, \cdots, x_{N - 1}$ に関して、
- $(x_i = f) \lor (x_j = g)$
というクローズを足し、これをすべて満たす変数の割当があるかを解きます。
コンストラクタ
ts = initTwoSat(n:int):TwoSat
$n$ 変数の2-SATを作ります。
制約
計算量
add_clause
ts.add_clause(i:int, f:bool, j:int, g:bool):void
$(x_i = f) \lor (x_j = g)$ というクローズを足します。
制約
- $0 \leq i \lt n$
- $0 \leq j \lt n$
計算量
satisfiable
ts.satisfiable():bool
条件を足す割当が存在するかどうかを判定する。割当が存在するならばtrue、そうでないならfalseを返す。
制約
計算量
足した制約の個数を $m$ として
answer
ts.answer():seq[bool]
最後に呼んだ satisfiable の、クローズを満たす割当を返す。satisfiable を呼ぶ前や、satisfiable で割当が存在しなかったときにこの関数を呼ぶと、中身が未定義の長さ $n$ の vectorを返す。
計算量
使用例
import atcoder/header
import atcoder/twosat
let n, d = nextInt()
var x, y = newSeq[int](n)
for i in 0..<n:
(x[i], y[i]) = (nextInt(), nextInt())
# ts[i] = (i-th flag is located on x[i])
var ts = init_two_sat(n)
for i in 0..<n:
for j in i + 1 ..< n:
if abs(x[i] - x[j]) < d:
# cannot use both of x[i] and x[j]
ts.add_clause(i, false, j, false)
if abs(x[i] - y[j]) < d:
ts.add_clause(i, false, j, true)
if abs(y[i] - x[j]) < d:
ts.add_clause(i, true, j, false)
if abs(y[i] - y[j]) < d:
ts.add_clause(i, true, j, true)
if not ts.satisfiable():
echo "No"
else:
echo "Yes"
let answer = ts.answer
for i in 0..<n:
if answer[i]:
echo x[i]
else:
echo y[i]