Anzeige
Erschienen in:
2006 | OriginalPaper | Buchkapitel
Variable Minimal Unsatisfiability
verfasst von : Zhenyu Chen, Decheng Ding
Erschienen in: Theory and Applications of Models of Computation
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
In this paper, we present variable minimal unsatisfiability (VMU), which is a generalization of minimal unsatisfiability (MU). A characterization of a VMU formula
F
is that every variable of
F
is used in every resolution refutation of
F
. We show that the class of VMU formulas is
D
P
-complete. For fixed deficiency (the difference of the number of clauses and the number of variables), the VMU formulas can be solved in polynomial time. Furthermore, we investigate more subclasses of VMU formulas. Although the theoretic results on VMU and MU are similar, some observations are shown that the extraction of VMU may be more practical than MU in some cases.