{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T05:33:50Z","timestamp":1742967230875,"version":"3.40.3"},"publisher-location":"Cham","reference-count":8,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319662626"},{"type":"electronic","value":"9783319662633"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-66263-3_9","type":"book-chapter","created":{"date-parts":[[2017,8,8]],"date-time":"2017-08-08T04:05:11Z","timestamp":1502165111000},"page":"136-144","source":"Crossref","is-referenced-by-count":3,"title":["Coverage-Based Clause Reduction Heuristics for CDCL Solvers"],"prefix":"10.1007","author":[{"given":"Hidetomo","family":"Nabeshima","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Katsumi","family":"Inoue","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,8,9]]},"reference":[{"key":"9_CR1","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Proceedings of IJCAI-2009, pp. 399\u2013404 (2009)"},{"key":"9_CR2","unstructured":"Audemard, G., Simon, L.: Glucose 3.1 in the SAT 2014 competition (2014). \nhttp:\/\/satcompetition.org\/edacc\/sc14\/solver-description-download\/118\n\n. SAT Competition 2014 Solver Description"},{"key":"9_CR3","unstructured":"Bayardo Jr., R.J., Schrag, R.: Using CSP look-back techniques to solve real-world SAT instances. In: Proceedings of the 14th National Conference on Artificial Intelligence (AAAI 1997), pp. 203\u2013208 (1997)"},{"key":"9_CR4","unstructured":"Biere, A.: Lingeling and Friends at the SAT Competition 2011 (2011). \nhttp:\/\/fmv.jku.at\/papers\/biere-fmv-tr-11-1.pdf\n\n. SAT Competition 2011 Solver Description"},{"key":"9_CR5","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. 6695, pp. 343\u2013356. Springer, Heidelberg (2011). doi:\n10.1007\/978-3-642-21581-0_27"},{"issue":"5","key":"9_CR6","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"JP Marques-Silva","year":"1999","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. Comput."},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Nabeshima, H., Iwanuma, K., Inoue, K.: On-the-fly lazy clause simplification based on binary resolvents. In: ICTAI, pp. 987\u2013995. IEEE (2013)","DOI":"10.1109\/ICTAI.2013.149"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-319-24318-4_23","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"C Oh","year":"2015","unstructured":"Oh, C.: Between SAT and UNSAT: the fundamental difference in CDCL SAT. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 307\u2013323. Springer, Cham (2015). doi:\n10.1007\/978-3-319-24318-4_23"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2017"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66263-3_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,8,8]],"date-time":"2017-08-08T14:46:50Z","timestamp":1502203610000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66263-3_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319662626","9783319662633"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66263-3_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}