{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T17:10:08Z","timestamp":1746378608028,"version":"3.40.4"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319112053"},{"type":"electronic","value":"9783319112060"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-11206-0_11","type":"book-chapter","created":{"date-parts":[[2014,9,15]],"date-time":"2014-09-15T01:31:55Z","timestamp":1410744715000},"page":"98-110","source":"Crossref","is-referenced-by-count":0,"title":["CDCL Solver Additions: Local Look-Ahead, All-Unit-UIP Learning and On-the-Fly Probing"],"prefix":"10.1007","author":[{"given":"Norbert","family":"Manthey","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","first-page":"399","volume-title":"IJCAI 2009","author":"G. Audemard","year":"2009","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Boutilier, C. (ed.) IJCAI 2009, pp. 399\u2013404. Morgan Kaufmann Publishers Inc., Pasadena (2009)"},{"unstructured":"Audemard, G., Simon, L.: Glucose 2.3 in the SAT 2013 competition. In: Balint, et al. (eds.) [3], pp. 42\u201343","key":"11_CR2"},{"unstructured":"Balint, A., Belov, A., Heule, M.J., J\u00e4rvisalo, M. (eds.): Proceedings of SAT Challenge 2013, Department of Computer Science Series of Publications B, vol. B-2013-1. University of Helsinki, Helsinki, Finland (2013)","key":"11_CR3"},{"unstructured":"Biere, A.: PrecoSAT system description (2009), http:\/\/fmv.jku.at\/precosat\/preicosat-sc09.pdf","key":"11_CR4"},{"unstructured":"Biere, A.: Lingeling, Plingeling and Treengeling entering the SAT competition 2013. In: Balint, et\u00a0al. (eds.) [3], pp. 51\u201352","key":"11_CR5"},{"volume-title":"Handbook of Satisfiability","year":"2009","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. IOS Press, Amsterdam (2009)","key":"11_CR6"},{"issue":"7","key":"11_CR7","doi-asserted-by":"publisher","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. Commun. ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/11499107_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2005","unstructured":"E\u00e9n, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 61\u201375. Springer, Heidelberg (2005)"},{"key":"11_CR9","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)"},{"issue":"1-2","key":"11_CR10","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1023\/A:1006314320276","volume":"24","author":"C.P. Gomes","year":"2000","unstructured":"Gomes, C.P., Selman, B., Crato, N., Kautz, H.: Heavy-tailed phenomena in satisfiability and constraint satisfaction problems. J. Autom. Reason.\u00a024(1-2), 67\u2013100 (2000)","journal-title":"J. Autom. Reason."},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-642-31087-4_18","volume-title":"Advanced Research in Applied Artificial Intelligence","author":"P. Gro\u00dfmann","year":"2012","unstructured":"Gro\u00dfmann, P., H\u00f6lldobler, S., Manthey, N., Nachtigall, K., Opitz, J., Steinke, P.: Solving periodic event scheduling problems with SAT. In: Jiang, H., Ding, W., Ali, M., Wu, X. (eds.) IEA\/AIE 2012. LNCS, vol.\u00a07345, pp. 166\u2013175. Springer, Heidelberg (2012)"},{"unstructured":"Han, H.J., Jin, H.S., Somenzi, F.: Clause simplification through dominator analysis. In: DATE, pp. 143\u2013148. IEEE (2011)","key":"11_CR12"},{"key":"11_CR13","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":"11_CR14","volume-title":"Handbook of Knowledge Representation","author":"F. van Harmelen","year":"2007","unstructured":"van Harmelen, F., Lifschitz, V., Porter, B.: Handbook of Knowledge Representation. Elsevier Science, San Diego (2007)"},{"unstructured":"Heule, M., van Maaren, H.: Look-ahead based SAT solvers. In: Biere, et\u00a0al. (eds.) [6], pp. 155\u2013184","key":"11_CR15"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-642-21581-0_17","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"M.J.H. Heule","year":"2011","unstructured":"Heule, M.J.H., J\u00e4rvisalo, M., Biere, A.: Efficient CNF simplification based on binary implication graphs. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol.\u00a06695, pp. 201\u2013215. Springer, Heidelberg (2011)"},{"key":"11_CR17","volume-title":"Stochastic Local Search: Foundations & Applications","author":"H. Hoos","year":"2004","unstructured":"Hoos, H., Sttzle, T.: Stochastic Local Search: Foundations & Applications. Morgan Kaufmann Publishers Inc., San Francisco (2004)"},{"unstructured":"Huang, J.: The effect of restarts on the efficiency of clause learning. In: IJCAI, pp. 2318\u20132323 (2007)","key":"11_CR18"},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1007\/978-3-642-25566-3_40","volume-title":"Learning and Intelligent Optimization","author":"F. Hutter","year":"2011","unstructured":"Hutter, F., Hoos, H.H., Leyton-Brown, K.: Sequential model-based optimization for general algorithm configuration. In: Coello Coello, C.A. (ed.) LION 2011. LNCS, vol.\u00a06683, pp. 507\u2013523. Springer, Heidelberg (2011)"},{"doi-asserted-by":"crossref","unstructured":"Jabbour, S., Lonlac, J., Sa\u00efs, L.: Adding new bi-asserting clauses for faster search in modern sat solvers. In: Frisch, A.M., Gregory, P. (eds.) SARA. AAAI (2013)","key":"11_CR20","DOI":"10.1007\/978-3-642-31612-8_50"},{"key":"11_CR21","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BF01531077","volume":"1","author":"R.G. Jeroslow","year":"1990","unstructured":"Jeroslow, R.G., Wang, J.: Solving propositional satisfiability problems. Annals of Mathematics and Artificial Intelligence\u00a01, 167\u2013187 (1990)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"11_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-642-21581-0_27","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"H. Katebi","year":"2011","unstructured":"Katebi, H., Sakallah, K.A., Marques-Silva, J.P.: Empirical study of the anatomy of modern SAT solvers. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol.\u00a06695, pp. 343\u2013356. Springer, Heidelberg (2011)"},{"doi-asserted-by":"crossref","unstructured":"Lynce, I., Marques-Silva, J.P.: Probing-based preprocessing techniques for propositional satisfiability. In: ICTAI 2003, pp. 105\u2013110. IEEE Computer Society (2003)","key":"11_CR23","DOI":"10.1109\/TAI.2003.1250177"},{"unstructured":"Manthey, N.: The SAT solver RISS3G at SC 2013. In: Balint, et\u00a0al. (eds.) [3], pp. 72\u201373","key":"11_CR24"},{"key":"11_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/978-3-642-31612-8_34","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"N. Manthey","year":"2012","unstructured":"Manthey, N.: Coprocessor 2.0 \u2013 A flexible CNF simplifier - (tool presentation). In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 436\u2013441. Springer, Heidelberg (2012)"},{"unstructured":"Marques-Silva, J.P., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere, et\u00a0al. (eds.) [6], ch.\u00a04, pp. 131\u2013153","key":"11_CR26"},{"issue":"5","key":"11_CR27","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J.P. Marques Silva","year":"1999","unstructured":"Marques Silva, J.P., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers\u00a048(5), 506\u2013521 (1999)","journal-title":"IEEE Transactions on Computers"},{"key":"11_CR28","first-page":"530","volume-title":"DAC 2001","author":"M.W. Moskewicz","year":"2001","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: DAC 2001, pp. 530\u2013535. ACM, New York (2001)"},{"unstructured":"Parkes, A.J.: Clustering at the phase transition. In: AAAI 1997\/IAAI 1997, pp. 340\u2013345. AAAI Press (1997)","key":"11_CR29"},{"unstructured":"Piette, C., Hamadi, Y., Sais, L.: Vivifying propositional clausal formulae. In: ECAI. Frontiers in Artificial Intelligence and Applications, vol.\u00a0178, pp. 525\u2013529 (2008)","key":"11_CR30"},{"key":"11_CR31","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":"4","key":"11_CR32","first-page":"133","volume":"7","author":"P. van der Tak","year":"2011","unstructured":"van der Tak, P., Ramos, A., Heule, M.: Reusing the assignment trail in cdcl solvers. JSAT\u00a07(4), 133\u2013138 (2011)","journal-title":"JSAT"},{"key":"11_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-642-39071-5_10","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"S. Wieringa","year":"2013","unstructured":"Wieringa, S., Heljanko, K.: Concurrent clause strengthening. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol.\u00a07962, pp. 116\u2013132. Springer, Heidelberg (2013)"},{"doi-asserted-by":"crossref","unstructured":"Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient conflict driven learning in boolean satisfiability solver. In: International Conference on Computer-Aided Design, pp. 279\u2013285 (2001)","key":"11_CR34","DOI":"10.1145\/774572.774637"}],"container-title":["Lecture Notes in Computer Science","KI 2014: Advances in Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-11206-0_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T16:32:51Z","timestamp":1746376371000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-11206-0_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319112053","9783319112060"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-11206-0_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}