= 2-satisfiability
{title2=$2\text{-SAT}$}
{wiki}
= 2-SAT
{c}
{synonym}
<2-satisfiability> restricts <SAT> to <CNF> in which each <Boolean clause> has at most two <Boolean literals>. The example in <Boolean satisfiability problem> is therefore a <2-SAT> instance. Unlike general <SAT> and <3-SAT>, <2-SAT> has a <polynomial-time algorithm>; its tractability concerns finding a <satisfying assignment> or deciding that none exists, not merely checking a candidate. <3-SAT> allows up to three <Boolean literals> per <Boolean clause> and is <NP-complete>, even though it includes many individually easy instances such as this one.<CS 252, Lecture 8: Constraint Satisfaction Problems (Carnegie Mellon University)>[CS 252, Lecture 8: Constraint Satisfaction Problems, pp. 1–2, §2 examples 1 and 3; p. 3, §3 classification items 1 and 3]{ref}
The key <logical equivalence> is
$$
a\lor b\equiv(\neg a\to b)\land(\neg b\to a),
$$
where $a,b$ are <Boolean literals>. It expresses a two-<Boolean literal> <Boolean clause> as two <logical implications>. Representing these <logical implications> as edges in a <directed graph> gives a route to the <polynomial-time algorithm>. In the example, $C_2$ says both $x\to z$ and $\neg z\to\neg x$: enabling the feature requires its component, and an absent component excludes the feature.
Back to article page
