{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:41:44Z","timestamp":1742913704312,"version":"3.40.3"},"publisher-location":"Cham","reference-count":38,"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_22","type":"book-chapter","created":{"date-parts":[[2021,7,1]],"date-time":"2021-07-01T14:13:49Z","timestamp":1625148829000},"page":"315-331","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["On Dedicated CDCL Strategies for PB Solvers"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3221-9923","authenticated-orcid":false,"given":"Daniel","family":"Le Berre","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7200-4279","authenticated-orcid":false,"given":"Romain","family":"Wallon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,7,2]]},"reference":[{"key":"22_CR1","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1613\/jair.3152","volume":"40","author":"A Atserias","year":"2011","unstructured":"Atserias, A., Fichte, J.K., Thurley, M.: Clause-learning algorithms with many restarts and bounded-width resolution. JAIR 40, 353\u2013373 (2011)","journal-title":"JAIR"},{"key":"22_CR2","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Proceedings of IJCAI 2009, pp. 399\u2013404 (2009)"},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"Audemard, G., Simon, L.: Refining restarts strategies for SAT and UNSAT. In: Milano, M. (ed.) Proceedings of CP 2012, pp. 118\u2013126 (2012)","DOI":"10.1007\/978-3-642-33558-7_11"},{"key":"22_CR4","unstructured":"Biedenkapp, A., Bozkurt, H.F., Eimer, T., Hutter, F., Lindauer, M.: Dynamic algorithm configuration: foundation of a new meta-algorithmic framework. In: Proceedings of ECAI 2020 (2020)"},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"Biere, A.: Adaptive restart strategies for conflict driven SAT solvers. In: Proceedings of SAT 2008, pp. 28\u201333 (2008)","DOI":"10.1007\/978-3-540-79719-7_4"},{"issue":"2\u20134","key":"22_CR6","first-page":"75","volume":"4","author":"A Biere","year":"2008","unstructured":"Biere, A.: PicoSAT essentials. JSAT 4(2\u20134), 75\u201397 (2008)","journal-title":"JSAT"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"Biere, A., Fr\u00f6hlich, A.: Evaluating CDCL variable scoring schemes. In: Proceedings of SAT 2015, pp. 405\u2013422 (2015)","DOI":"10.1007\/978-3-319-24318-4_29"},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"Biere, A., Fr\u00f6hlich, A.: Evaluating CDCL Restart Schemes. In: Proceedings of Pragmatics of SAT 2015 and 2018. EPiC Series in Computing, vol. 59, pp. 1\u201317 (2019)","DOI":"10.29007\/89dw"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Chai, D., Kuehlmann, A.: A fast pseudo-Boolean constraint solver. IEEE Trans. CAD Integrated Circuits Syst., 305\u2013317 (2005)","DOI":"10.1109\/TCAD.2004.842808"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"Cook, W., Coullard, C.R., Tur\u00e1n, G.: On the complexity of cutting-plane proofs. Discrete Appl. Math., 25\u201338 (1987)","DOI":"10.1016\/0166-218X(87)90039-4"},{"key":"22_CR11","unstructured":"Dixon, H.: Automating pseudo-boolean inference within a DPLL framework. Ph.D. thesis, University of Oregon (2004)"},{"key":"22_CR12","unstructured":"Dixon, H.E., Ginsberg, M.L.: Inference methods for a pseudo-boolean satisfiability solver. In: Proceedings of AAAI 2002, pp. 635\u2013640 (2002)"},{"key":"22_CR13","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An Extensible SAT-solver. In: Proceedings of SAT 2004, pp. 502\u2013518 (2004)","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"Elffers, J., Gir\u00e1ldez-Cr\u00fa, J., Nordstr\u00f6m, J., Vinyals, M.: Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers. In: Proceedings of SAT 2018, pp. 75\u201393 (2018)","DOI":"10.1007\/978-3-319-94144-8_5"},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"Elffers, J., Gir\u00e1ldez-Cru, J., Gocht, S., Nordstr\u00f6m, J., Simon, L.: Seeking practical CDCL insights from theoretical SAT benchmarks. In: Proceedings of IJCAI 2018, pp. 1300\u20131308 (2018)","DOI":"10.24963\/ijcai.2018\/181"},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"Elffers, J., Nordstr\u00f6m, J.: Divide and conquer: towards faster pseudo-boolean solving. In: Proceedings of IJCAI 2018, pp. 1291\u20131299 (2018)","DOI":"10.24963\/ijcai.2018\/180"},{"key":"22_CR17","doi-asserted-by":"crossref","unstructured":"Gocht, S., Nordstr\u00f6m, J., Yehudayoff, A.: On Division Versus Saturation in Pseudo-Boolean Solving. In: Proceedings of IJCAI\u20192019. pp. 1711\u20131718 (2019)","DOI":"10.24963\/ijcai.2019\/237"},{"key":"22_CR18","unstructured":"Gomes, C.P., Selman, B., Kautz, H.: Boosting combinatorial search through randomization. In: Proceedings of AAAI 1998, pp. 431\u2013437 (1998)"},{"key":"22_CR19","doi-asserted-by":"crossref","unstructured":"Gomory, R.E.: Outline of an algorithm for integer solutions to linear programs. Bulletin of the American Mathematical Society, pp. 275\u2013278 (1958)","DOI":"10.1090\/S0002-9904-1958-10224-4"},{"key":"22_CR20","doi-asserted-by":"crossref","unstructured":"Haken, A.: The intractability of resolution. Theoretical Computer Science, pp. 297\u2013308 (1985)","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"22_CR21","doi-asserted-by":"crossref","unstructured":"Hooker, J.N.: Generalized resolution and cutting planes. Annals of Operations Research, pp. 217\u2013239 (1988)","DOI":"10.1007\/BF02186368"},{"key":"22_CR22","unstructured":"Huang, J.: The Effect of Restarts on the Efficiency of Clause Learning. In: Proceedings of IJCAI 2007, pp. 2318\u20132323 (2007)"},{"key":"22_CR23","doi-asserted-by":"crossref","unstructured":"Le Berre, D., Marquis, P., Mengel, S., Wallon, R.: On irrelevant literals in pseudo-boolean constraint learning. In: Proceedings of IJCAI 2020, pp. 1148\u20131154 (2020)","DOI":"10.24963\/ijcai.2020\/160"},{"key":"22_CR24","doi-asserted-by":"crossref","unstructured":"Le Berre, D., Marquis, P., Wallon, R.: On Weakening strategies for PB solvers. In: Proceedings of SAT 2020, pp. 322\u2013331 (2020)","DOI":"10.1007\/978-3-030-51825-7_23"},{"key":"22_CR25","doi-asserted-by":"crossref","unstructured":"Le Berre, D., Parrain, A.: The SAT4J library, Release 2.2, System Description. JSAT, pp. 59\u201364 (2010)","DOI":"10.3233\/SAT190075"},{"key":"22_CR26","unstructured":"Le Berre, D., Wallon, R.: On Dedicated CDCL Strategies for PB Solvers Companion Artifact, May 2021. https:\/\/doi.org\/10.5281\/zenodo.4751685"},{"key":"22_CR27","doi-asserted-by":"crossref","unstructured":"Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Learning rate based branching heuristic for SAT solvers. In: Proceedings of SAT 2016, pp. 123\u2013140 (2016)","DOI":"10.1007\/978-3-319-40970-2_9"},{"key":"22_CR28","doi-asserted-by":"crossref","unstructured":"Luby, M., Sinclair, A., Zuckerman, D.: Optimal speedup of Las Vegas algorithms. In: Information Processing Letters, pp. 173\u2013180 (1993)","DOI":"10.1016\/0020-0190(93)90029-9"},{"key":"22_CR29","doi-asserted-by":"crossref","unstructured":"Manquinho, V., Roussel, O.: The First Evaluation of Pseudo-Boolean Solvers (PB\u201905). JSAT, pp. 103\u2013143 (2006)","DOI":"10.3233\/SAT190018"},{"key":"22_CR30","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput., 220\u2013227 (1999)","DOI":"10.1109\/12.769433"},{"key":"22_CR31","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of DAC 2001, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"22_CR32","doi-asserted-by":"crossref","unstructured":"Nordstr\u00f6m, J.: On the interplay between proof complexity and SAT solving. ACM SIGLOG News, pp. 19\u201344 (2015)","DOI":"10.1145\/2815493.2815497"},{"issue":"2","key":"22_CR33","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1016\/j.artint.2010.10.002","volume":"175","author":"K Pipatsrisawat","year":"2011","unstructured":"Pipatsrisawat, K., Darwiche, A.: On the power of clause-learning SAT solvers as resolution engines. Artif. Intell. 175(2), 512\u2013525 (2011)","journal-title":"Artif. Intell."},{"key":"22_CR34","unstructured":"Roussel, O.: Pseudo-Boolean Competition 2016 (2016). http:\/\/www.cril.fr\/PB16\/. Accessed 20 May 2020"},{"key":"22_CR35","unstructured":"Roussel, O., Manquinho, V.M.: Pseudo-Boolean and Cardinality Constraints. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 695\u2013733. IOS Press (2009)"},{"key":"22_CR36","doi-asserted-by":"crossref","unstructured":"Sheini, H.M., Sakallah, K.A.: Pueblo: a hybrid pseudo-boolean SAT solver. JSAT, pp. 165\u2013189 (2006)","DOI":"10.3233\/SAT190020"},{"key":"22_CR37","doi-asserted-by":"crossref","unstructured":"Vinyals, M., Elffers, J., Gir\u00e1ldez-Cr\u00fa, J., Gocht, S., Nordstr\u00f6m, J.: In Between resolution and cutting planes: a study of proof systems for pseudo-boolean SAT solving. In: Proceedings of SAT 2018, pp. 292\u2013310 (2018)","DOI":"10.1007\/978-3-319-94144-8_18"},{"key":"22_CR38","doi-asserted-by":"crossref","unstructured":"Whittemore, J., Kim, J., Sakallah, K.A.: SATIRE: a new incremental satisfiability engine. In: Proceedings of DAC 2001, pp. 542\u2013545 (2001)","DOI":"10.1145\/378239.379019"}],"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_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,1]],"date-time":"2021-07-01T23:33:56Z","timestamp":1625182436000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-80223-3_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030802226","9783030802233"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-80223-3_22","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"}}]}}