Horn-satisfiability

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 $\neg l$ 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 $\neg l$ . 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.