2-satisfiability

2-satisfiability, commonly abbreviated as 2-SAT, is the problem of determining whether a Boolean formula in which every clause contains at most two literals admits a satisfying assignment. It is a restricted form of the Boolean satisfiability problem, but its computational structure differs substantially from that of formulas containing clauses of unrestricted size. Whereas general satisfiability and 3-satisfiability are NP-complete, 2-satisfiability has deterministic algorithms whose running time is linear in the size of the formula.

A 2-SAT instance is normally expressed in conjunctive normal form. If (x_1,\ldots,x_n) are Boolean variables, each clause has the form

[ (a \lor b), ]

where (a) and (b) are literals, meaning that each is either a variable (x_i) or its negation (\neg x_i). Clauses containing one literal can be represented by repeating that literal, since ((a\lor a)) is equivalent to (a). The formula is satisfiable precisely when values can be assigned to its variables so that every clause evaluates to true.

Logical and graph-theoretic formulation

The central structural property of 2-SAT follows from the equivalence

[ (a\lor b)\equiv(\neg a\Rightarrow b)\land(\neg b\Rightarrow a). ]

Consequently, every clause can be represented by two directed implications. These implications form an implication graph having one vertex for each literal (x_i) and one vertex for each complementary literal (\neg x_i). For every clause ((a\lor b)), the graph contains an edge from (\neg a) to (b) and another edge from (\neg b) to (a).

The paired construction imposes a symmetry on the graph. If there is an implication path from a literal (a) to a literal (b), complementing the literals and reversing the implications produces a path from (\neg b) to (\neg a). This property distinguishes implication graphs arising from 2-CNF formulas from arbitrary directed graphs and accounts for the direct correspondence between graph reachability and logical consequence.

A directed implication path

[ a\rightsquigarrow b ]

means that every satisfying assignment in which (a) is true must also make (b) true. If both (a\rightsquigarrow\neg a) and (\neg a\rightsquigarrow a) hold, then either possible value of the underlying variable forces its own contradiction. In graph-theoretic terms, (a) and (\neg a) then belong to the same strongly connected component.

This yields the standard satisfiability criterion:

[ F\text{ is satisfiable} \quad\Longleftrightarrow\quad \operatorname{SCC}(x_i)\ne\operatorname{SCC}(\neg x_i) \text{ for every }i. ]

The forward direction follows because literals in the same strongly connected component imply one another and must therefore receive the same truth value in any satisfying assignment. A literal and its complement cannot both receive that value. For the reverse direction, contracting every strongly connected component produces an acyclic graph whose order can be used to assign consistent values to complementary component pairs.

Historical development

Melven R. Krom identified the polynomial-time structure of formulas with at most two literals per clause in 1967. The corresponding formulas are consequently also called Krom formulas, particularly in research on restricted logical languages and constraint satisfaction. Krom’s analysis separated the two-literal case from the computational behavior later associated with clauses containing three or more literals.

In 1974, You Watanabe expressed the consistency condition for two-literal clauses through complementary implication paths. Her formulation treated mutual reachability of a literal and its negation as the precise obstruction to satisfiability, thereby connecting the logical problem to the component structure of a directed graph. This representation also made the involution between each literal and its complement explicit at the level of the graph obtained after component contraction.

Shimon Even, Alon Itai, and Adi Shamir subsequently analyzed 2-SAT within the study of combinatorial decision problems and established a linear-time approach based on graph traversal. Their treatment contributed to the broader use of implication structures for scheduling and allocation constraints whose alternatives can be encoded by Boolean variables.

Linear-time solution

The strongly connected component formulation was developed into its standard algorithmic form by Bengt Aspvall, Michael F. Plass, and Robert Endre Tarjan. Their method computes the strongly connected components of the implication graph and tests whether any component contains both forms of the same variable. The graph has (2n) vertices when the formula has (n) variables, while a formula with (m) clauses contributes (2m) directed edges.

Algorithms such as Tarjan’s strongly connected components algorithm or Kosaraju’s algorithm process this graph in

[ O(n+m) ]

time and require linear storage. Because reading an explicitly represented formula already requires time proportional to its length, this running time is asymptotically optimal under the usual input model.

When no complementary pair occurs within a single component, the condensation graph of the implication graph is a directed acyclic graph. Its components can be arranged in a topological order in which every implication edge runs from an earlier component to a later component. Assigning a variable according to the relative positions of the components containing its two literals produces a satisfying valuation. Under the convention that edges point forward in the order, the literal whose component occurs later is assigned true and its complement is assigned false.

The correctness of this assignment follows from the closure of truth under implication. An edge cannot lead from a true component to a false component, because the ordering rule would then force the complementary components into the opposite order and contradict the selected valuation. Component pairs can therefore be assigned without violating any implication represented by the original clauses.

Computational complexity

The decision form of 2-SAT belongs to P and has a more precise classification under highly restricted computational resources. It is complete for NL under standard logarithmic-space reductions. Directed reachability supplies the relevant source of complexity, since implication paths encode the consequences that determine whether complementary literals become mutually reachable.

The placement of 2-SAT in NL also implies membership in co-NL, consistent with the Immerman–Szelepcsényi theorem that NL is closed under complementation. Unsatisfiability has a compact graph-theoretic certificate consisting of a variable together with directed paths from its positive literal to its negative literal and back again.

The tractability of the decision problem does not extend to every associated counting problem. Counting all satisfying assignments of a 2-CNF formula is the problem known as #2SAT, which is #P-complete. The implication graph determines whether at least one assignment exists, but the number of compatible selections among its complementary component pairs can encode substantially more difficult combinatorial information.

Structural interpretation

A 2-CNF formula can be regarded as a system of forbidden simultaneous choices. The clause ((a\lor b)) excludes only the valuation in which both (a) and (b) are false. The two associated implication edges record the consequences of approaching that excluded valuation from either side. Satisfiability therefore depends not on isolated clauses but on chains of consequences that circulate through the full formula.

This interpretation accounts for the role of strongly connected components. Within one component, every literal forces every other literal, so the component behaves as a single logical unit. The complement operation maps each component to another component unless the formula is inconsistent. A satisfiable instance consequently induces paired components whose relative ordering constrains, but does not always uniquely determine, the resulting assignment.