{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,21]],"date-time":"2026-09-21T06:38:38Z","timestamp":1789972718505,"version":"4.0.1"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642381706","type":"print"},{"value":"9783642381713","type":"electronic"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38171-3_6","type":"book-chapter","created":{"date-parts":[[2013,4,11]],"date-time":"2013-04-11T01:30:36Z","timestamp":1365643836000},"page":"77-93","source":"Crossref","is-referenced-by-count":8,"title":["Revisiting Hyper Binary Resolution"],"prefix":"10.1007","author":[{"given":"Marijn J. H.","family":"Heule","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matti","family":"J\u00e4rvisalo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-3-540-24605-3_26","volume-title":"Theory and Applications of Satisfiability Testing","author":"F. Bacchus","year":"2004","unstructured":"Bacchus, F., Winter, J.: Effective preprocessing with hyper-resolution and equality reduction. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 341\u2013355. Springer, Heidelberg (2004)"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/11499107_34","volume-title":"Theory and Applications of Satisfiability Testing","author":"R. Gershman","year":"2005","unstructured":"Gershman, R., Strichman, O.: Cost-effective hyper-resolution for preprocessing CNF formulas. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 423\u2013429. Springer, Heidelberg (2005)"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/11527695_26","volume-title":"Theory and Applications of Satisfiability Testing","author":"M. Heule","year":"2005","unstructured":"Heule, M., Dufour, M., van Zwieten, J., van Maaren, H.: March_eq: Implementing additional reasoning into an efficient look-ahead SAT solver. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 345\u2013359. Springer, Heidelberg (2005)"},{"key":"6_CR4","unstructured":"Heule, M.J.H., van Maaren, H.: Chapter 5: Look-Ahead Based SAT Solvers. In: Handbook of Satisfiability, pp. 155\u2013184. IOS Press (2009)"},{"key":"6_CR5","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/s10472-005-0433-5","volume":"43","author":"A. Van Gelder","year":"2005","unstructured":"Van Gelder, A.: Toward leaner binary-clause reasoning in a satisfiability solver. Annals of Mathematics and Artificial Intelligence\u00a043, 239\u2013253 (2005)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"issue":"2","key":"6_CR6","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1137\/0201008","volume":"1","author":"A. Aho","year":"1972","unstructured":"Aho, A., Garey, M., Ullman, J.: The transitive reduction of a directed graph. SIAM Journal on Computing\u00a01(2), 131\u2013137 (1972)","journal-title":"SIAM Journal on Computing"},{"key":"6_CR7","unstructured":"Bacchus, F.: Enhancing Davis Putnam with extended binary clause reasoning. In: Proc. AAAI, pp. 613\u2013619. AAAI Press (2002)"},{"issue":"8","key":"6_CR8","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. Computers\u00a035(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Computers"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Kuehlmann, A., Krohm, F.: Equivalence checking using cuts and heaps. In: Proc. DAC, pp. 263\u2013268. ACM (1997)","DOI":"10.1145\/266021.266090"},{"issue":"1","key":"6_CR10","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/s10009-002-0102-5","volume":"5","author":"P.F. Williams","year":"2003","unstructured":"Williams, P.F., Andersen, H.R., Hulgaard, H.: Satisfiability checking using boolean expression diagrams. STTT\u00a05(1), 4\u201314 (2003)","journal-title":"STTT"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1007\/3-540-46419-0_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P.A. Abdulla","year":"2000","unstructured":"Abdulla, P.A., Bjesse, P., E\u00e9n, N.: Symbolic reachability analysis based on SAT-solvers. In: Graf, S., Schwartzbach, M. (eds.) TACAS\/ETAPS 2000. LNCS, vol.\u00a01785, pp. 411\u2013425. Springer, Heidelberg (2000)"},{"issue":"1","key":"6_CR12","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1023\/A:1008725524946","volume":"16","author":"M. Sheeran","year":"2000","unstructured":"Sheeran, M., St\u00e5lmarck, G.: A tutorial on St\u00e5lmarck\u2019s proof procedure for propositional logic. Formal Methods in System Design\u00a016(1), 23\u201358 (2000)","journal-title":"Formal Methods in System Design"},{"issue":"1","key":"6_CR13","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/0167-6377(92)90019-Y","volume":"12","author":"A. Billionnet","year":"1992","unstructured":"Billionnet, A., Sutter, A.: An efficient algorithm for the 3-satisfiability problem. Operations Research Letters\u00a012(1), 29\u201336 (1992)","journal-title":"Operations Research Letters"},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/BFb0017450","volume-title":"Principles and Practice of Constraint Programming - CP97","author":"C.M. Li","year":"1997","unstructured":"Li, C.M., Anbulagan: Look-ahead versus look-back for satisfiability problems. In: Smolka, G. (ed.) CP 1997. LNCS, vol.\u00a01330, pp. 341\u2013355. Springer, Heidelberg (1997)"},{"key":"6_CR15","unstructured":"Anbulagan, Pham, D.N., Slaney, J.K., Sattar, A.: Old resolution meets modern SLS. In: Proc. AAAI, pp. 354\u2013359 (2005)"},{"key":"6_CR16","unstructured":"Heule, M.J.H.: March: Towards a lookahead SAT solver for general purposes, MSc thesis (2004)"},{"key":"6_CR17","unstructured":"Biere, A.: P{re,i}coSAT@SC\u201909. In: SAT 2009 Competitive Event Booklet (2009)"},{"key":"6_CR18","unstructured":"Boufkhad, Y.: Aspects probabilistes et algorithmiques du probl\u00e8me de satisfaisabilit\u00e9, PhD thesis, Univertsit\u00e9 de Paris 6 (1996)"},{"key":"6_CR19","unstructured":"Simons, P.: Towards constraint satisfaction through logic programs and the stable model semantics, Report A47, Digital System Laboratory, Helsinki University of Technology (1997)"},{"key":"6_CR20","unstructured":"Mijnders, S., de Wilde, B., Heule, M.J.H.: Symbiosis of search and heuristics for random 3-SAT. In: Proc.\u00a0LaSh (2010)"},{"key":"6_CR21","unstructured":"Biere, A.: (Q)CompSAT and (Q)PicoSAT at the SAT\u201906 Race (2006)"},{"key":"6_CR22","unstructured":"Han, H., Jin, H., Somenzi, F.: Clause simplification through dominator analysis. In: Proc. DATE, pp. 143\u2013148. IEEE (2011)"},{"key":"6_CR23","unstructured":"Biere, A.: Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. FMV Report Series TR 10\/1, JKU, Linz, Austria (2010)"},{"key":"6_CR24","unstructured":"Soos, M.: CryptoMiniSat 2.5.0, SAT Race\u201910 solver description (2010)"},{"key":"6_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-02777-2_21","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"H. Han","year":"2009","unstructured":"Han, H., Somenzi, F.: On-the-fly clause improvement. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 209\u2013222. Springer, Heidelberg (2009)"},{"key":"6_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-642-31365-3_28","volume-title":"Automated Reasoning","author":"M. J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol.\u00a07364, pp. 355\u2013370. Springer, Heidelberg (2012)"},{"key":"6_CR27","doi-asserted-by":"crossref","unstructured":"Kunz, W., Pradhan, D.K.: Recursive learning: a new implication technique for efficient solutions to CAD problems-test, verification, and optimization. IEEE T-CAD 13(9) (1994)","DOI":"10.1109\/43.310903"},{"key":"6_CR28","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Chpt.\u00a026: SMT Modulo Theories. In: Handbook of Satisfiability. IOS Press (2009)"},{"key":"6_CR29","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J., Glass, T.: Combinational equivalence checking using satisfiability and recursive learning. In: Proc. DATE (1999)","DOI":"10.1145\/307418.307477"},{"issue":"1\/2","key":"6_CR30","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1023\/A:1006366304347","volume":"24","author":"J.F. Groote","year":"2000","unstructured":"Groote, J.F., Warners, J.P.: The propositional formula checker HeerHugo. J. Autom. Reasoning\u00a024(1\/2), 101\u2013125 (2000)","journal-title":"J. Autom. Reasoning"},{"key":"6_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-642-34188-5_8","volume-title":"Hardware and Software: Verification and Testing","author":"M.J.H. Heule","year":"2012","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.) HVC 2011. LNCS, vol.\u00a07261, pp. 50\u201365. Springer, Heidelberg (2012)"}],"container-title":["Lecture Notes in Computer Science","Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38171-3_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,29]],"date-time":"2020-12-29T01:05:35Z","timestamp":1609203935000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38171-3_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642381706","9783642381713"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38171-3_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}