Constraint Satisfaction Problems in Clausal Form I: Autarkies and Deficiency

Kullmann, O.

Artykuł - szczegóły

Tytuł artykułu

Constraint Satisfaction Problems in Clausal Form I: Autarkies and Deficiency

Autorzy

Kullmann O.

Wybrane pełne teksty z tego czasopisma

https://fi.episciences.org/

Identyfikatory

Warianty tytułu

Języki publikacji

Abstrakty

We consider the problem of generalising boolean formulas in conjunctive normal form by allowing non-boolean variables, with the goal of maintaining combinatorial properties. Requiring that a literal involves only a single variable, the most general form of literals are the wellknown "signed literals", corresponding to unary constraints in CSP. However we argue that only the restricted form of "negative monosigned literals" and the resulting generalised clause-sets, corresponding to "sets of no-goods" in the AI literature, maintain the essential properties of boolean conjunctive normal forms. In this first part of a mini-series of two articles, we build up a solid foundation for (generalised) clause-sets, including the notion of autarky systems, the interplay between autarkies and resolution, and basic notions of (DP-)reductions. As a basic combinatorial parameter of generalised clause-sets we introduce the (generalised) notion of deficiency, which in the boolean case is the difference between the number of clauses and the number of variables. Autarky theory plays a fundamental role here, and we concentrate especially on matching autarkies (based on matching theory). A natural task is to determine the structure of (matching) lean clause-sets, which do not admit non-trivial (matching) autarkies. A central result is the computation of the lean kernel (the largest lean subset) of a (generalised) clause-set in polynomial time for bounded maximal deficiency.

Słowa kluczowe

autarkies deficiency satisfiability problem constraint satisfaction problems generalised clause-sets signed formulas non-boolean variables polynomial time matching autarkies lean clause-sets

Wydawca

IOS Press

Czasopismo

Fundamenta Informaticae

Rocznik

2011

Tom

Vol. 109, nr 1

Strony

27--81

Opis fizyczny

Bibliogr. 72 poz.

Twórcy

autor

Kullmann O.

Computer Science Department, Swansea University, Swansea, SA2 8PP, United Kingdom, O.Kullmann@Swansea.ac.uk

Bibliografia

