×

On Davis-Putnam reductions for minimally unsatisfiable clause-sets. (English) Zbl 1296.03010

Summary: DP-reduction \(F\rightsquigarrow\mathrm{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(\mathrm{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{MU}\), sDP-reduction produces another \(F^\prime:=\mathrm{DP}_v(F)\in\mathcal{MU}\) with the same deficiency, that is, \(\delta(F^\prime)=\delta(F)\); recall \(\delta(F)=c(F)-n(F)\), using \(n(F)\) for the number of variables. Let \(\mathrm{sDP}(F)\) for \(F\in\mathcal{MU}\) be the set of results of complete sDP-reduction for \(F\); so \(F^\prime\in\mathrm{sDP}(F)\) fulfil \(F^\prime\in\mathcal{MU}\), are nonsingular (every literal occurs at least twice), and we have \(\delta(F^\prime)=\delta(F)\). We show that for \(F\in\mathcal{MU}\) all complete reductions by sDP must have the same length, establishing the singularity index of \(F\). In other words, for \(F^\prime,F^{\prime\prime}\in\mathrm{sDP}(F)\) we have \(n(F^\prime)=n(F^{\prime\prime})\). In general the elements of \(\mathrm{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 \(\mathrm{sDP}(F)\) are pairwise isomorphic) in case \(\delta(F)=2\). In general we prove that we have confluence (i.e., \(|\mathrm{sDP}(F)|=1\)) for saturated \(F\) (i.e., \(F\in\mathcal{SMU}\)). More generally, we show confluence modulo isomorphism for eventually saturated \(F\), that is, where we have \(\mathrm{sDP}(F)\subseteq\mathcal{SMU}\), yielding another proof for confluence modulo isomorphism in case of \(\delta(F)=2\).

MSC:

03B35 Mechanization of proofs and logical operations

Software:

MiniSat; JBool; NiVER
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Aharoni, Ron; Linial, Nathan, Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas, Journal of Combinatorial Theory, A, 43, 196-204 (1986) · Zbl 0611.05045
[2] Crama, Yves; Hammer, Peter L., (Boolean Functions: Theory, Algorithms, and Applications. Boolean Functions: Theory, Algorithms, and Applications, Encyclopedia of Mathematics and Its Applications, vol. 142 (2011), Cambridge University Press) · Zbl 1237.06001
[3] Davis, Martin; Putnam, Hilary, A computing procedure for quantification theory, Journal of the ACM, 7, 201-215 (1960) · Zbl 0212.34203
[4] Davydov, Gennady; Davydova, Inna; Kleine Büning, Hans, An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF, Annals of Mathematics and Artificial Intelligence, 23, 229-245 (1998) · Zbl 0913.68090
[5] Eén, Niklas; Biere, Armin, Effective preprocessing in SAT through variable and clause elimination, (Bacchus, Fahiem; Walsh, Toby, Theory and Applications of Satisfiability Testing 2005. Theory and Applications of Satisfiability Testing 2005, Lecture Notes in Computer Science, vol. 3569 (2005), Springer: Springer Berlin), 61-75 · Zbl 1128.68463
[6] Fleischner, Herbert; Kullmann, Oliver; Szeider, Stefan, Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference, Theoretical Computer Science, 289, 1, 503-516 (2002) · Zbl 1061.68072
[8] Franco, John, Elimination of infrequent variables improves average case performance of satisfiability algorithms, SIAM Journal on Computing, 20, 6, 1119-1127 (1991) · Zbl 0738.68041
[9] Van Gelder, Allen, Combining preorder and postorder resolution in a satisfiability solver, Electronic Notes in Discrete Mathematics (ENDM), 9, June, 115-128 (2001) · Zbl 0990.90534
[10] Henschen, Lawrence J.; Wos, Lawrence, Unit refutations and Horn sets, Journal of the Association for Computing Machinery, 21, 4, 590-605 (1974) · Zbl 0296.68093
[11] Kleine Büning, Hans, On subclasses of minimal unsatisfiable formulas, Discrete Applied Mathematics, 107, 83-98 (2000) · Zbl 0965.03016
[12] Kleine Büning, Hans; Kullmann, Oliver, Minimal unsatisfiability and autarkies, (Biere, Armin; Heule, Marijn J. H.; van Maaren, Hans; Walsh, Toby, Handbook of Satisfiability. Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185 (2009), IOS Press), 339-401, (Chapter 11)
[14] Kullmann, Oliver, Investigating a general hierarchy of polynomially decidable classes of CNF’s based on short tree-like resolution proofs, Technical Report TR99-041, Electronic Colloquium on Computational Complexity (ECCC) (October 1999)
[15] Kullmann, Oliver, An application of matroid theory to the SAT problem, (Fifteenth Annual IEEE Conference on Computational Complexity (2000) (July 2000), IEEE Computer Society), 116-124
[16] Kullmann, Oliver, Lean clause-sets: generalizations of minimally unsatisfiable clause-sets, Discrete Applied Mathematics, 130, 209-249 (2003) · Zbl 1029.68079
[17] Kullmann, Oliver, Upper and lower bounds on the complexity of generalised resolution and generalised constraint satisfaction problems, Annals of Mathematics and Artificial Intelligence, 40, 3-4, 303-352 (2004) · Zbl 1081.68032
[18] Kullmann, Oliver, Constraint satisfaction problems in clausal form I: autarkies and deficiency, Fundamenta Informaticae, 109, 1, 27-81 (2011) · Zbl 1242.68289
[19] Kullmann, Oliver, Constraint satisfaction problems in clausal form II: minimal unsatisfiability and conflict structure, Fundamenta Informaticae, 109, 1, 83-119 (2011) · Zbl 1242.68290
[24] Kullmann, Oliver; Zhao, Xishun, On Davis-Putnam reductions for minimally unsatisfiable clause-sets, (Cimatti, Alessandro; Sebastiani, Roberto, Theory and Applications of Satisfiability Testing - SAT 2012. Theory and Applications of Satisfiability Testing - SAT 2012, Lecture Notes in Computer Science, vol. LNCS 7317 (2012), Springer), 270-283 · Zbl 1273.03050
[25] Kullmann, Oliver; Zhao, Xishun, On Davis-Putnam reductions for minimally unsatisfiable clause-sets, Technical Report [cs.DM], arXiv (December 2012)
[26] Li, Chu Min; Manyá, Felip; Mohamedou, Nouredine Ould; Planes, Jordi, Resolution-based lower bounds in MaxSAT, Constraints, 15, 4, 456-484 (2010) · Zbl 1208.68204
[27] Marques-Silva, Joao, Computing minimally unsatisfiable subformulas: state of the art and future directions, Journal of Multiple-Valued Logic and Soft Computing, 19, 1-3, 163-183 (2012) · Zbl 1394.68359
[29] (Sakallah, Karem A.; Simon, Laurent, Theory and Applications of Satisfiability Testing - SAT 2011. Theory and Applications of Satisfiability Testing - SAT 2011, Lecture Notes in Computer Science, vol. LNCS 6695 (2011), Springer) · Zbl 1215.68023
[30] Subbarayan, Sathiamoorthy; Pradhan, Dhiraj K., NiVER: non-increasing variable elimination resolution for preprocessing SAT instances, (Hoos, Holger H.; Mitchell, David G., The Seventh International Conference on Theory and Applications of Satisfiability Testing. The Seventh International Conference on Theory and Applications of Satisfiability Testing, Lecture Notes in Computer Science, vol. 3542 (2005), Springer: Springer Berlin), 276-291 · Zbl 1122.68618
[31] Szeider, Stefan, Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable, Journal of Computer and System Sciences, 69, 4, 656-674 (2004) · Zbl 1108.68065
[32] Zhao, Xishun; Decheng, Ding, Two tractable subclasses of minimal unsatisfiable formulas, Science in China (Series A), 42, 7, 720-731 (1999) · Zbl 0937.03009
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.