×

Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets. (English) Zbl 1029.68079

Summary: We study the problem of (efficiently) deleting such clauses from conjunctive normal forms (clause-sets) which cannot contribute to any proof of unsatisfiability. For that purpose we introduce the notion of an autarky system \(\mathcal A\), which detects deletion of superfluous clauses from a clause-set \(F\) and yields a canonical normal form \(N_{\mathcal A}(F)\subseteq F\). Clause-sets where no clauses can be deleted are called \(\mathcal A\)-lean, a natural weakening of minimally unsatisfiable clause-sets opening the possibility for combinatorial approaches and including also satisfiable instances. Three special examples for autarky systems are considered: general autarkies, linear autarkies (based on linear programming) and matching autarkies (based on matching theory). We give new characterizations of (“absolutely”) lean clause-sets in terms of qualitative matrix analysis, while matching lean clause-sets are characterized in terms of deficiency (the difference between the number of clauses and the number of variables), by having a cyclic associated transversal matroid, and also in terms of fully indecomposable matrices. Finally we discuss how to obtain polynomial time satisfiability decision for clause-sets with bounded deficiency, and we make a few steps towards a general theory of autarky systems.

MSC:

68Q25 Analysis of algorithms and problem complexity

Software:

Mosek
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Aharoni, R.; Linial, N., Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas, J. Combin. Theory Ser. A, 43, 196-204 (1986) · Zbl 0611.05045
[2] Aigner, M., Kombinatorik; Teil II: Matroide und Transversaltheorie (1976), Springer: Springer Berlin · Zbl 0373.05002
[3] E.D. Andersen, K.D. Andersen, The XPRESS interior point optimizer for linear programming: an implementation of the homogeneous algorithm, in: J.B.G. Frenk, C. Roos, T. Terlaky, S. Zhang (Eds.), High Performance Optimization Techniques, Proceedings of the HPOPT-II Conference, 1997.; E.D. Andersen, K.D. Andersen, The XPRESS interior point optimizer for linear programming: an implementation of the homogeneous algorithm, in: J.B.G. Frenk, C. Roos, T. Terlaky, S. Zhang (Eds.), High Performance Optimization Techniques, Proceedings of the HPOPT-II Conference, 1997. · Zbl 1028.90022
[4] A. Bachem, W. Kern, Linear Programming Duality: An Introduction to Oriented Matroids, Universitext. Springer, Berlin, 1992.; A. Bachem, W. Kern, Linear Programming Duality: An Introduction to Oriented Matroids, Universitext. Springer, Berlin, 1992. · Zbl 0757.90050
[5] Boros, E.; Crama, Y.; Hammer, P. L., Polynomial-time inference of all valid implications for Horn and related formulae, Ann. Math. Artif. Intell., 1, 21-32 (1990) · Zbl 0878.68105
[6] Boros, E.; Crama, Y.; Hammer, P. L.; Saks, M., A complexity index for satisfiability problems, SIAM J. Comput., 23, 1, 45-49 (1994) · Zbl 0793.90038
[7] Boros, E.; Hammer, P. L.; Sun, X., Recognition of q-Horn formulae in linear time, Discrete Appl. Math., 55, 1-13 (1994) · Zbl 0821.68109
[8] Brualdi, R. A.; Ryser, H. J., Combinatorial Matrix Theory, Encyclopedia of Mathematics and its Applications, Vol. 39 (1991), Cambridge University: Cambridge University Cambridge · Zbl 0746.05002
[9] Brualdi, R. A.; Shader, B. L., Matrices of Sign-Solvable Linear Systems, Cambridge Tracts in Mathematics, Vol. 116 (1995), Cambridge University: Cambridge University Cambridge · Zbl 0833.15002
[10] Kleine Büning, H., On generalized Horn formulas and \(k\)-resolution, Theoret. Comput. Sci., 116, 405-413 (1993) · Zbl 0786.03009
[11] Kleine Büning, H., An upper bound for minimal resolution refutations, (Gottlob, G.; Grandjean, E.; Seyr, K., Computer Science Logic 12th International Workshop, CSL’98. Computer Science Logic 12th International Workshop, CSL’98, Lecture Notes in Computer Science, Vol. 1584 (1999), Springer: Springer Berlin), 171-178 · Zbl 0934.03015
[12] Kleine Büning, H., On subclasses of minimal unsatisfiable formulas, Discrete Appl. Math., 107, 83-98 (2000) · Zbl 0965.03016
[13] H. Kleine Büning, X. Zhao, The complexity of read-once resolution, Ann. Math. Artif. Intell., to appear.; H. Kleine Büning, X. Zhao, The complexity of read-once resolution, Ann. Math. Artif. Intell., to appear. · Zbl 1015.68081
[14] Dalal, M.; Etherington, D. W., A hierarchy of tractable satisfiability problems, Inform. Process. Lett., 44, 173-180 (1992) · Zbl 0774.68057
[15] Davydov, G. V.; Davydova, I. V., Tautologies and positive solvability of linear homogeneous systems, Ann. Pure Appl. Logic, 57, 27-43 (1992) · Zbl 0764.15001
[16] Davydov, G. V.; Davydova, I. V.; Kleine Büning, H., An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF, Ann. Math. Artif. Intell., 23, 229-245 (1998) · Zbl 0913.68090
[17] Davydov, G. V.; Davydova, I. M., Number representations of satisfiability, J. Math. Sci., 98, 4, 464-477 (2000), (A Translation of Selected Russian-Language Serial Publications in Mathematics)
[18] Fleischner, H.; Kullmann, O.; Szeider, S., Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference, Theoret. Comput. Sci., 289, 1, 503-516 (2002) · Zbl 1061.68072
[19] H. Fleischner, S. Szeider, Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference, Technical Report TR00-049, Electronic Colloquium on Computational Complexity (ECCC), July 2000.; H. Fleischner, S. Szeider, Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference, Technical Report TR00-049, Electronic Colloquium on Computational Complexity (ECCC), July 2000. · Zbl 1061.68072
[20] T. Fliti, G. Reynaud, Sizes of minimally unsatisfiable conjunctive normal forms, Faculté des Sciences de Luminy, Dpt. Mathematique-Informatique, 13288 Marseille, France, November 1994.; T. Fliti, G. Reynaud, Sizes of minimally unsatisfiable conjunctive normal forms, Faculté des Sciences de Luminy, Dpt. Mathematique-Informatique, 13288 Marseille, France, November 1994.
[21] Franco, J.; Gelder, A. V., A perspective on certain polynomial time solvable classes of satisfiability, Discrete Appl. Math., 125, 2,3, 177-214 (2003) · Zbl 1012.68085
[22] Gallo, G.; Scutellà, M. G., Polynomially solvable satisfiability problems, Inform. Process. Lett., 29, 221-227 (1988) · Zbl 0662.68037
[23] Van Gelder, A., Autarky pruning in propositional model elimination reduces failure redundancy, J. Autom. Reason., 23, 2, 137-193 (1999) · Zbl 0939.68108
[24] Gordan, P., Ueber die Auflösung linearer Gleichungen mit reellen Coeffizienten, Mathemat. Annal., 6, 23-28 (1873) · JFM 05.0095.01
[25] Hirsch, E., New worst-case upper bounds for SAT, J. Autom. Reason., 24, 4, 397-420 (2000) · Zbl 0960.03009
[26] G. Huet, Confluent reductions: Abstract properties and applications to term rewriting systems, in: 18th Annual Symposium on Foundations of Computer Science, IEEE, New York, 1977, pp. 30-45.; G. Huet, Confluent reductions: Abstract properties and applications to term rewriting systems, in: 18th Annual Symposium on Foundations of Computer Science, IEEE, New York, 1977, pp. 30-45.
[27] H. Kautz, D. McAllester, B. Selman, Encoding plans in propositional logic, in: Proceedings KR-96.; H. Kautz, D. McAllester, B. Selman, Encoding plans in propositional logic, in: Proceedings KR-96.
[28] H. Kautz, B. Selman, Pushing the envelope: planning, propositional logic, and stochastic search, in: Proceedings AAAI-96.; H. Kautz, B. Selman, Pushing the envelope: planning, propositional logic, and stochastic search, in: Proceedings AAAI-96. · Zbl 0979.68094
[29] H. Kautz, B. Selman, SAT-encoded logistics planning problems, From the problem collection Internet site SATLIB; see http://www.satlib.org.; H. Kautz, B. Selman, SAT-encoded logistics planning problems, From the problem collection Internet site SATLIB; see http://www.satlib.org.
[30] Klee, V.; Ladner, R.; Manber, R., Signsolvability revistied, Linear Algebra Appl., 59, 131-157 (1984) · Zbl 0543.15016
[31] O. Kullmann, Heuristics for SAT algorithms: a systematic study, in: SAT’98, March 1998. Extended abstract for the Second Workshop on the Satisfiability Problem, May 10-14, 1998, Eringerfeld, Germany.; O. Kullmann, Heuristics for SAT algorithms: a systematic study, in: SAT’98, March 1998. Extended abstract for the Second Workshop on the Satisfiability Problem, May 10-14, 1998, Eringerfeld, Germany.
[32] O. Kullmann, Heuristics for SAT algorithms: searching for some foundations, Manuscript 23pp., based on [31]http://www.cs-srv1.swan.ac.uk/ csoliver/; O. Kullmann, Heuristics for SAT algorithms: searching for some foundations, Manuscript 23pp., based on [31]http://www.cs-srv1.swan.ac.uk/ csoliver/
[33] O. Kullmann, 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.; O. Kullmann, 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.
[34] Kullmann, O., New methods for 3-SAT decision and worst-case analysis, Theoret. Comput. Sci., 223, 1-2, 1-72 (1999) · Zbl 0930.68066
[35] Kullmann, O., On a generalization of extended resolution, Discrete Appl. Math., 96-97, 1-3, 149-176 (1999) · Zbl 0941.68126
[36] O. Kullmann, An application of matroid theory to the SAT problem, in: 15th Annual IEEE Conference of Computational Complexity, IEEE Computer Society, Silver Spring, MD, July 2000, pp. 116-124. See also TR00-018, Electronic Colloquium on Computational Complexity (ECCC), March 2000.; O. Kullmann, An application of matroid theory to the SAT problem, in: 15th Annual IEEE Conference of Computational Complexity, IEEE Computer Society, Silver Spring, MD, July 2000, pp. 116-124. See also TR00-018, Electronic Colloquium on Computational Complexity (ECCC), March 2000.
[37] Kullmann, O., Investigations on autark assignments, Discrete Appl. Math., 107, 99-137 (2000) · Zbl 0965.03018
[38] O. Kullmann, The SAT solver OKsolver, implemented in C. Available at http://cs-svr1.swan.ac.uk/ csoliver/OKsolver.html; O. Kullmann, The SAT solver OKsolver, implemented in C. Available at http://cs-svr1.swan.ac.uk/ csoliver/OKsolver.html
[39] O. Kullmann, Some general considerations on heuristics, and the SAT solver “OKsolver”, September 2000, in preparation.; O. Kullmann, Some general considerations on heuristics, and the SAT solver “OKsolver”, September 2000, in preparation.
[40] O. Kullmann, On the use of autarkies for satisfiability decision, in: H. Kautz, B. Selman (Eds.), LICS 2001 Workshop on Theory and Applications of Satisfiability Testing (SAT 2001), Electronic Notes in Discrete Mathematics (ENDM), Vol. 9, Elsevier Science, Amsterdam, June 2001.; O. Kullmann, On the use of autarkies for satisfiability decision, in: H. Kautz, B. Selman (Eds.), LICS 2001 Workshop on Theory and Applications of Satisfiability Testing (SAT 2001), Electronic Notes in Discrete Mathematics (ENDM), Vol. 9, Elsevier Science, Amsterdam, June 2001. · Zbl 0990.90545
[41] O. Kullmann, H. Luckhardt, Deciding propositional tautologies: Algorithms and their complexity. Preprint, 82pp; the ps-file can be obtained at http://cs-svr1.swan.ac.uk/ csoliver; O. Kullmann, H. Luckhardt, Deciding propositional tautologies: Algorithms and their complexity. Preprint, 82pp; the ps-file can be obtained at http://cs-svr1.swan.ac.uk/ csoliver
[42] O. Kullmann, H. Luckhardt, Algorithms for SAT/TAUT decision based on various measures, Preprint, 71pp; the ps-file can be obtained from http://cs-svr1.swan.ac.uk/ csoliver; O. Kullmann, H. Luckhardt, Algorithms for SAT/TAUT decision based on various measures, Preprint, 71pp; the ps-file can be obtained from http://cs-svr1.swan.ac.uk/ csoliver
[43] Lee, G.-Y.; Shader, B. L., Sign-consistency and solvability of constrained linear systems, The Electron. J. Linear Algebra, 4, 1-18 (1998), http://math.technion.ac.il/iic/ela. · Zbl 0912.15004
[44] Lovász, L.; Plummer, M. D., Matching Theory, Mathematics Studies, Vol. 121 (1986), North-Holland: North-Holland Amsterdam · Zbl 0618.05001
[45] H. Luckhardt, Obere Komplexitätsschranken für TAUT-Entscheidungen, in: Frege Conference 1984, Schwerin, Akademie-Verlag, Berlin, 1984, pp. 331-337.; H. Luckhardt, Obere Komplexitätsschranken für TAUT-Entscheidungen, in: Frege Conference 1984, Schwerin, Akademie-Verlag, Berlin, 1984, pp. 331-337.
[46] Monien, B.; Speckenmeyer, E., Solving satisfiability in less than \(2^n\) steps, Discrete Appl. Math., 10, 287-295 (1985) · Zbl 0603.68092
[47] Newman, M. H.A., On theories with a combinatorial definition of “equivalence”, Ann. Math., 43, 223-243 (1942) · Zbl 0060.12501
[48] Okushi, F., Parallel cooperative propositional theorem proving, Ann. Math. Artif. Intell., 26, 59-85 (2000) · Zbl 0940.68120
[49] Oxley, J. G., Matroid Theory (1992), Oxford University Press: Oxford University Press Oxford
[50] Papadimitriou, C. H.; Wolfe, D., The complexity of facets resolved, J. Comput. System Sci., 37, 2-13 (1988) · Zbl 0655.68041
[51] Schrijver, A., Theory of Linear and Integer Programming (1986), Wiley: Wiley Chichester · Zbl 0665.90063
[52] Shaohan, M.; Dongmin, L., A polynomial-time algorithm for reducing the number of variables in MAX SAT problem, Sci. China (Series E), 40, 3, 301-311 (1997) · Zbl 0881.68086
[53] Singer, J.; Gent, I. P.; Smaill, A., Backbone fragility and the local search cost peak, J. Artif. Intell. Res., 12, 235-270 (2000) · Zbl 0947.68044
[54] Szeider, S., NP-completeness of refutability by literal-once resolution, (Gore, R.; Leitsch, A.; Nipkow, T., IJCAR 2001, Proceedings of the International Joint Conference on Automated Reasoning. IJCAR 2001, Proceedings of the International Joint Conference on Automated Reasoning, Lecture Notes in Artificial Intelligence, Vol. 2083 (2001), Springer: Springer Berlin), 168-181 · Zbl 0988.03020
[55] J. Torán, July 2000. Personal communication.; J. Torán, July 2000. Personal communication.
[56] G.S. Tseitin, On the complexity of derivation in propositional calculus, in: A.O. Slisenko (Ed.), Seminars in Mathematics, Vol. 8. V.A. Steklov Mathematical Institute, Leningrad, 1968. English translation: Studies in Mathematics and Mathematical Logic, Part II, 1970, pp. 115-125.; G.S. Tseitin, On the complexity of derivation in propositional calculus, in: A.O. Slisenko (Ed.), Seminars in Mathematics, Vol. 8. V.A. Steklov Mathematical Institute, Leningrad, 1968. English translation: Studies in Mathematics and Mathematical Logic, Part II, 1970, pp. 115-125. · Zbl 0197.00102
[57] van Maaren, H., A short note on some tractable cases of the satisfiability problem, Inform. Comput., 158, 2, 125-130 (2000) · Zbl 1046.68542
[58] van Maaren, H.; Warners, J., Solving satisfiability problems using elliptic approximations—effective branching rules, Discrete Appl. Math., 107, 241-259 (2000) · Zbl 0965.68026
[59] Xishun, Z.; Decheng, D., Two tractable subclasses of minimal unsatisfiable formulas, Sci. 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.