acl_cpp.twosat

• C++ version documentation

• Source code

twosat.two_sat

# two_sat
from acl_cpp.twosat import two_sat

Solves the 2-SAT problem. For variables \(x_0, x_1, \cdots, x_{n - 1}\) and clauses with form

• \((x_i = f) \lor (x_j = g)\),

decides whether there is a truth assignment that satisfies all clauses.

Constructor

# two_sat::two_sat(int n)
def two_sat(n: int = 0) -> two_sat

Creates a 2-SAT instance with \(n\) variables.

Constraints

• \(0 \le n < 2^{31}\)

Complexity

• \(O(n)\)

two_sat.add_clause

# void two_sat::add_clause(int i, bool f, int j, bool g)
def two_sat.add_clause(i: int, f: bool, j: int, g: bool) -> None

Adds a clause \((x_i = f) \lor (x_j = g)\).

Constraints

• \(0 \le i < n\)

• \(0 \le j < n\)

Complexity

• Amortized \(O(1)\)

two_sat.satisfiable

# bool two_sat::satisfiable()
def two_sat.satisfiable() -> bool

Determines if there is an assignment that satisfies all the clauses. Returns true if such an assignment exists, otherwise returns false.

Constraints

• Can be called multiple times.

Complexity

Let \(m\) be the number of added constraints.

• \(O(n + m)\)

two_sat.answer

# vector<bool> two_sat::answer()
def two_sat.answer() -> list[bool]

Returns the assignment that satisfies all the clauses from the last call to satisfiable.

Constraints

• Call this function after two_sat.satisfiable() returns true.

  • If called before satisfiable or when satisfiable returned false, returns a list of length \(n\) with undefined content.

Complexity

• \(O(n)\)

Examples

AC code of https://atcoder.jp/contests/practice2/tasks/practice2_h

from acl_cpp.twosat import two_sat

N, D = map(int, input().split())
X, Y = zip(*(list(map(int, input().split())) for _ in range(N)))

ts = two_sat(N)
for i in range(N):
    for j in range(i + 1, N):
        if abs(X[i] - X[j]) < D:
            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():
    print("No")
    exit()

print("Yes")
answer = ts.answer()
for i in range(N):
    print(X[i] if answer[i] else Y[i])