Constraint Satisfaction Problems in Clausal Form II: Minimal Unsatisfiability and Conflict Structure

• Autorzy: Kullmann O.
• Języki publikacji: EN

Abstrakty

EN

Concluding this mini-series of 2 articles on the foundations of generalised clause-sets, we study the combinatorial properties of non-boolean conjunctive normal forms (clause-sets), allowing arbitrary (but finite) sets of values for variables, while literals express that some variable shall not get some (given) value. First we study the properties of the direct translation (or "encoding") of generalised clause-sets into boolean clause-sets. Many combinatorial properties are preserved, and as a result we can lift fixed-parameter tractability of satisfiability in the maximal deficiency from the boolean case to the general case. Then we turn to irredundant clause-sets, which generalise minimally unsatisfiable clause-sets, and we prove basic properties. The simplest irredundant clause-sets are hitting clause-sets, and we provide characterisations and generalisations. Unsatisfiable irredundant clause-sets are the minimally unsatisfiable clause-sets, and we provide basic tools. These tools allow us to characterise the minimally unsatisfiable clause-sets of minimal deficiency. Finally we provide a new translation of generalised boolean clause-sets into boolean clause-sets, the nested translation, which preserves the conflict structure. As an application, we can generalise results for boolean clause-sets regarding the hermitian rank/defect, especially the characterisation of unsatisfiable hitting clause-sets where between every two clauses we have exactly one conflict. We conclude with a list of open problems, and a discussion of the "generic translation scheme".

Słowa kluczowe

EN

generalised clause-sets; satisfiability; non-boolean variables; boolean translations; direct ecoding; irredundant clause-sets; minimally unsatisfiable clause-sets; deficiency; hitting clause-sets; disjoint DNF; hermitian defect; nested translation

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2011
• Tom: Vol. 109, nr 1
• Strony: 83--119
• Opis fizyczny: Bibliogr. 39 poz.

Twórcy

autor

Kullmann O.

• Computer Science Department, Swansea University, Swansea, SA2 8PP, United Kingdom

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] Ansótegui, C., Manyà, F.: Mapping Problems with Finite-Domain Variables to Problems with Boolean Variables, in: Hoos and Mitchell [13], 1-15, ISBN 3-540-27829-X.
• [3] Bacchus, F., Walsh, T., Eds.: Theory and Applications of Satisfiability Testing 2005, vol. 3569 of Lecture Notes in Computer Science, Springer, Berlin, 2005, ISBN 3-540-26276-8.
• [4] 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.
• [5] Bruni, R.: Approximating minimal unsatisfiable subformulae by means of adaptive core search, Discrete Applied Mathematics, 130, 2003, 85-100.
• [6] 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.
• [7] Fliti, T., Reynaud, G.: Sizes of minimally unsatisfiable conjunctive normal forms, November 1994, Faculté des Sciences de Luminy, Dpt. Mathematique-Informatique, 13288 Marseille, France.
• [8] 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.
• [9] Galesi, N., Kullmann, O.: Polynomial Time SAT Decision, HypergraphTransversals and the Hermitian Rank, in: Hoos and Mitchell [13], 89-104, ISBN 3-540-27829-X.
• [10] 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.
• [11] Green, B., Tao, T.: The primes contain arbitrarily long arithmetic progressions, Annals of Mathematics, 167(2), 2008, 481-547.
• [12] Gregory, D. A., Meulen, K. N. V.: Sharp Bounds for Decompositions of Graphs into Complete r-Partite Subgraphs, Journal of Graph Theory, 21(4), 1996, 393-400.
• [13] 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.
• [14] Kleine Büning, H.: On subclasses of minimal unsatisfiable formulas, Discrete Applied Mathematics, 107, 2000, 83-98.
• [15] Kleine Büning, H., Kullmann, O.: Minimal Unsatisfiability and Autarkies, in: Biere et al. [4], chapter 11, 339-401.
• [16] Kleine Büning, H., Zhao, X.: Extension and equivalence problems for clause minimal formulae, Annals of Mathematics and Artificial Intelligence, 43, 2005, 295-306.
• [17] 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.
• [18] Kratzke, T., Reznik, B., West, D.: Eigensharp Graphs: Decompositions into Complete Bipartite Subgraphs, Transactions of the American Mathematical Society, 308(2), August 1988, 637-653.
• [19] Kullmann, O.: An application of matroid theory to the SAT problem, Fifteenth Annual IEEE Conference on Computational Complexity (2000), IEEE Computer Society, July 2000.
• [20] 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.
• [21] Kullmann, O.: On the conflict matrix of clause-sets, Technical Report CSR 7-2003, University of Wales Swansea, Computer Science Report Series, March 2003.
• [22] Kullmann, O.: The Combinatorics of Conflicts between Clauses, in: Giunchiglia and Tacchella [10], 426-440, ISBN 3-540-20851-8.
• [23] Kullmann, O.: Conflict matrices and multi-hitting clause-sets, September 2004, Extended Abstract for the Guangzhou Symposium on Satisfiability and its Applications.
• [24] 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.
• [25] Kullmann, O.: The conflict matrix of (multi-)clause-sets - a link between combinatorics and (generalised) satisfiability problems, Technical report, Swansea University, Computer Science Report Series (http://www-compsci.swan.ac.uk/reports/2007.html), 2008, In preparation; continuation of [21].
• [26] 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.
• [27] Kullmann, O.: Constraint satisfaction problems in clausal form I: Autarkies and deficiency, Fundamenta Informaticae, 2011, To appear.
• [28] Kullmann, O.: Multiclique partitions of multigraphs, and conflict-regular satisfiability problems with nonboolean variables, August 2011, In preparation.
• [29] 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.
• [30] Kullmann, O., Zhao, X.: On variables with few occurrences in conjunctive normal forms, Technical report, arXiv, October 2010.
• [31] Liberatore, P.: Redundancy in Logic I: CNF Propositional Formulae, Artificial Intelligence, 163, 2005, 203-232.
• [32] Liffiton, M. H., Sakallah, K. A.: On Finding All Minimally Unsatisfiable Subformulas, in: Bacchus and Walsh [3], 173-186, ISBN 3-540-26276-8.
• [33] van Lint, J. H., Wilson, R. M.: A Course in Combinatorics, Second edition, Cambridge University Press, 2001, ISBN 0 521 00601 5; fifth printing with corrections 2006.
• [34] 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.
• [35] Papadimitriou, C. H., Wolfe, D.: The Complexity of Facets Resolved, Journal of Computer and System Sciences, 37, 1988, 2-13.
• [36] Prestwich, S.: Local Search on SAT-encoded Colouring Problems, in: Giunchiglia and Tacchella [10], 105-119, ISBN 3-540-20851-8.
• [37] Prestwich, S.: CNF Encodings, in: Biere et al. [4], chapter 2, 75-97.
• [38] 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.
• [39] Szeider, S.: Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable, Journal of Computer and System Sciences, 69(4), 2004, 656-