{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T11:39:19Z","timestamp":1791459559081,"version":"4.3.4"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030581114","type":"print"},{"value":"9783030581121","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-58112-1_26","type":"book-chapter","created":{"date-parts":[[2020,9,2]],"date-time":"2020-09-02T16:04:30Z","timestamp":1599062670000},"page":"373-389","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["PbO-CCSAT: Boosting Local Search for Satisfiability Using Programming by Optimisation"],"prefix":"10.1007","author":[{"given":"Chuan","family":"Luo","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Holger","family":"Hoos","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shaowei","family":"Cai","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,8,31]]},"reference":[{"key":"26_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1007\/978-3-642-14186-7_3","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"A Balint","year":"2010","unstructured":"Balint, A., Fr\u00f6hlich, A.: Improving stochastic local search for SAT with a new probability distribution. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 10\u201315. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14186-7_3"},{"key":"26_CR2","unstructured":"Balyo, T., Heule, M.J.H., J\u00e4rvisalo, M. (eds.): Proceedings of SAT Competition 2017: Solver and Benchmark Descriptions. University of Helsinki (2017)"},{"key":"26_CR3","unstructured":"Biere, A.: CaDiCaL, Lingeling, Plingeling, Treengeling and YalSAT entering the SAT competition 2017. In: Proceedings of SAT Competition 2017: Solver and Benchmark Descriptions, pp. 14\u201315 (2017)"},{"key":"26_CR4","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1613\/jair.4480","volume":"51","author":"S Cai","year":"2014","unstructured":"Cai, S., Luo, C., Su, K.: Scoring functions based on second level score for k-SAT with long clauses. J. Artif. Intell. Res. 51, 413\u2013441 (2014)","journal-title":"J. Artif. Intell. Res."},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"Cai, S., Su, K.: Configuration checking with aspiration in local search for SAT. In: 2012 Proceedings of AAAI, pp. 434\u2013440 (2012)","DOI":"10.1609\/aaai.v26i1.8133"},{"key":"26_CR6","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/j.artint.2013.09.001","volume":"204","author":"S Cai","year":"2013","unstructured":"Cai, S., Su, K.: Local search for Boolean satisfiability with configuration checking and subscore. Artif. Intell. 204, 75\u201398 (2013)","journal-title":"Artif. Intell."},{"key":"26_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-3-642-39071-5_22","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"O Gableske","year":"2013","unstructured":"Gableske, O.: On the interpolation between product-based message passing heuristics for SAT. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 293\u2013308. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39071-5_22"},{"key":"26_CR8","unstructured":"Gent, I.P., Walsh, T.: Towards an understanding of hill-climbing procedures for SAT. In: 1993 Proceedings of AAAI, pp. 28\u201333 (1993)"},{"key":"26_CR9","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/j.artint.2016.06.001","volume":"238","author":"J Gir\u00e1ldez-Cru","year":"2016","unstructured":"Gir\u00e1ldez-Cru, J., Levy, J.: Generating SAT instances with community structure. Artif. Intell. 238, 119\u2013134 (2016)","journal-title":"Artif. Intell."},{"key":"26_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-319-40970-2_15","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"MJH Heule","year":"2016","unstructured":"Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the boolean pythagorean triples problem via Cube-and-Conquer. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 228\u2013245. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_15"},{"key":"26_CR11","unstructured":"Hoos, H.H.: On the run-time behaviour of stochastic local search algorithms for SAT. In: 1999 Proceedings of AAAI, pp. 661\u2013666 (1999)"},{"issue":"2","key":"26_CR12","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1145\/2076450.2076469","volume":"55","author":"HH Hoos","year":"2012","unstructured":"Hoos, H.H.: Programming by optimization. Commun. ACM 55(2), 70\u201380 (2012)","journal-title":"Commun. ACM"},{"key":"26_CR13","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, C.A.C. (ed.) LION 2011. LNCS, vol. 6683, pp. 507\u2013523. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-25566-3_40"},{"key":"26_CR14","doi-asserted-by":"crossref","unstructured":"Ishtaiwi, A., Thornton, J., Sattar, A., Pham, D.N.: Neighbourhood clause weight redistribution in local search for SAT. In: 2005 Proceedings of CP, pp. 772\u2013776 (2005)","DOI":"10.1007\/11564751_62"},{"key":"26_CR15","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1016\/j.artint.2015.11.002","volume":"232","author":"AR KhudaBukhsh","year":"2016","unstructured":"KhudaBukhsh, A.R., Xu, L., Hoos, H.H., Leyton-Brown, K.: SATenstein: automatically building local search SAT solvers from components. Artif. Intell. 232, 20\u201342 (2016)","journal-title":"Artif. Intell."},{"key":"26_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-642-31612-8_43","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"CM Li","year":"2012","unstructured":"Li, C.M., Li, Yu.: Satisfying versus falsifying in local search for satisfiability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 477\u2013478. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_43"},{"key":"26_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-319-40970-2_9","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"JH Liang","year":"2016","unstructured":"Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Learning rate based branching heuristic for SAT solvers. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 123\u2013140. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_9"},{"issue":"5","key":"26_CR18","first-page":"1014","volume":"45","author":"C Luo","year":"2015","unstructured":"Luo, C., Cai, S., Su, K., Wu, W.: Clause states based configuration checking in local search for satisfiability. IEEE Trans. Cybern. 45(5), 1014\u20131027 (2015)","journal-title":"IEEE Trans. Cybern."},{"key":"26_CR19","doi-asserted-by":"crossref","unstructured":"Luo, C., Cai, S., Wu, W., Su, K.: Double configuration checking in stochastic local search for satisfiability. In: 2014 Proceedings of AAAI, pp. 2703\u20132709 (2014)","DOI":"10.1609\/aaai.v28i1.9110"},{"key":"26_CR20","doi-asserted-by":"crossref","unstructured":"Luo, C., Hoos, H.H., Cai, S., Lin, Q., Zhang, H., Zhang, D.: Local search with efficient automatic configuration for minimum vertex cover. In: 2019 Proceedings of IJCAI, pp. 1297\u20131304 (2019)","DOI":"10.24963\/ijcai.2019\/180"},{"key":"26_CR21","doi-asserted-by":"crossref","unstructured":"Luo, M., Li, C., Xiao, F., Many\u00e0, F., L\u00fc, Z.: An effective learnt clause minimization approach for CDCL SAT solvers. In: 2017 Proceedings of IJCAI, pp. 703\u2013711 (2017)","DOI":"10.24963\/ijcai.2017\/98"},{"key":"26_CR22","unstructured":"McAllester, D.A., Selman, B., Kautz, H.A.: Evidence for invariants in local search. In: 1997 Proceedings of AAAI, pp. 321\u2013326 (1997)"},{"key":"26_CR23","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"},{"issue":"1","key":"26_CR24","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/3107548","volume":"61","author":"N Newman","year":"2018","unstructured":"Newman, N., Fr\u00e9chette, A., Leyton-Brown, K.: Deep optimization for spectrum repacking. Commun. ACM 61(1), 97\u2013104 (2018)","journal-title":"Commun. ACM"},{"issue":"3","key":"26_CR25","doi-asserted-by":"publisher","first-page":"608","DOI":"10.1007\/s10703-017-0295-6","volume":"51","author":"A Niemetz","year":"2017","unstructured":"Niemetz, A., Preiner, M., Biere, A.: Propagation based local search for bit-precise reasoning. Formal Methods Syst. Des. 51(3), 608\u2013636 (2017). https:\/\/doi.org\/10.1007\/s10703-017-0295-6","journal-title":"Formal Methods Syst. Des."},{"key":"26_CR26","unstructured":"Oh, C.: COMiniSatPS Pulsar and GHackCOMSPS. In: Proceedings of SAT Competition 2017: Solver and Benchmark Descriptions, pp. 12\u201313 (2017)"},{"key":"26_CR27","doi-asserted-by":"crossref","unstructured":"Pham, D.N., Duong, T., Sattar, A.: Trap avoidance in local search using pseudo-conflict learning. In: 2012 Proceedings of AAAI, pp. 542\u2013548 (2012)","DOI":"10.1609\/aaai.v26i1.8149"},{"issue":"4","key":"26_CR28","doi-asserted-by":"publisher","first-page":"139","DOI":"10.3233\/SAT190083","volume":"7","author":"O Roussel","year":"2011","unstructured":"Roussel, O.: Controlling a solver execution with the runsolver tool. J. Satisfiability Boolean Mode. Comput. 7(4), 139\u2013144 (2011)","journal-title":"J. Satisfiability Boolean Mode. Comput."},{"key":"26_CR29","unstructured":"Selman, B., Levesque, H.J., Mitchell, D.G.: A new method for solving hard satisfiability problems. In: 1992 Proceedings of AAAI, pp. 440\u2013446 (1992)"},{"key":"26_CR30","unstructured":"Thornton, J., Pham, D.N., Bain, S., Ferreira Jr., V.: Additive versus multiplicative clause weighting for SAT. In: 2004 Proceedings of AAAI, pp. 191\u2013196 (2004)"},{"key":"26_CR31","unstructured":"Yolcu, E., P\u00f3czos, B.: Learning local search heuristics for Boolean satisfiability. In: 2019 Proceedings of NeurIPS, pp. 7990\u20138001 (2019)"}],"container-title":["Lecture Notes in Computer Science","Parallel Problem Solving from Nature \u2013 PPSN XVI"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-58112-1_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,16]],"date-time":"2022-11-16T01:41:15Z","timestamp":1668562875000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-58112-1_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030581114","9783030581121"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-58112-1_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"31 August 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"PPSN","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Parallel Problem Solving from Nature","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Leiden","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"The Netherlands","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 September 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ppsn2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ppsn2020.liacs.leidenuniv.nl\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"268","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"99","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"37% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2.2","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}