Module twosat 

2-SAT in linear time via the implication graph + strongly-connected components.

A clause of at most two literals (a ∨ b) is equivalent to the two implications ¬a → b and ¬b → a. Over all clauses these form an implication graph on the 2n literals; the formula is unsatisfiable iff some variable x lies in the same SCC as ¬x (so x → ¬x and ¬x → x, forcing x both ways). Otherwise a model is read off the SCC condensation’s topological order. Kosaraju’s two-pass SCC makes the whole decision O(n+m) — and certified: a model is re-checkable, and an Unsat returns the conflicting variable, whose mutual implication is_refutation independently re-derives by reachability.

Structs

Lit

A literal: variable var, positive when pos.

Enums

TwoSatOutcome

The outcome of solving a 2-SAT instance.

Functions

is_refutation

Re-check an Unsat witness: in the implication graph, x reaches ¬x and ¬x reaches x (mutual implication ⇒ no value of x is consistent). A solver-free certificate.

satisfies

Re-check a satisfying assignment: every clause has a true literal.

solve

Decide a 2-SAT instance (clauses of two literals each — a unit clause is (a, a)). Returns a satisfying assignment, or the variable whose SCC contains both polarities.