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.[ref]
The key logical equivalence iswhere 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, says both and : enabling the feature requires its component, and an absent component excludes the feature.
Articles by others on the same topic
2-Satisfiability, often abbreviated as 2-SAT, is a decision problem in computer science and mathematical logic that involves determining the satisfiability of a boolean formula expressed in conjunctive normal form (CNF) with exactly two literals per clause. In formal terms, a 2-SAT formula consists of a conjunction (AND) of clauses, where each clause is a disjunction (OR) of exactly two literals. A literal is a variable or its negation.