arXiv:2611.14471 · v1

A note on the intractability of enumerating the maximal satisfiable subformulas of a Horn expression

首次提交 2026-11-11 02:34

版本更新 2026-11-11 02:34

雷达观测 2026-11-11 13:07

摘要

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.

作者备注：6 pages