Abstract
The class \({\mathcal{SLUR}}\) (Single Lookahead Unit Resolution) was introduced in Schlipf et al. (Inf Process Lett 54:133–137, 1995) as an umbrella class for efficient (poly-time) SAT solving, with linear-time SAT decision, while the recognition problem was not considered. Čepek et al. (2012) and Balyo et al. (2012) extended this class in various ways to hierarchies covering all of CNF (all clause-sets). We introduce a hierarchy \({\mathcal{SLUR}}_k\) which we argue is the natural “limit” of such approaches. The second source for our investigations is the class \({\mathcal{UC}}\) of unit-refutation complete clause-sets, introduced in del Val (1994) as a target class for knowledge compilation. Via the theory of “hardness” of clause-sets as developed in Kullmann (1999), Kullmann (Ann Math Artif Intell 40(3–4):303–352, 2004) and Ansótegui et al. (2008) we obtain a natural generalisation \({\mathcal{UC}}_k\), containing those clause-sets which are “unit-refutation complete of level k”, which is the same as having hardness at most k. Utilising the strong connections to (tree-)resolution complexity and (nested) input resolution, we develop basic methods for the determination of hardness (the level k in \({\mathcal{UC}}_k\)). A fundamental insight now is that \({\mathcal{SLUR}}_k = {\mathcal{UC}}_k\) holds for all k. We can thus exploit both streams of intuitions and methods for the investigations of these hierarchies. As an application we can easily show that the hierarchies from Čepek et al. (2012) and Balyo et al. (2012) are strongly subsumed by \({\mathcal{SLUR}}_k\). Finally we consider the problem of “irredundant” clause-sets in \({\mathcal{UC}}_k\). For 2-CNF we show that strong minimisations are possible in polynomial time, while already for (very special) Horn clause-sets minimisation is NP-complete. We conclude with an extensive discussion of open problems and future directions. We envisage the concepts investigated here to be the starting point for a theory of good SAT translations, which brings together the good SAT-solving aspects from \({\mathcal{SLUR}}\) together with the knowledge-representation aspects from \({\mathcal{UC}}\), and expands this combination via notions of “hardness”.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Ansótegui, C., Bonet, M.L., Levy, J., Manyà, F.: Measuring the hardness of SAT instances. In: Fox, D., Gomes, C. (eds.) Proceedings of the 23th AAAI Conference on Artificial Intelligence (AAAI-08), pp. 222–228 (2008)
Balyo, T., Gurský, Š., Kučera, P., Vlček, V.: On hierarchies over the SLUR class. In: Twelfth International Symposium on Artificial Intelligence and Mathematics (ISAIM 2012) (2012). Available at http://www.cs.uic.edu/bin/view/Isaim2012/AcceptedPapers
Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, chapter 26, pp. 825–885. IOS Press (2009). ISBN 978-1-58603-929-5
Bessiere, C.: Constraint propagation. In: Rossi, F., van Beek, P., Walsh, T. (eds.) Handbook of Constraint Programming. Foundations of Artificial Intelligence, chapter 3, pp. 29–83. Elsevier (2006). ISBN 0-444-52726-5
Bessiere, C., Katsirelos, G., Narodytska, N., Walsh, T.: Circuit complexity and decompositions of global constraints. In: Proceedings of the Twenty-First International Joint Conference on Artificial Intelligence (IJCAI-09), pp. 412–418 (2009)
Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (2009). ISBN 978-1-58603-929-5
Bordeaux, L., Marques-Silva, J.: Knowledge compilation with empowerment. In: Bieliková, M., Friedrich, G., Gottlob, G., Katzenbeisser, S., Turán, G. (eds.) SOFSEM 2012: Theory and Practice of Computer Science. Lecture Notes in Computer Science, vol. 7147, pp. 612–624. Springer (2012)
Bordeaux, L., Janota, M., Marques-Silva, J., Marquis, P.: On unit-refutation complete formulae with existentially quantified variables. In: Knowledge Representation 2012 (KR 2012). Association for the Advancement of Artificial Intelligence (AAAI Press) (2012)
Boros, E., Čepek, O.: On the complexity of Horn minimization. Technical Report RRR 1-94, Rutcor Research Report (1994)
Bubeck, U., Büning, H.K.: The power of auxiliary variables for propositional and quantified boolean formulas. Stud. Log. 3(3), 1–23 (2010)
Čepek, O., Kučera, P.: Known and new classes of generalized Horn formulae with polynomial recognition and SAT testing. Discrete Appl. Math. 149, 14–52 (2005)
Čepek, O., Kučera, P., Vlček, V.: Properties of SLUR formulae. In: Bieliková, M., Friedrich, G., Gottlob, G., Katzenbeisser, S., Turán, G. (eds.) SOFSEM 2012: Theory and Practice of Computer Science. LNCS Lecture Notes in Computer Science, vol. 7147, pp. 177–189. Springer (2012)
Chang, T.: Horn formula minimization. Master’s thesis, Rochester Institute of Technology (2004)
Crama, Y., Hammer, P.L.: Boolean functions: theory, algorithms, and applications. In: Encyclopedia of Mathematics and Its Applications, vol. 142. Cambridge University Press (2011). ISBN 978-0-521-84751-3
Creignou, N., Kolaitis, P., Vollmer, H. (eds.): Complexity of Constraints: An Overview of Current Research Themes. Lecture Notes in Computer Science (LNCS), vol. 5250. Springer (2008). ISBN-10 3-540-92799-9
Dantsin, E., Hirsch, E.A.: Worst-case upper bounds. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, chapter 12, pp. 403–424. IOS Press (2009). ISBN 978-1-58603-929-5
Darwiche, A., Marquis, P.: A knowledge compilation map. J. Artif. Intell. Res. 17, 229–264 (2002)
Darwiche, A., Pipatsrisawat, K.: On the power of clause-learning SAT solvers as resolution engines. Artif. Intell. 175(2), 512–525 (2011)
de Klerk, E., van Maaren, H., Warners, J.P.: Relaxations of the satisfiability problem using semidefinite programming. J. Autom. Reason. 24, 37–65 (2000)
del Val, A.: 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), pp. 551–561 (1994)
Franco, J.: Relative size of certain polynomial time solvable subclasses of satisfiability. In: Du, D., Gu, J., Pardalos, P.M. (eds.) Satisfiability Problem: Theory and Applications (DIMACS Workshop March 11–13, 1996). DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 35, pp. 211–223. American Mathematical Society (1997). ISBN 0-8218-0479-0
Franco, J., Martin, J.: A history of satisfiability. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, chapter 1, pp. 3–74. IOS Press (2009). ISBN 978-1-58603-929-5
Franco, J., Schlipf, J.: 1997 final report: Describing new results under the research project entitled Complexity of algorithms for problems in propositional logic. Covering the period January 1, 1994–march 31, 1997. Technical report, University of Cincinnati and Office of Naval Research (1997). Available at http://www.dtic.mil/docs/citations/ADA325949
Franco, J., Van Gelder, A.: A perspective on certain polynomial-time solvable classes of satisfiability. Discrete Appl. Math. 125, 177–214 (2003)
Gwynne, M., Kullmann, O.: Towards a better understanding of hardness. In: The Seventeenth International Conference on Principles and Practice of Constraint Programming (CP 2011): Doctoral Program Proceedings, pp. 37–42 (2011). Proceedings available at http://www.dmi.unipg.it/cp2011/downloads/dp2011/DP_at_CP2011.pdf
Gwynne, M., Kullmann, O.: Towards a better understanding of SAT translations. In: Berger, U., Therien, D. (eds.) Logic and Computational Complexity (LCC’11), as part of LICS 2011 (2011). 10 pp., available at http://www.cs.swansea.ac.uk/lcc2011/
Gwynne, M., Kullmann, O.: Generalising unit-refutation completeness and SLUR via nested input resolution. Technical Report arXiv:1204.6529v5 [cs.LO], arXiv (2013)
Gwynne, M., Kullmann, O.: Generalising and unifying SLUR and unit-refutation completeness. In: van Emde Boas, P., Groen, F.C.A., Italiano, G.F., Nawrocki, J., Sack, H. (eds.) SOFSEM 2013: Theory and Practice of Computer Science. Lecture Notes in Computer Science (LNCS), vol. 7741, pp. 220–232. Springer (2013). doi:10.1007/978-3-642-35843-2_20
Gwynne, M., Kullmann, O.: Towards a theory of good SAT representations. Technical Report arXiv:1302.4421 [cs.AI], arXiv (2013)
Hemaspaandra, E., Schnoor, H.: Minimization for generalized boolean formulas. In: Walsh, T. (ed.) Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence, vol. 1, pp. 566–571. AAAI Press (2011)
Henschen, L.J., Wos, L.: Unit refutations and Horn sets. J. Assoc. Comput. Mach. 21(4), 590–605 (1974)
Heule, M.J.H., van Maaren, H.: Look-ahead based SAT solvers. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, chapter 5, pp. 155–184. IOS Press (2009). ISBN 978-1-58603-929-5
Heule, M.J.H., Kullmann, O., Wieringa, S., Biere, A.: Cube and conquer: guiding CDCL SAT solvers by lookaheads. In: Eder, K., Lourenço, J., Shehory, O. (eds.) Hardware and Software: Verification and Testing (HVC 2011). Lecture Notes in Computer Science (LNCS), vol. 7261, pp. 50–65. Springer (2012). doi:10.1007/978-3-642-34188-5_8. http://cs.swan.ac.uk/~csoliver/papers.html#CuCo2011
Kleine Büning, H.: On generalized Horn formulas and k-resolution. Theor. Comput. Sci. 116, 405–413 (1993)
Kleine Büning, H., Kullmann, O.: Minimal unsatisfiability and autarkies. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, chapter 11, pp. 339–401 (2009). ISBN 978-1-58603-929-5. doi:10.3233/978-1-58603-929-5-339
Kullmann, O.: 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) (1999)
Kullmann, O.: Upper and lower bounds on the complexity of generalised resolution and generalised constraint satisfaction problems. Ann. Math. Artif. Intell. 40(3–4), 303–352 (2004)
Kullmann, O.: Present and future of practical SAT solving. In: Creignou, N., Kolaitis, P., Vollmer, H. (eds.): Complexity of Constraints: An Overview of Current Research Themes. Lecture Notes in Computer Science (LNCS), vol. 5250, pp. 283–319. Springer (2008). ISBN-10 3-540-92799-9. doi:10.1007/978-3-540-92800-3_11
Kullmann, O.: Fundaments of branching heuristics. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, chapter 7, pp. 205–244. IOS Press (2009). ISBN 978-1-58603-929-5. doi:10.3233/978-1-58603-929-5-205
Laitinen, T., Junttila, T., Niemelä, I.: Classifing and propagating parity constraints. In: Milano, M. (ed.) Principles and Practice of Constraint Programming—CP 2012. Lecture Notes in Computer Science (LNCS), vol. 7514, pp. 357–372. Springer (2012)
Nordström, J.: Pebble games, proof complexity, and time-space trade-offs. In: Logical Methods in Computer Science (2013, to appear)
Schaefer, M., Umans, C.: Completeness in the polynomial-time hierarchy: a compendium. SIGACT News 33(3), 32–49 (2002)
Schlipf, J.S., Annexstein, F.S., Franco, J.V., Swaminathan, R.P.: On finding solutions for extended Horn formulas. Inf. Process. Lett. 54, 133–137 (1995)
van Maaren, H.: A short note on some tractable cases of the satisfiability problem. Inf. Comput. 158(2), 125–130 (2000)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Gwynne, M., Kullmann, O. Generalising Unit-Refutation Completeness and SLUR via Nested Input Resolution. J Autom Reasoning 52, 31–65 (2014). https://doi.org/10.1007/s10817-013-9275-8
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-013-9275-8