From Wikipedia, the free encyclopedia

In formal logic, Horn-satisfiability, or HORNSAT, is the problem of deciding whether a given set of propositional Horn clauses is satisfiable.

A Horn clause is a clause with at most one positive 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 conjunction of Horn clauses.

The problem of Horn satisfiability is solvable in polynomial time. A polynomial-time algorithm for Horn satisfiability is based on the rule of unit propagation: if the formula contains a clause composed of a single literal l (a unit clause), then all clauses containing l are removed, and all clauses containing have this literal removed. The result of the second rule may itself be a unit clause, which is propagated in the same manner. The formula is satisfiable if this transformation does not generate a pair of opposite unit clauses l and . Horn satisfiability is actually one of the "hardest" or "most expressive" problems which can be computed in polynomial time, in the sense that it is a P-complete problem.

This algorithm also allows determining a truth assignment of satisfiable Horn formulae: all variables contained in a unit clause are set to the value satisfying that unit clause; all other literals are set to false. The resulting assignment is the minimal model of the Horn formula, that is, the assignment having a minimal set of variables assigned to true, where comparison is made using set containment.

Using a linear algorithm for unit propagation, the algorithm is linear in the size of the formula.

It is logical to wonder if Horn-SAT can be used to prove that P=NP, by converting any SAT problem to a Horn-SAT problem and then solving it in polynomial time. The problem with this is two-fold. First, transforming a SAT problem to a Horn-SAT problem takes exponential time. Second, the resultant transformation is exponential in length.

• Unit propagation
• Boolean satisfiability problem
• 2-satisfiability

This mathematical logic-related article is a stub. You can help Wikipedia by expanding it.