{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T22:46:22Z","timestamp":1768344382359,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642027765","type":"print"},{"value":"9783642027772","type":"electronic"}],"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_23","type":"book-chapter","created":{"date-parts":[[2009,6,26]],"date-time":"2009-06-26T06:58:18Z","timestamp":1245999498000},"page":"237-243","source":"Crossref","is-referenced-by-count":37,"title":["Minimizing Learned Clauses"],"prefix":"10.1007","author":[{"given":"Niklas","family":"S\u00f6rensson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"23_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-79719-7_3","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2008","author":"G. Audemard","year":"2008","unstructured":"Audemard, G., Bordeaux, L., Hamadi, Y., Jabbour, S., Sais, L.: A generalized framework for conflict analysis. In: Kleine B\u00fcning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol.\u00a04996, pp. 21\u201327. Springer, Heidelberg (2008)"},{"key":"23_CR2","doi-asserted-by":"crossref","unstructured":"Beame, P., Kautz, H., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. J.\u00a0Artif.\u00a0Intell.\u00a0Res.\u00a0(JAIR)\u00a022 (2004)","DOI":"10.1613\/jair.1410"},{"key":"23_CR3","doi-asserted-by":"crossref","unstructured":"Biere, A.: PicoSAT essentials. Journal on Satisfiability, Boolean Modeling and Computation (JSAT)\u00a04 (2008)","DOI":"10.3233\/SAT190039"},{"key":"23_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-540-72788-0_27","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"N. Dershowitz","year":"2007","unstructured":"Dershowitz, N., Hanna, Z., Nadel, A.: Towards a better understanding of the functionality of a conflict-driven SAT solver. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 287\u2013293. Springer, Heidelberg (2007)"},{"key":"23_CR5","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":"23_CR6","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)"},{"key":"23_CR7","unstructured":"Jin, H.S., Somenzi, F.: Strong conflict analysis for propositional satisfiability. In: Proc. DATE 2006 (2006)"},{"key":"23_CR8","volume-title":"Handbook of Satisfiability","author":"J. Marques-Silva","year":"2009","unstructured":"Marques-Silva, J., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Handbook of Satisfiability, IOS Press, Amsterdam (2009)"},{"key":"23_CR9","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J., Sakallah, K.: GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Trans.\u00a0on Computers\u00a048(5) (1999)","DOI":"10.1109\/12.769433"},{"key":"23_CR10","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proc.\u00a0DAC 2001 (2001)","DOI":"10.1145\/378239.379017"},{"key":"23_CR11","unstructured":"Nadel, A.: Understanding and Improving a Modern SAT Solver. PhD thesis, Tel Aviv University (submitted, 2008)"},{"key":"23_CR12","doi-asserted-by":"crossref","unstructured":"Pilarski, S., Hu, G.: Speeding up SAT for EDA. In: Proc.\u00a0DATE 2002 (2002)","DOI":"10.1109\/DATE.2002.998437"},{"key":"23_CR13","unstructured":"Pipatsrisawat, K., Darwiche, A.: A new clause learning scheme for efficient unsatisfiability proofs. In: Proc. AAAI 2008 (2008)"},{"key":"23_CR14","unstructured":"Sinz, C.: SAT-Race 2008 (2008), http:\/\/baldur.iti.uka.de\/sat-race-2008"},{"key":"23_CR15","unstructured":"S\u00f6rensson, N., E\u00e9n, N.: MS 2.1 and MS++ 1.0, SAT Race 2008 edn. (2008)"},{"key":"23_CR16","unstructured":"S\u00f6rensson, N., E\u00e9n, N.: MiniSat v1.13 \u2013 A SAT solver with conflict-clause minimization (2005)"},{"key":"23_CR17","unstructured":"Urquhart, A.: The complexity of propositional proofs. Bull.\u00a0of EATCS\u00a064 (1998)"},{"key":"23_CR18","doi-asserted-by":"crossref","unstructured":"Zhang, L., Madigan, C., Moskewicz, M., Malik, S.: Efficient conflict driven learning in boolean satisfiability solver. In: Proc.\u00a0ICCAD 2001 (2001)","DOI":"10.1145\/774572.774637"}],"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_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,20]],"date-time":"2020-05-20T01:26:09Z","timestamp":1589937969000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02777-2_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642027765","9783642027772"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02777-2_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}