{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T21:34:52Z","timestamp":1742938492331,"version":"3.40.3"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030802226"},{"type":"electronic","value":"9783030802233"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-80223-3_12","type":"book-chapter","created":{"date-parts":[[2021,7,1]],"date-time":"2021-07-01T14:13:49Z","timestamp":1625148829000},"page":"171-187","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Efficient All-UIP Learned Clause Minimization"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1705-3083","authenticated-orcid":false,"given":"Mathias","family":"Fleury","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7170-9242","authenticated-orcid":false,"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,7,2]]},"reference":[{"key":"12_CR1","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: IJCAI, pp. 399\u2013404 (2009), http:\/\/ijcai.org\/Proceedings\/09\/Papers\/074.pdf"},{"key":"12_CR2","unstructured":"Biere, A.: CaDiCaL, Lingeling, Plingeling, Treengeling and YalSAT entering the SAT Competition 2018. In: Heule, M., J\u00e4rvisalo, M., Suda, M. (eds.) Proceedings of of SAT Competition 2018 - Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B, vol. B-2018-1, pp. 13\u201314. University of Helsinki (2018)"},{"key":"12_CR3","unstructured":"Biere, A.: Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. Technical Report, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University (August 2021)"},{"key":"12_CR4","unstructured":"Biere, A.: The SAT solver Satch. Git repository (2021). https:\/\/github.com\/arminbiere\/satch Accessed 03 2021"},{"key":"12_CR5","unstructured":"Biere, A., Fazekas, K., Fleury, M., Heisinger, M.: CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In: Balyo, T., Froleyks, N., Heule, M., Iser, M., J\u00e4rvisalo, M., Suda, M. (eds.) Proceedings of SAT Competition 2020 - Solver and Benchmark Descriptions. Department of Computer Science Report Series B, vol. B-2020-1, pp. 51\u201353. University of Helsinki (2020)"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/978-3-319-24318-4_29","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"A Biere","year":"2015","unstructured":"Biere, A., Fr\u00f6hlich, A.: Evaluating CDCL variable scoring schemes. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 405\u2013422. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24318-4_29"},{"key":"12_CR7","unstructured":"Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)"},{"key":"12_CR8","doi-asserted-by":"publisher","unstructured":"Cherkassky, B.V., Goldberg, A.V., Silverstein, C.: Buckets, heaps, lists, and monotone priority queues. SIAM J. Comput. 28(4), 1326\u20131346 (1999). https:\/\/doi.org\/10.1137\/S0097539796313490","DOI":"10.1137\/S0097539796313490"},{"key":"12_CR9","doi-asserted-by":"publisher","unstructured":"Dowling, W.F., Gallier, J.H.: Linear-time algorithms for testing the satisfiability of propositional Horn formulae. J. Log. Program. 1(3), 267\u2013284 (1984). https:\/\/doi.org\/10.1016\/0743-1066(84)90014-1","DOI":"10.1016\/0743-1066(84)90014-1"},{"key":"12_CR10","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. 2919, pp. 502\u2013518. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-030-51825-7_3","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2020","author":"N Feng","year":"2020","unstructured":"Feng, N., Bacchus, F.: Clause size reduction with all-UIP learning. In: Pulina, L., Seidl, M. (eds.) SAT 2020. LNCS, vol. 12178, pp. 28\u201345. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51825-7_3"},{"key":"12_CR12","unstructured":"Fleury, M.: Formalization of logical calculi in Isabelle\/HOL. Ph.D. thesis, Saarland University, Saarbr\u00fccken, Germany (2020). https:\/\/tel.archives-ouvertes.fr\/tel-02963301"},{"key":"12_CR13","unstructured":"Fleury, M., Biere, A.: Efficient all-UIP learned clause minimization (extended version). Technical Report. 21\/3, Johannes Kepler University Linz, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria (2021). https:\/\/doi.org\/10.350\/fmvtr.2021-3"},{"key":"12_CR14","unstructured":"Hickey, R., Feng, N., Bacchus, F.: Cadical-trail, Cadical-alluip, Cadical-alluip-trail and maple-LCM-dist-alluip-trail at the SAT competition. In: Balyo, T., Froleyks, N., Heule, M., Iser, M., J\u00e4rvisalo, M., Suda, M. (eds.) Proceedings of SAT Competition 2020 - Solver and Benchmark Descriptions. Department of Computer Science Report Series B, vol. B-2020-1, p. 10. University of Helsinki (2020)"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-030-24258-9_18","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2019","author":"S M\u00f6hle","year":"2019","unstructured":"M\u00f6hle, S., Biere, A.: Backing backtracking. In: Janota, M., Lynce, I. (eds.) SAT 2019. LNCS, vol. 11628, pp. 250\u2013266. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-24258-9_18"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-319-94144-8_7","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2018","author":"A Nadel","year":"2018","unstructured":"Nadel, A., Ryvchin, V.: Chronological backtracking. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 111\u2013121. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94144-8_7"},{"key":"12_CR17","doi-asserted-by":"publisher","unstructured":"Silva, J.P.M., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 131\u2013153. IOS Press (2009). https:\/\/doi.org\/10.3233\/978-1-58603-929-5-131","DOI":"10.3233\/978-1-58603-929-5-131"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-642-02777-2_23","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"N S\u00f6rensson","year":"2009","unstructured":"S\u00f6rensson, N., Biere, A.: Minimizing learned clauses. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 237\u2013243. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02777-2_23"},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-642-02777-2_15","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"A Gelder","year":"2009","unstructured":"Gelder, A.: Improved conflict-clause minimization leads to improved propositional proof traces. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 141\u2013146. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02777-2_15"},{"key":"12_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/978-3-642-21581-0_26","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"A Gelder","year":"2011","unstructured":"Gelder, A.: Generalized conflict-clause strengthening for satisfiability solvers. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 329\u2013342. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21581-0_26"},{"key":"12_CR21","doi-asserted-by":"publisher","unstructured":"Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient conflict driven learning in Boolean satisfiability solver. In: ICCAD, pp. 279\u2013285. IEEE Computer Society (2001). https:\/\/doi.org\/10.1109\/ICCAD.2001.968634","DOI":"10.1109\/ICCAD.2001.968634"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2021"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-80223-3_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,1]],"date-time":"2021-07-01T23:30:01Z","timestamp":1625182201000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-80223-3_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030802226","9783030802233"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-80223-3_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"2 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAT","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Theory and Applications of Satisfiability Testing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Barcelona","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sat2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.iiia.csic.es\/sat2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}