Abstract
DP-reduction \(F \rightsquigarrow DP_{v}(F)\), applied to a clause-set F and a variable v, replaces all clauses containing v by their resolvents (on v). A basic case, where the number of clauses is decreased (i.e., c(DP v (F)) < c(F)), is singular DP-reduction (sDP-reduction), where v must occur in one polarity only once. For minimally unsatisfiable \(F \in \mathcal{M\hspace{0.8pt}U}\), sDP-reduction produces another \(F' := DP_{v}(F) \in \mathcal{M\hspace{0.8pt}U}\) with the same deficiency, that is, δ(F′) = δ(F); recall δ(F) = c(F) − n(F), using n(F) for the number of variables. Let sDP(F) for \(F \in \mathcal{M\hspace{0.8pt}U}\) be the set of results of complete sDP-reduction for F; so F′ ∈ sDP(F) fulfil \(F' \in \mathcal{M\hspace{0.8pt}U}\), are nonsingular (every literal occurs at least twice), and we have δ(F′) = δ(F). We show that for \(F \in \mathcal{M\hspace{0.8pt}U}\) all complete reductions by sDP must have the same length, establishing the singularity index of F. In other words, for F′, F′′ ∈ sDP(F) we have n(F′) = n(F′′). In general the elements of sDP(F) are not even (pairwise) isomorphic. Using the fundamental characterisation by Kleine Büning, we obtain as application of the singularity index, that we have confluence modulo isomorphism (all elements of sDP(F) are pairwise isomorphic) in case δ(F) = 2. In general we prove that we have confluence (i.e., |sDP(F) = 1) for saturated F (i.e., \(F \in \mathcal{S}\mathcal{M\hspace{0.8pt}U} \)). More generally, we show confluence modulo isomorphism for eventually saturated F, that is, where we have \(sDP(F) \subseteq \mathcal{S}\mathcal{M\hspace{0.8pt}U} \), yielding another proof for confluence modulo isomorphism in case of δ(F) = 2.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aharoni, R., Linial, N.: Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas. Journal of Combinatorial Theory A 43, 196–204 (1986)
Davydov, G., Davydova, I., Büning, H.K.: An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF. Annals of Mathematics and Artificial Intelligence 23, 229–245 (1998)
Fleischner, H., Kullmann, O., Szeider, S.: Polynomial–time recognition of minimal unsatisfiable formulas with fixed clause–variable difference. Theoretical Computer Science 289(1), 503–516 (2002)
Fliti, T., Reynaud, G.: Sizes of minimally unsatisfiable conjunctive normal forms. Faculté des Sciences de Luminy, Dpt. Mathematique-Informatique, 13288 Marseille, France (November 1994)
Büning, H.K.: On subclasses of minimal unsatisfiable formulas. Discrete Applied Mathematics 107, 83–98 (2000)
Büning, H.K., Kullmann, O.: Minimal unsatisfiability and autarkies. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, ch. 11, pp. 339–401. IOS Press (February 2009)
Kullmann, O.: Obere und untere Schranken für die Komplexität von aussagenlogischen Resolutionsbeweisen und Klassen von SAT-Algorithmen. Master’s thesis, Johann Wolfgang Goethe-Universität Frankfurt am Main (Upper and lower bounds for the complexity of propositional resolution proofs and classes of SAT algorithm; Diplomarbeit am Fachbereich Mathematik) (April 1992) (in German)
Kullmann, O.: An application of matroid theory to the SAT problem. In: Fifteenth Annual IEEE Conference on Computational Complexity, pp. 116–124. IEEE Computer Society (July 2000)
Kullmann, O.: Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets. Discrete Applied Mathematics 130, 209–249 (2003)
Kullmann, O.: Constraint satisfaction problems in clausal form I: Autarkies and deficiency. Fundamenta Informaticae 109(1), 27–81 (2011)
Kullmann, O.: Constraint satisfaction problems in clausal form II: Minimal unsatisfiability and conflict structure. Fundamenta Informaticae 109(1), 83–119 (2011)
Kullmann, O., Luckhardt, H.: Deciding propositional tautologies: Algorithms and their complexity. Preprint, 82 pages; the ps-file can be obtained (January 1997), http://cs.swan.ac.uk/~csoliver/Artikel/tg.ps
Kullmann, O., Luckhardt, H.: Algorithms for SAT/TAUT decision based on various measures. Preprint, 71 pages; the ps-file can be obtained (February 1999), http://cs.swan.ac.uk/~csoliver/Artikel/TAUT.ps
Kullmann, O., Zhao, X.: On Variables with Few Occurrences in Conjunctive Normal Forms. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 33–46. Springer, Heidelberg (2011)
Kullmann, O., Zhao, X.: On Davis-Putnam reductions for minimally unsatisfiable clause-sets. Technical Report arXiv:1202.2600v3 [cs.DM], arXiv (May 2012)
Marques-Silva, J.: Computing minimally unsatisfiable subformulas: State of the art and future directions. Journal of Multiple-Valued Logic and Soft Computing (to appear, 2012)
Szeider, S.: Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable. Journal of Computer and System Sciences 69(4), 656–674 (2004)
Zhao, X., Decheng, D.: Two tractable subclasses of minimal unsatisfiable formulas. Science in China (Series A) 42(7), 720–731 (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kullmann, O., Zhao, X. (2012). On Davis-Putnam Reductions for Minimally Unsatisfiable Clause-Sets. In: Cimatti, A., Sebastiani, R. (eds) Theory and Applications of Satisfiability Testing – SAT 2012. SAT 2012. Lecture Notes in Computer Science, vol 7317. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31612-8_21
Download citation
DOI: https://doi.org/10.1007/978-3-642-31612-8_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-31611-1
Online ISBN: 978-3-642-31612-8
eBook Packages: Computer ScienceComputer Science (R0)