[1] Aharoni, R., Linial, N.: Minimal Non-Two-Colorable Hypergraphs and Minimal Unsatisfiable Formulas, Journal of Combinatorial Theory, A 43, 1986, 196-204.
[2] Ahmed, T.: Some new van der Waerden numbers and some van der Waerden-type numbers, INTEGERS: Electronic Journal of Combinatorial Number Theory, 9, 2009, 65-76.
[3] Ahmed, T.: Two new van der Waerden numbers: w(2;3,17) and w(2;3,18), INTEGERS: Electronic Journal of Combinatorial Number Theory, 10(A32), 2010, 369-377.
[4] Ahmed, T., Kullmann, O., Snevily, H.: On the van der Waerden numbers w(2; 3, t), Technical Report arXiv:1102.5433v1 [math.CO], arXiv, February 2011.
[5] Ansótegui, C., Béjar, R., Cabiscol, A., Li, C. M., Manyá, F.: Resolution Methods for Many-Valued CNF Formulas, Fifth International Symposium on Theory and Applications of Satisfiability Testing (J. Franco, H. Kautz, H. Kleine Büning, H. van Maaren, B. Selman, E. Speckenmeyer, Eds.), 2002, University of Cincinnati (USA), May 6, 2002 to May 9, 2002.
[6] Ansótegui, C., Bonet, M. L., Levy, J., Manyà, F.: Mapping CSP into Many-Valued SAT, in: Marques-Silva and Sakallah [60], 10-15, ISBN 978-3-540-72787-3.
[7] Ansótegui, C., Manyà, F.: Mapping Problems with Finite-Domain Variables to Problems with Boolean Variables, in: Hoos and Mitchell [27], 1-15, ISBN 3-540-27829-X.
[8] Apt, K. R.: Principles of Constraint Programming, Cambridge University Press, 2003, ISBN 0 521 82583 0.
[9] Baker, A. B.: Intelligent Backtracking on Constraint Satisfaction Problems: Experimental and Theoretical Results, Ph.D. Thesis, University of Oregon, March 1995, The ps-file can be down loaded using the URL http://www.cirl.uoregon.edu/baker/thesis.ps.gz.
[10] Beckert, B., Hähnle, R., Manyà, F.: The SAT Problem of Signed CNF Formulas, in: Labelled Deduction (D. Basin, M. D'Agostino, D. Gabbay, S. Matthews, L. Vigano, Eds.), vol. 17 of Applied Logic Series, Kluwer, Dordrecht, 2000, 61-82, ISBN 0-7923-6237-3.
[11] Biere, A., Heule, M. J., van Maaren, H., Walsh, T., Eds.: Handbook of Satisfiability, vol. 185 of Frontiers in Artificial Intelligence and Applications, IOS Press, February 2009, ISBN 978-1-58603-929-5.
[12] Creignou, N., Daudé, H.: Generalized satisfiability problems: minimal elements and phase transitions, Theoretical Computer Science, 302, 2003, 417-430.
[13] Davydov, G., Davydova, I., Kleine Büning, H.: An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF, Annals of Mathematics and Artificial Intelligence, 23, 1998, 229-245.
[14] Dechter, R.: Constraint Processing, Morgan Kaufmann, San Francisco, 2003, ISBN 1-55860-890-7; QA76.612.D43 2003.
[15] Dransfield, M. R., Liu, L., Marek, V. W., Truszczy´nski, M.: Satisfiability and computing van der Waerden Numbers, The Electronic Journal of Combinatorics, 11(#R41), 2004.
[16] Duchet, P.: Hypergraphs, in: Handbook of Combinatorics, Volume 1 (R. L. Graham,M. Gr¨otschel, L. Lovász, Eds.), chapter 7, North-Holland, Amsterdam, 1995, 381-432, ISBN 0-444-82346-8;QA164.H33 1995.
[17] Fleischner, H., Kullmann, O., Szeider, S.: Polynomial-Time Recognition ofMinimal Unsatisfiable Formulas with Fixed Clause-Variable Difference, Theoretical Computer Science, 289(1), November 2002, 503-516.
[18] Fleischner, H., Szeider, S.: Polynomial-Time Recognition of Minimal Unsatisfiable Formulas with Fixed Clause-Variable Difference, Technical Report TR00-049, Electronic Colloquium on Computational Complexity (ECCC), July 2000.
[19] Franco, J., Gelder, A. V.: A perspective on certain polynomial-time solvable classes of satisfiability, Discrete Applied Mathematics, 125, 2003, 177-214.
[20] Frisch, A. M., Peugniez, T. J.: Solving Non-Boolean Satisfiability Problems with Stochastic Local Search, Proceedings of the 17th International Joint Conference on Artificial Intelligence, 2001.
[21] Galesi, N., Kullmann, O.: Polynomial Time SAT Decision, HypergraphTransversals and the Hermitian Rank, in: Hoos and Mitchell [27], 89-104, ISBN 3-540-27829-X.
[22] Gelder, A. V.: Autarky Pruning in PropositionalModel Elimination Reduces Failure Redundancy, Journal of Automated Reasoning, 23(2), 1999, 137-193.
[23] Giunchiglia, E., Tacchella, A., Eds.: Theory and Applications of Satisfiability Testing 2003, vol. 2919 of Lecture Notes in Computer Science, Springer, Berlin, 2004, ISBN 3-540-20851-8.
[24] Green, B., Tao, T.: The primes contain arbitrarily long arithmetic progressions, Annals of Mathematics, 167(2), 2008, 481-547.
[25] Herwig, P., Heule, M., van Lambalgen, P., van Maaren, H.: A New Method to Construct Lower Bounds for Van der Waerden Numbers, The Electronic Journal of Combinatorics, 14(#R6), 2007.
[26] Hoory, S., Szeider, S.: A note on unsatisfiable k-CNF formulas with few occurrences per variable, SIAM Journal on Discrete Mathematics, 20(2), 2006, 523-528.
[27] Hoos, H. H., Mitchell, D. G., Eds.: Theory and Applications of Satisfiability Testing 2004, vol. 3542 of Lecture Notes in Computer Science, Springer, Berlin, 2005, ISBN 3-540-27829-X.
[28] Jarvisalo, M., Biere, A., Heule, M. J.: Blocked Clause Elimination, TACAS 2010 (J. Esparza, R. Majumdar, Eds.), Lecture Notes in Computer Science (LNCS) 6015, Springer, 2010.
[29] Kleine Büning, H.: An Upper Bound for Minimal Resolution Refutations, Computer Science Logic 12th International Workshop, CSL'98 (G. Gottlob, E. Grandjean, K. Seyr, Eds.), 1584, Springer, 1999.
[30] Kleine Büning, H.: On subclasses of minimal unsatisfiable formulas, Discrete Applied Mathematics, 107, 2000, 83-98.
[31] Kleine Büning, H., Kullmann, O.: Minimal Unsatisfiability and Autarkies, in: Biere et al. [11], chapter 11, 339-401.
[32] Kleine Büning, H., Zhao, X.: On the structure of some classes of minimal unsatisfiable formulas, Discrete Applied Mathematics, 130, 2003, 185-207.
[33] Kleine Büning, H., Zhao, X.: The Complexity of Some Subclasses of Minimal Unsatisfiable Formulas, Journal on Satisfiability, Boolean Modeling and Computation, 3, 2007, 1-17.
[34] Kouril, M., Franco, J.: Resolution Tunnels for Improved SAT Solver Performance, Theory and Applications of Satisfiability Testing 2005 (F. Bacchus, T.Walsh, Eds.), 3569, Springer, Berlin, 2005, ISBN 3-540-26276-8.
[35] Kouril, M., Paul, J. L.: The van der Waerden Number W(2, 6) is 1132, Experimental Mathematics, 17(1), 2008, 53-61.
[36] Kullmann, O.: New methods for 3-SAT decision and worst-case analysis, Theoretical Computer Science, 223(1-2), July 1999, 1-72.
[37] Kullmann, O.: Restricted versions of extended resolution, The Bulletin of Symbolic Logic, 5(1), 1999, 119, Abstracts of contributed papers of the Logic Colloquium' 98, Prague, Czech Republic, August 9 - 15, 1998.
[38] Kullmann, O.: An application of matroid theory to the SAT problem, Fifteenth Annual IEEE Conference on Computational Complexity (2000), IEEE Computer Society, July 2000.
[39] Kullmann, O.: Investigations on autark assignments, Discrete Applied Mathematics, 107, 2000, 99-137.
[40] Kullmann, O.: On the use of autarkies for satisfiability decision, LICS 2001 Workshop on Theory and Applications of Satisfiability Testing (SAT 2001) (H. Kautz, B. Selman, Eds.), 9, Elsevier Science, June 2001.
[41] Kullmann, O.: Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets, Discrete Applied Mathematics, 130, 2003, 209-249.
[42] Kullmann, O.: On the conflict matrix of clause-sets, Technical Report CSR 7-2003, University of Wales Swansea, Computer Science Report Series, March 2003.
[43] Kullmann, O.: The Combinatorics of Conflicts between Clauses, in: Giunchiglia and Tacchella [23], 426-440, ISBN 3-540-20851-8.
[44] Kullmann, O.: Conflict matrices and multi-hitting clause-sets, September 2004, Extended Abstract for the Guangzhou Symposium on Satisfiability and its Applications.
[45] Kullmann, O.: Upper and Lower Bounds on the Complexity of Generalised Resolution and Generalised Constraint Satisfaction Problems, Annals of Mathematics and Artificial Intelligence, 40(3-4), March 2004, 303-352.
[46] Kullmann, O.: Constraint satisfaction problems in clausal form: Autarkies, minimal unsatisfiability, and applications to hypergraph inequalities, Complexity of Constraints (N. Creignou, P. Kolaitis, H. Vollmer, Eds.), number 06401 in Dagstuhl Seminar Proceedings, InternationalesBegegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany, 2006, ISSN 1862-4405, http://drops.dagstuhl. de/opus/volltexte/2006/803.
[47] Kullmann, O.: Polynomial Time SAT Decision for Complementation-Invariant Clause-Sets, and Sign-non-Singular Matrices, in: Marques-Silva and Sakallah [60], 314-327, ISBN 978-3-540-72787-3.
[48] Kullmann, O.: Present and Future of Practical SAT Solving, in: Complexity of Constraints: An Overview of Current Research Themes (N. Creignou, P. Kolaitis, H. Vollmer, Eds.), vol. 5250 of Lecture Notes in Computer Science (LNCS), Springer, 2008, 283-319, ISBN-10 3-540-92799-9.
[49] Kullmann, O.: The OKlibrary: Introducing a "Holistic" Research Platform for (Generalised) SAT Solving, Studies in Logic, 2(1), 2009, 20-53.
[50] Kullmann, O.: Constraint satisfaction problems in clausal form: Autarkies and minimal unsatisfiability, Technical Report TR 07-055, version 02, Electronic Colloquium on Computational Complexity (ECCC), January 2009.
[51] Kullmann, O.: Exact Ramsey Theory: Green-Tao numbers and SAT, Technical Report arXiv:1004.0653v2 [cs.DM], arXiv, April 2010.
[52] Kullmann, O.: Green-Tao numbers and SAT, Theory and Applications of Satisfiability Testing - SAT 2010 (O. Strichman, S. Szeider, Eds.), LNCS 6175, Springer, 2010, ISBN-13 978-3-642-14185-0.
[53] Kullmann, O.: Multiclique partitions of multigraphs, and conflict-regular satisfiability problems with nonboolean variables, August 2011, In preparation.
[54] Kullmann, O., Luckhardt, H.: Algorithms for SAT/TAUT decision based on various measures, December 1998, Preprint, 71 pages; the ps-file can be obtained from http://cs.swan.ac.uk/~csoliver/.
[55] Kullmann, O., Lynce, I., Marques-Silva, J.: Categorisation of clauses in conjunctive normal forms: Minimally unsatisfiable sub-clause-sets and the lean kernel, Theory and Applications of Satisfiability Testing -SAT 2006 (A. Biere, C. P. Gomes, Eds.), 4121, Springer, 2006, ISBN 3-540-37206-7.
[56] Kullmann, O., Marek, V. W., Truszczy´nski, M.: Computing autarkies and properties of the autarky monoid, October 2008, Preprint.
[57] Landman, B., Robertson, A., Culver, C.: Some New Exact van derWaerden numbers, INTEGERS: Electronic Journal of Combinatorial Number Theory, 5(2), 2005, 1-11, #A10.
[58] Lovász, L., Plummer, M. D.: Matching Theory, vol. 121 of Mathematics Studies, North-Holland, 1986.
[59] Marek, V. W.: Introduction to Mathematics of Satisfiability, Studies in Informatics, Chapman & Hall/CRC, 2009, ISBN 978-1-4398-0167-3.
[60] Marques-Silva, J., Sakallah, K. A., Eds.: Theory and Applications of Satisfiability Testing - SAT 2007, vol. 4501 of Lecture Notes in Computer Science, Springer, 2007, ISBN 978-3-540-72787-3.
[61] McKay, B. D., Radziszowski, S. P.: Subgraph Counting Identities and Ramsey Numbers, Journal of Combinatorial Theory, Series B, 69(2), 1997, 193-209.
[62] Mitchell, D. G., Hwang, J.: 2-way vs. d-way Branching for CSP, Principles and Practice of Constraint Programming - CP 2005 (P. van Beek, Ed.), 3709, Springer, 2005, ISBN 3-540-29238-1.
[63] Okushi, F.: Parallel Cooperative Propositional Theorem Proving, Annals of Mathematics and Artificial Intelligence, 26, 1999, 59-85.
[64] Prestwich, S.: Local Search on SAT-encoded Colouring Problems, in: Giunchiglia and Tacchella [23], 105-119, ISBN 3-540-20851-8.
[65] Prestwich, S.: CNF Encodings, in: Biere et al. [11], chapter 2, 75-97.
[66] Radziszowski, S. P.: Small Ramsey Numbers, The Electronic Journal of Combinatorics, 2006, Dynamic Surveys DS1, Revision 11; see http://www.combinatorics.org/Surveys.
[67] Schrijver, A.: Combinatorial Optimization, vol. A, Springer, Berlin, 2003, ISBN 3-540-44389-4; Series Algorithms and Combinatorics, no. 24.
[68] Sloan, R. H., S¨orényi, B., Turán, G.: On k-term DNF with the largest number of prime implicants, SIAM Journal on Discrete Mathematics, 21(4), 2007, 987-998.
[69] Szeider, S.: Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable, Journal of Computer and System Sciences, 69(4), 2004, 656-674.
[70] Tovey, C. A.: A simplified NP-complete satisfiability problem, Discrete Applied Mathematics, 8, 1984, 85-89.
[71] Voloshin, V. I.: Coloring Mixed Hypergraphs: Theory, Algorithms and Applications, Fields Institute Monographs, American Mathematical Society, 2002, ISBN 0-8218-2812-6.
[72] Zhao, X., Decheng, D.: Two tractable subclasses of minimal unsatisfiable formulas, Science in China (Series A), 42(7), July 1999, 720-731.

Typ dokumentu

Bibliografia

Identyfikator YADDA

bwmeta1.element.baztech-article-BUS8-0018-0036