We consider the problem of finding the smallest proof of unsatisfiability of a 2CNF formula. In particular, we look at Resolution refutations and at minimum unsatisfiable subsets of the clauses of the CNF. We give a characterization of minimum tree-like Resolution refutations that explains why, to find them, it is not sufficient to find shortest paths in the implication graph of the CNF. The characterization allows us to develop an efficient algorithm for finding a smallest tree-like refutation and to show that the size of such a refutation is a good approximation to the size of the smallest general refutation. We also give a polynomial time dynamic programming algorithm for finding a smallest unsatisfiable subset of the clauses of a 2CNF. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Buresh-Oppenheim, J., & Mitchell, D. (2006). Minimum witnesses for unsatisfiable 2CNFs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4121 LNCS, pp. 42–47). Springer Verlag. https://doi.org/10.1007/11814948_6
Mendeley helps you to discover research relevant for your work.