{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T00:10:08Z","timestamp":1745971808057,"version":"3.40.4"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2013,3,9]],"date-time":"2013-03-09T00:00:00Z","timestamp":1362787200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2014,1]]},"DOI":"10.1007\/s10817-013-9275-8","type":"journal-article","created":{"date-parts":[[2013,3,8]],"date-time":"2013-03-08T07:18:59Z","timestamp":1362727139000},"page":"31-65","source":"Crossref","is-referenced-by-count":10,"title":["Generalising Unit-Refutation Completeness and SLUR via Nested Input Resolution"],"prefix":"10.1007","volume":"52","author":[{"given":"Matthew","family":"Gwynne","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Oliver","family":"Kullmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,3,9]]},"reference":[{"key":"9275_CR1","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., Levy, J., Many\u00e0, 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\u2013228 (2008)"},{"key":"9275_CR2","unstructured":"Balyo, T., Gursk\u00fd, \u0160., Ku\u010dera, P., Vl\u010dek, 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"},{"key":"9275_CR3","unstructured":"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\u2013885. IOS Press (2009). ISBN 978-1-58603-929-5"},{"key":"9275_CR4","unstructured":"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\u201383. Elsevier (2006). ISBN 0-444-52726-5"},{"key":"9275_CR5","unstructured":"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\u2013418 (2009)"},{"key":"9275_CR6","unstructured":"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"},{"key":"9275_CR7","doi-asserted-by":"crossref","unstructured":"Bordeaux, L., Marques-Silva, J.: Knowledge compilation with empowerment. In: Bielikov\u00e1, M., Friedrich, G., Gottlob, G., Katzenbeisser, S., Tur\u00e1n, G. (eds.) SOFSEM 2012: Theory and Practice of Computer Science. Lecture Notes in Computer Science, vol. 7147, pp. 612\u2013624. Springer (2012)","DOI":"10.1007\/978-3-642-27660-6_50"},{"key":"9275_CR8","unstructured":"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)"},{"key":"9275_CR9","unstructured":"Boros, E., \u010cepek, O.: On the complexity of Horn minimization. Technical Report RRR 1-94, Rutcor Research Report (1994)"},{"issue":"3","key":"9275_CR10","first-page":"1","volume":"3","author":"U Bubeck","year":"2010","unstructured":"Bubeck, U., B\u00fcning, H.K.: The power of auxiliary variables for propositional and quantified boolean formulas. Stud. Log. 3(3), 1\u201323 (2010)","journal-title":"Stud. Log."},{"key":"9275_CR11","unstructured":"\u010cepek, O., Ku\u010dera, P.: Known and new classes of generalized Horn formulae with polynomial recognition and SAT testing. Discrete Appl. Math. 149, 14\u201352 (2005)"},{"key":"9275_CR12","doi-asserted-by":"crossref","unstructured":"\u010cepek, O., Ku\u010dera, P., Vl\u010dek, V.: Properties of SLUR formulae. In: Bielikov\u00e1, M., Friedrich, G., Gottlob, G., Katzenbeisser, S., Tur\u00e1n, G. (eds.) SOFSEM 2012: Theory and Practice of Computer Science. LNCS Lecture Notes in Computer Science, vol. 7147, pp. 177\u2013189. Springer (2012)","DOI":"10.1007\/978-3-642-27660-6_15"},{"key":"9275_CR13","unstructured":"Chang, T.: Horn formula minimization. Master\u2019s thesis, Rochester Institute of Technology (2004)"},{"key":"9275_CR14","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1017\/CBO9780511852008"},{"key":"9275_CR15","unstructured":"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"},{"key":"9275_CR16","unstructured":"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\u2013424. IOS Press (2009). ISBN 978-1-58603-929-5"},{"key":"9275_CR17","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1613\/jair.989","volume":"17","author":"A Darwiche","year":"2002","unstructured":"Darwiche, A., Marquis, P.: A knowledge compilation map. J. Artif. Intell. Res. 17, 229\u2013264 (2002)","journal-title":"J. Artif. Intell. Res."},{"issue":"2","key":"9275_CR18","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1016\/j.artint.2010.10.002","volume":"175","author":"A Darwiche","year":"2011","unstructured":"Darwiche, A., Pipatsrisawat, K.: On the power of clause-learning SAT solvers as resolution engines. Artif. Intell. 175(2), 512\u2013525 (2011)","journal-title":"Artif. Intell."},{"key":"9275_CR19","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1023\/A:1006362203438","volume":"24","author":"E Klerk de","year":"2000","unstructured":"de Klerk, E., van Maaren, H., Warners, J.P.: Relaxations of the satisfiability problem using semidefinite programming. J. Autom. Reason. 24, 37\u201365 (2000)","journal-title":"J. Autom. Reason."},{"key":"9275_CR20","doi-asserted-by":"crossref","unstructured":"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\u201994), pp. 551\u2013561 (1994)","DOI":"10.1016\/B978-1-4832-1452-8.50146-9"},{"key":"9275_CR21","unstructured":"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\u201313, 1996). DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 35, pp. 211\u2013223. American Mathematical Society (1997). ISBN 0-8218-0479-0"},{"key":"9275_CR22","unstructured":"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\u201374. IOS Press (2009). ISBN 978-1-58603-929-5"},{"key":"9275_CR23","unstructured":"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\u2013march 31, 1997. Technical report, University of Cincinnati and Office of Naval Research (1997). Available at http:\/\/www.dtic.mil\/docs\/citations\/ADA325949"},{"key":"9275_CR24","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/S0166-218X(01)00358-4","volume":"125","author":"J Franco","year":"2003","unstructured":"Franco, J., Van Gelder, A.: A perspective on certain polynomial-time solvable classes of satisfiability. Discrete Appl. Math. 125, 177\u2013214 (2003)","journal-title":"Discrete Appl. Math."},{"key":"9275_CR25","unstructured":"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\u201342 (2011). Proceedings available at http:\/\/www.dmi.unipg.it\/cp2011\/downloads\/dp2011\/DP_at_CP2011.pdf"},{"key":"9275_CR26","unstructured":"Gwynne, M., Kullmann, O.: Towards a better understanding of SAT translations. In: Berger, U., Therien, D. (eds.) Logic and Computational Complexity (LCC\u201911), as part of LICS 2011 (2011). 10 pp., available at http:\/\/www.cs.swansea.ac.uk\/lcc2011\/"},{"key":"9275_CR27","doi-asserted-by":"crossref","unstructured":"Gwynne, M., Kullmann, O.: Generalising unit-refutation completeness and SLUR via nested input resolution. Technical Report arXiv:1204.6529v5 [cs.LO], arXiv (2013)","DOI":"10.1007\/s10817-013-9275-8"},{"key":"9275_CR28","doi-asserted-by":"crossref","unstructured":"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\u2013232. Springer (2013). doi: 10.1007\/978-3-642-35843-2_20","DOI":"10.1007\/978-3-642-35843-2_20"},{"key":"9275_CR29","unstructured":"Gwynne, M., Kullmann, O.: Towards a theory of good SAT representations. Technical Report arXiv:1302.4421 [cs.AI], arXiv (2013)"},{"key":"9275_CR30","unstructured":"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\u2013571. AAAI Press (2011)"},{"issue":"4","key":"9275_CR31","doi-asserted-by":"crossref","first-page":"590","DOI":"10.1145\/321850.321857","volume":"21","author":"LJ Henschen","year":"1974","unstructured":"Henschen, L.J., Wos, L.: Unit refutations and Horn sets. J. Assoc. Comput. Mach. 21(4), 590\u2013605 (1974)","journal-title":"J. Assoc. Comput. Mach."},{"key":"9275_CR32","unstructured":"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\u2013184. IOS Press (2009). ISBN 978-1-58603-929-5"},{"key":"9275_CR33","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Kullmann, O., Wieringa, S., Biere, A.: Cube and conquer: guiding CDCL SAT solvers by lookaheads. In: Eder, K., Louren\u00e7o, J., Shehory, O. (eds.) Hardware and Software: Verification and Testing (HVC 2011). Lecture Notes in Computer Science (LNCS), vol. 7261, pp. 50\u201365. Springer (2012). doi: 10.1007\/978-3-642-34188-5_8 . http:\/\/cs.swan.ac.uk\/~csoliver\/papers.html#CuCo2011","DOI":"10.1007\/978-3-642-34188-5_8"},{"key":"9275_CR34","doi-asserted-by":"crossref","first-page":"405","DOI":"10.1016\/0304-3975(93)90331-M","volume":"116","author":"H Kleine B\u00fcning","year":"1993","unstructured":"Kleine B\u00fcning, H.: On generalized Horn formulas and k-resolution. Theor. Comput. Sci. 116, 405\u2013413 (1993)","journal-title":"Theor. Comput. Sci."},{"key":"9275_CR35","doi-asserted-by":"crossref","unstructured":"Kleine B\u00fcning, 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\u2013401 (2009). ISBN 978-1-58603-929-5. doi: 10.3233\/978-1-58603-929-5-339","DOI":"10.3233\/978-1-58603-929-5-339"},{"key":"9275_CR36","unstructured":"Kullmann, O.: Investigating a general hierarchy of polynomially decidable classes of CNF\u2019s based on short tree-like resolution proofs. Technical Report TR99-041, Electronic Colloquium on Computational Complexity (ECCC) (1999)"},{"issue":"3\u20134","key":"9275_CR37","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1023\/B:AMAI.0000012871.08577.0b","volume":"40","author":"O Kullmann","year":"2004","unstructured":"Kullmann, O.: Upper and lower bounds on the complexity of generalised resolution and generalised constraint satisfaction problems. Ann. Math. Artif. Intell. 40(3\u20134), 303\u2013352 (2004)","journal-title":"Ann. Math. Artif. Intell."},{"key":"9275_CR38","doi-asserted-by":"crossref","unstructured":"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\u2013319. Springer (2008). ISBN-10 3-540-92799-9. doi: 10.1007\/978-3-540-92800-3_11","DOI":"10.1007\/978-3-540-92800-3_11"},{"key":"9275_CR39","doi-asserted-by":"crossref","unstructured":"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\u2013244. IOS Press (2009). ISBN 978-1-58603-929-5. doi: 10.3233\/978-1-58603-929-5-205","DOI":"10.3233\/978-1-58603-929-5-205"},{"key":"9275_CR40","doi-asserted-by":"crossref","unstructured":"Laitinen, T., Junttila, T., Niemel\u00e4, I.: Classifing and propagating parity constraints. In: Milano, M. (ed.) Principles and Practice of Constraint Programming\u2014CP 2012. Lecture Notes in Computer Science (LNCS), vol. 7514, pp. 357\u2013372. Springer (2012)","DOI":"10.1007\/978-3-642-33558-7_28"},{"key":"9275_CR41","doi-asserted-by":"crossref","unstructured":"Nordstr\u00f6m, J.: Pebble games, proof complexity, and time-space trade-offs. In: Logical Methods in Computer Science (2013, to appear)","DOI":"10.2168\/LMCS-9(3:15)2013"},{"issue":"3","key":"9275_CR42","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1145\/582475.582484","volume":"33","author":"M Schaefer","year":"2002","unstructured":"Schaefer, M., Umans, C.: Completeness in the polynomial-time hierarchy: a compendium. SIGACT News 33(3), 32\u201349 (2002)","journal-title":"SIGACT News"},{"key":"9275_CR43","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/0020-0190(95)00019-9","volume":"54","author":"JS Schlipf","year":"1995","unstructured":"Schlipf, J.S., Annexstein, F.S., Franco, J.V., Swaminathan, R.P.: On finding solutions for extended Horn formulas. Inf. Process. Lett. 54, 133\u2013137 (1995)","journal-title":"Inf. Process. Lett."},{"issue":"2","key":"9275_CR44","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1006\/inco.2000.2867","volume":"158","author":"H Maaren van","year":"2000","unstructured":"van Maaren, H.: A short note on some tractable cases of the satisfiability problem. Inf. Comput. 158(2), 125\u2013130 (2000)","journal-title":"Inf. Comput."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9275-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-013-9275-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9275-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T23:33:53Z","timestamp":1745969633000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-013-9275-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,3,9]]},"references-count":44,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,1]]}},"alternative-id":["9275"],"URL":"https:\/\/doi.org\/10.1007\/s10817-013-9275-8","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2013,3,9]]}}}