Editing Horn-satisfiability (section)

In [[formal logic]], '''Horn-satisfiability''', or '''HORNSAT''', is the [[Decision problem|problem]] of deciding whether a given conjunction of propositional [[Horn clause]]s is [[Boolean satisfiability|satisfiable]] or not. Horn-satisfiability and Horn clauses are named after [[Alfred Horn]].<ref name="Horn51">{{cite journal |last1=Horn |first1=Alfred |title=On sentences which are true of direct unions of algebras |journal=Journal of Symbolic Logic |date=March 1951 |volume=16 |issue=1 |pages=14–21 |doi=10.2307/2268661}}</ref>

A Horn clause is a [[Clause (logic)|clause]] with at most one positive [[literal (mathematical logic)|literal]], called the ''head'' of the clause, and any number of negative literals, forming the ''body'' of the clause. A Horn formula is a [[propositional formula]] formed by [[logical and|conjunction]] of Horn clauses.

Horn satisfiability is actually one of the "hardest" or "most expressive" problems which is known to be computable in polynomial time, in the sense that it is a [[P-complete|'''P'''-complete]] problem.<ref name="CookNguyen2010">{{cite book|author1=Stephen Cook|author2=Phuong Nguyen|title=Logical foundations of proof complexity|url=https://books.google.com/books?id=2aW2sSlQj_QC&pg=PA224|year=2010|publisher=Cambridge University Press|isbn=978-0-521-51729-4|page=224}} ([https://www.cs.toronto.edu/~sacook/homepage/book Author's 2008 draft version], see p.213f)</ref> The extension of the problem for [[Quantified Boolean formula|quantified]] Horn formulae can be also solved in polynomial time.<ref name="buningkarpinski">{{Cite journal | last1 = Buning | first1 = H.K. | last2 = Karpinski| first2 =  Marek| last3=Flogel|first3=A.|year = 1995 | title = Resolution for Quantified Boolean Formulas | journal = Information and Computation | volume = 117 | issue = 1 | pages = 12–18 | publisher = Elsevier | doi= 10.1006/inco.1995.1025| doi-access = free }}</ref>

The Horn satisfiability problem can also be asked for propositional [[many-valued logic]]s. The algorithms are not usually linear, but some are polynomial; see Hähnle (2001 or 2003) for a survey.<ref>{{cite book|editor=Dov M. Gabbay, Franz Günthner|title=Handbook of philosophical logic|chapter-url=https://books.google.com/books?id=_ol81ow-1s4C&pg=PA373|year=2001|publisher=Springer|isbn=978-0-7923-7126-7|page=373|chapter=Advanced many-valued logics|author=Reiner Hähnle|edition=2nd|volume=2}}</ref><ref name="FittingOrlowska2003">{{cite book|editor=Melvin Fitting, [[Ewa Orłowska]]|title=Beyond two: theory and applications of multiple-valued logic|year=2003|publisher=Springer|isbn=978-3-7908-1541-2|author=Reiner Hähnle|chapter=Complexity of Many-valued Logics}}</ref>