Generalizations of matched CNF formulas |
| |
Authors: | Stefan Szeider |
| |
Affiliation: | (1) Department of Computer Science, University of Durham, DH1 3LE Durham, UK |
| |
Abstract: | A CNF formula is called matched if its associated bipartite graph (whose vertices are clauses and variables) has a matching that covers all clauses. Matched CNF formulas are satisfiable and can be recognized efficiently by matching algorithms. We generalize this concept and cover clauses by collections of bicliques (complete bipartite graphs). It turns out that such generalization indeed gives rise to larger classes of satisfiable CNF formulas which we term biclique satisfiable. We show, however, that the recognition of biclique satisfiable CNF formulas is NP-complete, and remains NP-hard if the size of bicliques is bounded. A satisfiable CNF formula is called var-satisfiable if it remains satisfiable under arbitrary replacement of literals by their complements. Var-satisfiable CNF formulas can be viewed as the best possible generalization of matched CNF formulas as every matched CNF formula and every biclique satisfiable CNF formula is var-satisfiable. We show that recognition of var-satisfiable CNF formulas is
P
2
P-complete, answering a question posed by Kleine Büning and Zhao. |
| |
Keywords: | SAT problem bipartite graph matched formula deficiency biclique cover NP-completeness
P
2
-completeness" target="_blank">gif" alt="Pgr" align="BASELINE" BORDER="0">
P
2
-completeness polynomial hierarchy |
本文献已被 SpringerLink 等数据库收录! |
|