On the complexity of the maximum satisfiability problem for Horn formulas (Q1099168)

Some results concerning the corresponding complexity of algorithms which check the partial consistency of logic databases are presented. It is proved that even when some quite strong restrictions are imposed, the maximum satisfiability (MAX-SAT) problem for Horn formulas is NP- complete. Hence, when the Horn formula is either quadratic or all its clauses have precisely one complemented variable, it is shown that MAX- SAT is still an NP-complete problem. For elementary Horn formulas, the MAX-SAT problem can be solved by a polynomial-time algorithm, where an elementary Horn formula is a quadratic Horn formula such that every nonunit clause has exactly one positive literal.