Editing 2-satisfiability (section)

===Renamable Horn satisfiability===
Next to 2-satisfiability, the other major subclass of satisfiability problems that can be solved in polynomial time is [[Horn-satisfiability]]. In this class of satisfiability problems, the input is again a formula in conjunctive normal form. It can have arbitrarily many literals per clause but at most one positive literal. {{harvtxt|Lewis|1978}} found a generalization of this class, ''renamable Horn satisfiability'', that can still be solved in polynomial time by means of an auxiliary 2-satisfiability instance. A formula is ''renamable Horn'' when it is possible to put it into Horn form by replacing some variables by their negations. To do so, Lewis sets up a 2-satisfiability instance with one variable for each variable of the renamable Horn instance, where the 2-satisfiability variables indicate whether or not to negate the corresponding renamable Horn variables.
In order to produce a Horn instance, no two variables that appear in the same clause of the renamable Horn instance should appear positively in that clause; this constraint on a pair of variables is a 2-satisfiability constraint. By finding a satisfying assignment to the resulting 2-satisfiability instance, Lewis shows how to turn any renamable Horn instance into a Horn instance in polynomial time.<ref>{{citation
 | last = Lewis | first = Harry R. | author-link = Harry R. Lewis
 | doi = 10.1145/322047.322059
 | issue = 1
 | journal = [[Journal of the ACM]]
 | mr = 0468315
 | pages = 134–135
 | title = Renaming a set of clauses as a Horn set
 | volume = 25
 | year = 1978| s2cid = 3071958 | doi-access = free
 }}.</ref> By breaking up long clauses into multiple smaller clauses, and applying a linear-time 2-satisfiability algorithm, it is possible to reduce this to linear time.<ref>{{citation
 | last = Aspvall | first = Bengt
 | doi = 10.1016/0196-6774(80)90007-3
 | issue = 1
 | journal = Journal of Algorithms
 | mr = 578079
 | pages = 97–103
 | title = Recognizing disguised NR(1) instances of the satisfiability problem
 | volume = 1
 | year = 1980}}.</ref>