{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T19:45:41Z","timestamp":1725479141962},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540262763"},{"type":"electronic","value":"9783540316794"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11499107_11","type":"book-chapter","created":{"date-parts":[[2010,7,14]],"date-time":"2010-07-14T21:56:25Z","timestamp":1279144585000},"page":"143-157","source":"Crossref","is-referenced-by-count":8,"title":["Resolution Tunnels for Improved SAT Solver Performance"],"prefix":"10.1007","author":[{"given":"Michal","family":"Kouril","sequence":"first","affiliation":[]},{"given":"John","family":"Franco","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"6","key":"11_CR1","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1109\/TC.1978.1675141","volume":"27","author":"S.B. Akers","year":"1978","unstructured":"Akers, S.B.: Binary decision diagrams. IEEE Transactions on Computers\u00a0C-27(6), 509\u2013516 (1978)","journal-title":"IEEE Transactions on Computers"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Beame, P., Pitassi, T.: Simplified and improved resolution lower bounds. In: Proc. 37th Annual Symposium on Foundations of Computer Science, pp. 274\u2013282 (1996)","DOI":"10.1109\/SFCS.1996.548486"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Beame, P., Karp, R.M., Pitassi, T., Saks, M.: On the complexity of unsatisfiability proofs for random k-CNF formulas. In: Proc. 30th Annual Symposium on the Theory of Computing, pp. 561\u2013571 (1998)","DOI":"10.1145\/276698.276870"},{"key":"11_CR4","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1145\/375827.375835","volume":"48","author":"E. Ben-Sasson","year":"2001","unstructured":"Ben-Sasson, E., Wigderson, A.: Short proofs are narrow - resolution made simple. Journal of the Association for Computing Machinery\u00a048, 149\u2013169 (2001)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Brace, K.S., Rudell, R.R., Bryant, R.E.: Efficient implementation of a BDD package. In: Proc. 27th ACM\/IEEE Design Automation Conf., pp. 40\u201345 (1990)","DOI":"10.1145\/123186.123222"},{"issue":"8","key":"11_CR6","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. on Comp.\u00a0C-35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. on Comp."},{"key":"11_CR7","series-title":"IFIP Transactions","first-page":"49","volume-title":"Intnl. Conf. on VLSI","author":"J. Burch","year":"1991","unstructured":"Burch, J., Clark, E., Long, D.: Symbolic model checking with partitioned transitions relations. In: Halaas, A., Denyer, P.B. (eds.) Intnl. Conf. on VLSI. IFIP Transactions, pp. 49\u201358. North-Holland, Amsterdam (1991)"},{"key":"11_CR8","doi-asserted-by":"crossref","first-page":"759","DOI":"10.1145\/48014.48016","volume":"35","author":"V. Chv\u00e1tal","year":"1988","unstructured":"Chv\u00e1tal, V., Szemer\u00e9di, E.: Many hard examples for resolution. Journal of the Association for Computing Machinery\u00a035, 759\u2013768 (1988)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"11_CR9","unstructured":"Cooke, M.: Van der Waerden numbers, Available from http:\/\/home.comcast.net\/~rm_cooke\/vdw.html"},{"key":"11_CR10","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A Machine Program for Theorem Proving. Communications of the Association of Computing Machinery\u00a05, 394\u2013397 (1962)","journal-title":"Communications of the Association of Computing Machinery"},{"key":"11_CR11","unstructured":"Dransfield, M.R., Liu, L., Marek, V., Truszczynski, M.: Using Answer-Set Programming to study van der Waerden numbers. Logic and Artificial Intelligence Laboratory, Computer Science Department, College of Enginnering, University of Kentucky (September 2004), Available from http:\/\/cs.engr.uky.edu\/ai\/vdw\/"},{"key":"11_CR12","unstructured":"Dransfield, M., Bryant, R.E.: Using ordered binary decision diagrams to solve highly structured satisfiability problems. Unpublished technical report CMU-CS-1996, Carnegie Mellon University (1996)"},{"key":"11_CR13","doi-asserted-by":"publisher","first-page":"444","DOI":"10.1137\/0206031","volume":"6","author":"Z. Galil","year":"1977","unstructured":"Galil, Z.: On resolution with clauses of bounded size. SIAM Journal on Computing\u00a06, 444\u2013459 (1977)","journal-title":"SIAM Journal on Computing"},{"key":"11_CR14","unstructured":"Gent, I.P., Walsh, T.: Towards an understanding of hill-climbing procedures for SAT. In: Proc. 11th National Conference on Artificial Intelligence, pp. 28\u201333 (1993)"},{"key":"11_CR15","unstructured":"Groote, J.F.: Hiding propositional constants in BDDs. Logic Group Preprint Series 120, Utrecht University (1994)"},{"issue":"1","key":"11_CR16","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1145\/130836.130837","volume":"3","author":"J. Gu","year":"1992","unstructured":"Gu, J.: Efficient local search for very large-scale satisfiability problems. ACM SIGART Bulletin\u00a03(1), 8\u201312 (1992)","journal-title":"ACM SIGART Bulletin"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Gu, J., Purdom, P.W., Franco, J., Wah, J.: Algorithms for the Satisfiability problem: a survey. DIMACS Series on Discrete Mathematics and Theoretical Computer Science, vol.\u00a035, pp. 19\u2013151 (1997)","DOI":"10.1090\/dimacs\/035\/02"},{"key":"11_CR18","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A. Haken","year":"1985","unstructured":"Haken, A.: The intractability of resolution. Theoretical Computer Science\u00a039, 297\u2013308 (1985)","journal-title":"Theoretical Computer Science"},{"key":"11_CR19","doi-asserted-by":"crossref","first-page":"985","DOI":"10.1002\/j.1538-7305.1959.tb01585.x","volume":"38","author":"C.Y. Lee","year":"1959","unstructured":"Lee, C.Y.: Representation of switching circuits by binary-decision programs. Bell System Technical Journal\u00a038, 985\u2013999 (1959)","journal-title":"Bell System Technical Journal"},{"key":"11_CR20","unstructured":"McAllester, D., Selman, B., Kautz, H.A.: Evidence for invariants in local search. In: Proc. International Joint Conference on Artificial Intelligence, pp. 321\u2013326 (1997)"},{"key":"11_CR21","first-page":"117","volume":"10","author":"B. Monien","year":"1983","unstructured":"Monien, B., Speckenmeyer, E.: Solving satisfiability in less than 2 n steps. Discrete Applied Mathematics\u00a010, 117\u2013133 (1983)","journal-title":"Discrete Applied Mathematics"},{"key":"11_CR22","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. Journal of the ACM\u00a012, 23\u201341 (1965)","journal-title":"Journal of the ACM"},{"key":"11_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/11527695_19","volume-title":"Theory and Applications of Satisfiability Testing","author":"G. Pan","year":"2005","unstructured":"Pan, G., Vardi, M.Y.: Search vs. symbolic techniques in satisfiability solving. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 235\u2013250. Springer, Heidelberg (2005)"},{"key":"11_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/3-540-45578-7_9","volume-title":"Principles and Practice of Constraint Programming - CP 2001","author":"A. San Miguel Aguirre","year":"2001","unstructured":"San Miguel Aguirre, A., Vardi, M.Y.: Random 3-SAT and BDDs: The plot thickens further. In: Walsh, T. (ed.) CP 2001. LNCS, vol.\u00a02239, pp. 121\u2013136. Springer, Heidelberg (2001)"},{"key":"11_CR25","unstructured":"Selman, B., Kautz, H.A., Cohen, B.: Noise strategies for improving local search. In: Proc. 12th National Conference on Artificial Intelligence, pp. 337\u2013343 (1994)"},{"key":"11_CR26","unstructured":"Somenzi, F.: Colorado University Decision Diagram package, Available from http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/"},{"issue":"2","key":"11_CR27","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1016\/0097-3165(92)90018-P","volume":"61","author":"H.Y. Song","year":"1992","unstructured":"Song, H.Y., Golomb, S.W., Taylor, H.: Progressions in Every Two-coloration of Z n . Journal of Combinatorial Theory, Series A\u00a061(2), 211\u2013221 (1992)","journal-title":"Journal of Combinatorial Theory, Series A"},{"issue":"1","key":"11_CR28","doi-asserted-by":"publisher","first-page":"87","DOI":"10.4153\/CMB-1979-012-1","volume":"22","author":"J.R. Rabung","year":"1979","unstructured":"Rabung, J.R.: Some Progression-Free Partitions Constructed Using Folkman\u2019s Method. Canadian Mathematical Bulletin\u00a022(1), 87\u201391 (1979)","journal-title":"Canadian Mathematical Bulletin"},{"key":"11_CR29","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1145\/7531.8928","volume":"34","author":"A. Urquhart","year":"1987","unstructured":"Urquhart, A.: Hard examples for resolution. Journal of the Association for Computing Machinery\u00a034, 209\u2013219 (1987)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"11_CR30","first-page":"212","volume":"15","author":"B.L. Waerden Van der","year":"1927","unstructured":"Van der Waerden, B.L.: Beweis einer Baudetschen Veermutung. Nieuw Archief voor Wiskunde\u00a015, 212\u2013216 (1927)","journal-title":"Nieuw Archief voor Wiskunde"},{"key":"11_CR31","unstructured":"Weaver, S.A., Franco, J., Schlipf, J.S.: Extending Existential Quantification in Conjunctions of BDDs. University of Cincinnati Technical Report"},{"key":"11_CR32","unstructured":"Weisstein, E.W., et al.: van der Waerden Number, From MathWorld\u2013A Wolfram Web Resource, http:\/\/mathworld.wolfram.com\/vanderWaerdenNumber.html"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11499107_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:00:53Z","timestamp":1605643253000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11499107_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540262763","9783540316794"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/11499107_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}