Towards a theory of good SAT representations

Matthew Gwynne

(Swansea University)

We aim at providing a foundation of a theory of "good" SAT representations (CNF clause-sets) F of boolean functions f. The hierarchy UC_k of unit-refutation complete clause-sets of level k was introduced by the authors in [2,3,5], based on notions of hardness and generalised unit-clause propagation (UCP) from [6,7]. We argue UC_k provides the most basic target classes for representation. That is, for a good representation, F in UC_k is to be achieved for k as small as feasible.

The first level of the hierarchy, UC_1, is the same as the class UC of unit-refutation complete clause-sets, introduced in 1994 in [10]. The aim of UC was to offer a class of clause-sets which was good for knowledge compilation and representation. More formally, UC is the class of clause-sets where unit-clause propagation (UCP), a simple linear-time inference algorithm, is sufficient decide questions of clausal entailment. In 1995 in [8], the class SLUR (Single Lookahead Unit Resolution) was introduced as an umbrella class for efficient satisfiability (SAT) solving. The motivation was to offer an algorithm for efficiently deciding satisfiability for existing poly-time SAT classes, including renamable Horn, extended Horn, hidden extended Horn, simple extended Horn, and CC-balanced clause-sets. In [2,3,5], we generalise SLUR to a hierarchy SLUR_k, again using generalised UCP, and show that these two hierarchies are in fact equal (SLUR_k = UC_k). This brings together the two notions of representation and efficient SAT solving, and allows one to think of "finding a good representation" as a form of "SAT knowledge compilation". As a first application of this dual perspective, we use results from [1] to show that, for (fixed) k >= 1, deciding whether a clause-set is in UC_k is coNP-complete.

UC_k is directly related to the space complexity of tree resolution. However, in general, it is known that modern SAT solvers can (in some sense) simulate stronger proof systems such as full-resolution. Using the notion of resolution width from [6,7], in [3,5] we introduce the hierarchy WC_k of clause-sets with width-hardness k; for all k the class UC_k is a subset of WC_k. In [4], we introduce lower bound methods for WC_k and use these to prove separation results between UC_(k+1) and UC_k, as well as between WC_(k+1) and WC_k. More formally, we show that for every k >= 1 there are sequences of boolean functions with polynomial size equivalent clause-set representations in UC_(k+1) which have no equivalent polynomial-size representations in WC_k. The boolean functions for these separations are "doped" minimally unsatisfiable clause-sets of deficiency 1; these functions have been introduced in [9], and we generalise their construction and show a correspondence to a strengthened notion of irredundant sub-clause-sets. Turning from lower bounds to upper bounds, we believe that many common CNF representations fit into the UC_k scheme, and we give some basic tools to construct representations in UC_1 with new variables, based on the Tseitin translation.

[1] Ondrej Cepek, Petr Kucera, and Vaclav Vlcek. Properties of SLUR formulae.In Maria Bielikova, Gerhard Friedrich, Georg Gottlob, Stefan Katzenbeisser, and Gyorgy Turan, editors, SOFSEM 2012: Theory and Practice of Computer Science, volume 7147 of LNCS Lecture Notes in Computer Science, pages 177–189. Springer, 2012.

[2] Matthew Gwynne and Oliver Kullmann. Generalising and unifying SLUR and unit-refutation completeness. In Peter van Emde Boas, Frans C. A. Groen, Giuseppe F. Italiano, Jerzy Nawrocki, and Harald Sack, editors, SOFSEM 2013: Theory and Practice of Computer Science, volume 7741 of Lecture Notes in Computer Science (LNCS), pages 220–232. Springer, 2013.

[3] Matthew Gwynne and Oliver Kullmann. Generalising unit-refutation completeness and SLUR via nested input resolution. Technical Report arXiv:1204.6529v5 [cs.LO], arXiv, January 2013.

[4] Matthew Gwynne and Oliver Kullmann. Towards a theory of good SAT representations. Technical Report arXiv:1302.4421v1 [cs.AI], arXiv, February 2013.

[5] Matthew Gwynne and Oliver Kullmann. Generalising unit-refutation completeness and SLUR via nested input resolution. Journal of Automated Reasoning, 2013. To appear.

[6] Oliver 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.

[7] Oliver Kullmann. 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, March 2004.

[8] John S. Schlipf, Fred S. Annexstein, John V. Franco, and R.P. Swaminathan. On finding solutions for extended Horn formulas. Information Processing Letters, 54:133–137, 1995.

[9] Robert H. Sloan, Balazs Sorenyi, and Gyorgy Turan. On k-term DNF with the largest number of prime implicants. SIAM Journal on Discrete Mathematics, 21(4):987–998, 2007.

[10] Alvaro del Val. Tractable databases: How to make propositional unit resolution complete through compilation. In Proceedings of the 4th International Conference on Principles of Knowledge Representation and Reasoning (KR’94), pages 551–561, 1994

Thursday 14th March 2013, 14:00
Robert Recorde Room
Department of Computer Science