{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T10:58:26Z","timestamp":1725533906886},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642027765"},{"type":"electronic","value":"9783642027772"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02777-2_32","type":"book-chapter","created":{"date-parts":[[2009,6,26]],"date-time":"2009-06-26T02:58:18Z","timestamp":1245985098000},"page":"341-355","source":"Crossref","is-referenced-by-count":6,"title":["Width-Based Restart Policies for Clause-Learning Satisfiability Solvers"],"prefix":"10.1007","author":[{"given":"Knot","family":"Pipatsrisawat","sequence":"first","affiliation":[]},{"given":"Adnan","family":"Darwiche","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Gomes, C.P., Selman, B., Crato, N.: Heavy-tailed distributions in combinatorial search. In: Principles and Practice of Constraint Programming, pp. 121\u2013135 (1997)","key":"32_CR1","DOI":"10.1007\/BFb0017434"},{"doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient sat solver. In: Proc. of DAC 2001, pp. 530\u2013535 (2001)","key":"32_CR2","DOI":"10.1145\/378239.379017"},{"key":"32_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible sat-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: Berkmin: A fast and robust sat-solver. In: DATE 2002, pp. 142\u2013149 (2002)","key":"32_CR4","DOI":"10.1109\/DATE.2002.998262"},{"unstructured":"Huang, J.: The effect of restarts on the efficiency of clause learning. In: Proc. of IJCAI 2007, pp. 2318\u20132323 (2007)","key":"32_CR5"},{"key":"32_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-79719-7_4","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2008","author":"A. Biere","year":"2008","unstructured":"Biere, A.: Adaptive restart strategies for conflict driven sat solvers. In: Kleine B\u00fcning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol.\u00a04996, pp. 28\u201333. Springer, Heidelberg (2008)"},{"key":"32_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-540-79719-7_25","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2008","author":"V. Ryvchin","year":"2008","unstructured":"Ryvchin, V., Strichman, O.: Local restarts. In: Kleine B\u00fcning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol.\u00a04996, pp. 271\u2013276. Springer, Heidelberg (2008)"},{"key":"32_CR8","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1613\/jair.1410","volume":"22","author":"P. Beame","year":"2004","unstructured":"Beame, P., Kautz, H., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. JAIR\u00a022, 319\u2013351 (2004)","journal-title":"JAIR"},{"issue":"2","key":"32_CR9","doi-asserted-by":"publisher","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\u2014resolution made simple. J. ACM\u00a048(2), 149\u2013169 (2001)","journal-title":"J. ACM"},{"unstructured":"Ryan, L.: Efficient Algorithms for Clause-Learning SAT Solvers. Master\u2019s thesis, Simon Fraser University (2004)","key":"32_CR10"},{"unstructured":"Zhang, L., Malik, S.: Validating sat solvers using an independent resolution-based checker: Practical implementations and other applications. In: DATE 2003, pp. 880\u2013885 (2003)","key":"32_CR11"},{"issue":"3","key":"32_CR12","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(3), 444\u2013459 (1977)","journal-title":"SIAM Journal on Computing"},{"doi-asserted-by":"crossref","unstructured":"Beame, P., Pitassi, T.: Simplified and improved resolution lower bounds. In: Annual IEEE Symposium on Foundations of Computer Science, p. 274 (1996)","key":"32_CR13","DOI":"10.1109\/SFCS.1996.548486"},{"doi-asserted-by":"crossref","unstructured":"Mahajan, Y.S., Fu, Z., Malik, S.: Zchaff2004: An efficient sat solver. In: Proc. of SAT 2005, pp. 360\u2013375 (2005)","key":"32_CR14","DOI":"10.1007\/11527695_27"},{"unstructured":"Nadel, A., Gordon, M., Patti, A., Hanna, Z.: Eureka-2006 sat solver Solver description for SAT-Race 2006 (2006)","key":"32_CR15"},{"doi-asserted-by":"crossref","unstructured":"Biere, A.: Picosat essentials. JSAT, 75\u201397 (2008)","key":"32_CR16","DOI":"10.3233\/SAT190039"},{"key":"32_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"839","DOI":"10.1007\/978-3-540-74970-7_62","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2007","author":"J. Huang","year":"2007","unstructured":"Huang, J.: A case for simple SAT solvers. In: Bessi\u00e8re, C. (ed.) CP 2007. LNCS, vol.\u00a04741, pp. 839\u2013846. Springer, Heidelberg (2007)"},{"unstructured":"Pipatsrisawat, K., Darwiche, A.: Rsat 2.0: Sat solver description. Technical Report D\u2013153, Automated Reasoning Group, Computer Science Department, UCLA (2007)","key":"32_CR18"},{"unstructured":"S\u00f6rensson, N., E\u00e9n, N.: Minisat 2.1 and minisat++ 1.0\u2013sat race 2008 editions (2008)","key":"32_CR19"},{"issue":"4","key":"32_CR20","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/s00493-004-0036-5","volume":"24","author":"E. Ben-Sasson","year":"2004","unstructured":"Ben-Sasson, E., Impagliazzo, R., Wigderson, A.: Near optimal separation of tree-like and general resolution. Combinatorica\u00a024(4), 585\u2013603 (2004)","journal-title":"Combinatorica"},{"key":"32_CR21","series-title":"Lecture Notes in Computer Science","first-page":"371","volume-title":"Computer Aided Verification","author":"D. Babi\u0107","year":"2007","unstructured":"Babi\u0107, D., Hu, A.J.: Structural Abstraction of Software Verification Conditions. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 371\u2013383. Springer, Heidelberg (2007)"},{"doi-asserted-by":"crossref","unstructured":"Babi\u0107, D., Hu, A.J.: Calysto: Scalable and Precise Extended Static Checking. In: Proc. of ICSE 2008, pp. 211\u2013220 (2008)","key":"32_CR22","DOI":"10.1145\/1368088.1368118"},{"unstructured":"Hertel, A., Urquhart, A.: Comments on eccc report tr06-133: The resolution width problem is exptime-complete. Technical Report TR09-003, ECCC (2009)","key":"32_CR23"},{"key":"32_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-72788-0_28","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"K. Pipatsrisawat","year":"2007","unstructured":"Pipatsrisawat, K., Darwiche, A.: A lightweight component caching scheme for satisfiability solvers. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 294\u2013299. Springer, Heidelberg (2007)"},{"issue":"3","key":"32_CR25","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/0004-3702(90)90046-3","volume":"41","author":"R. Dechter","year":"1990","unstructured":"Dechter, R.: Enhancement schemes for constraint processing: backjumping, learning, and cutset decomposition. Artif. Intell.\u00a041(3), 273\u2013312 (1990)","journal-title":"Artif. Intell."},{"unstructured":"Bayardo, R.J., Miranker, D.P.: A complexity analysis of space-bounded learning algorithms for the constraint satisfaction problem. In: AAAI 1996, pp. 298\u2013304 (1996)","key":"32_CR26"},{"unstructured":"Bayardo, R.J.J., Schrag, R.C.: Using CSP look-back techniques to solve real-world SAT instances. In: Proc. of AAAI 1997, Providence, Rhode Island, pp. 203\u2013208 (1997)","key":"32_CR27"},{"unstructured":"Nadel, A.: Backtrack search algorithms for propositional logic satisfiability: Review and innovations. Master\u2019s thesis, The Hebrew University (2002)","key":"32_CR28"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing - SAT 2009"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02777-2_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,19]],"date-time":"2020-05-19T21:26:17Z","timestamp":1589923577000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02777-2_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642027765","9783642027772"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02777-2_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}