2-SAT
It solves 2-SAT.
For variables $x_0, x_1, \cdots, x_{N - 1}$ and clauses with form
- $(x_i = f) \lor (x_j = g)$,
it decides whether there is a truth assignment that satisfies all clauses.
Constructor
two_sat ts(int n)
It creates a 2-SAT of $n$ variables and $0$ clauses.
Constraints
- $0 \leq n \leq 10^8$
Complexity
- $O(n)$
add_clause
void ts.add_clause(int i, bool f, int j, bool g)
It adds a clause $(x_i = f) \lor (x_j = g)$.
Constraints
- $0 \leq i \lt n$
- $0 \leq j \lt n$
Complexity
- $O(1)$ amortized
satisfiable
bool ts.satisfiable()
If there is a truth assignment that satisfies all clauses, it returns true. Otherwise, it returns false.
Constraints
- You may call it multiple times.
Complexity
- $O(n + m)$, where $m$ is the number of added clauses.
answer
vector<bool> ts.answer()
It returns a truth assignment that satisfies all clauses of the last call of satisfiable.
If we call it before calling satisfiable or when the last call of satisfiable returns false, it returns the vector of length $n$ with undefined elements.
Complexity
- $O(n)$
Examples
AC code of https://atcoder.jp/contests/practice2/tasks/practice2_h
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]