Editing Horn-satisfiability (section)

==Generalization==

A generalization of the class of Horn formulae is that of renamable-Horn formulae, which is the set of formulae that can be placed in Horn form by replacing some variables with their respective negation. Checking the existence of such a replacement can be done in linear time; therefore, the satisfiability of such formulae is in P as it can be solved by first performing this replacement and then checking the satisfiability of the resulting Horn formula.<ref>{{cite journal
 | 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| doi-access = free
 }}.</ref><ref>{{cite journal
 | 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><ref>{{cite journal
 | last = Hébrard | first = Jean-Jacques
 | doi = 10.1016/0304-3975(94)90015-9
 | issue = 2
 | journal = [[Theoretical Computer Science (journal)|Theoretical Computer Science]]
 | mr = 1260003
 | pages = 343–350
 | title = A linear algorithm for renaming a set of clauses as a Horn set
 | volume = 124
 | year = 1994| doi-access = 
 }}.</ref><ref>
{{cite journal
| last=Chandru
| first=Vijaya
|author2=Collette R. Coullard|author2-link=Collette Coullard |author3=Peter L. Hammer |author4=Miguel Montañez |author5=Xiaorong Sun
 | title=On renamable Horn and generalized Horn functions
| journal=Annals of Mathematics and Artificial Intelligence
| year=2005
| doi=10.1007/BF01531069
| volume=1
| issue=1–4
| pages=33–47
}}</ref> Horn satisfiability and renamable Horn satisfiability provide one of two important subclasses of satisfiability that are solvable in polynomial time; the other such subclass is [[2-satisfiability]].

===Dual-Horn SAT===

A dual variant of Horn SAT is '''Dual-Horn SAT''', in which each clause has at most one negative literal. Negating all variables transforms an instance of Dual-Horn SAT into Horn SAT. It was proven in 1951 by Horn that Dual-Horn SAT is in [[P_(complexity)|P]]. {{Citation needed|reason=where is the paper|date=November 2022}}