Summary
This paper shows that figuring out whether there is another largest group of conditions that can all be true at the same time in a special kind of logic problem called a Horn expression is very hard. The authors demonstrate that this task is as difficult as the hardest problems in a class called NP-complete. Because of this, there is no fast method that can efficiently list all such largest groups unless a widely believed assumption about computational difficulty is wrong.
What this means in practice
- •For software verification teams: Avoid relying on efficient enumeration of maximal satisfiable subsets when analyzing Horn clauses due to proven computational limits.
- •For automated reasoning engineers: Design algorithms that circumvent full enumeration for Horn expressions since the problem is shown to be computationally infeasible.
A theory result. No direct application yet.
Abstract
We show that, given a Horn expression and a family of inclusion-wise maximal satisfiable subsets of its clauses, deciding whether there exists another maximal satisfiable subset is NP-complete. As a consequence, unless P=NP, there is no output-polynomial time algorithm enumerating the maximal satisfiable subformulas of a Horn expression.