Constraint satisfaction problems in clausal form: Autarkies, minimal unsatisfiability, and applications to hypergraph inequalities

作者: Oliver Kullmann

DOI:

关键词: Conjunctive normal formConstraint satisfaction problemDomain (mathematical analysis)Value (mathematics)HypergraphVariable (computer science)CombinatoricsMathematicsMatching (graph theory)Discrete mathematics

摘要: Generalised CNFs are considered using such literals, which exclude exactly one possible value from the domain of variable. First we consider poly-time SAT decision (and fixed-parameter tractability) exploiting matching theory. Then consider irredundant generalised CNFs, and characterise some extremal minimally unsatisfiable CNFs.

参考文章(32)
C. D. Godsil, L. Lovász, Tools from linear algebra Handbook of combinatorics (vol. 2). pp. 1705- 1748 ,(1996)
Christian Sloper, Daniel Lokshtanov, Fixed Parameter Set Splitting, Linear Kernel and Improved Running Time ACiD. pp. 105- 113 ,(2005)
Oliver Kullmann, The Combinatorics of Conflicts between Clauses theory and applications of satisfiability testing. pp. 426- 440 ,(2003) , 10.1007/978-3-540-24605-3_32
Gennady Davydov, Inna Davydova, Hans Kleine Büning, An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF Annals of Mathematics and Artificial Intelligence. ,vol. 23, pp. 229- 245 ,(1998) , 10.1023/A:1018924526592
Steven Prestwich, Local Search on SAT-encoded Colouring Problems theory and applications of satisfiability testing. pp. 105- 119 ,(2003) , 10.1007/978-3-540-24605-3_9
Nicola Galesi, Oliver Kullmann, Polynomial Time SAT Decision, Hypergraph Transversals and the Hermitian Rank Theory and Applications of Satisfiability Testing. pp. 89- 104 ,(2005) , 10.1007/11527695_8
Hans Kleine Büning, An Upper Bound for Minimal Resolution Refutations computer science logic. pp. 171- 178 ,(1998) , 10.1007/10703163_12
Joey Hwang, David G. Mitchell, 2 -Way vs.d -Way Branching for CSP Principles and Practice of Constraint Programming - CP 2005. pp. 343- 357 ,(2005) , 10.1007/11564751_27
Timothy J. Peugniez, Alan M. Frisch, Solving non-Boolean satisfiability problems with stochastic local search international joint conference on artificial intelligence. pp. 282- 288 ,(2001)