{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T13:05:05Z","timestamp":1760101505317,"version":"3.40.3"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031606977"},{"type":"electronic","value":"9783031606984"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-60698-4_1","type":"book-chapter","created":{"date-parts":[[2024,5,27]],"date-time":"2024-05-27T00:01:51Z","timestamp":1716768111000},"page":"3-20","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Structure-Guided Cube-and-Conquer for\u00a0MaxSAT"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6475-5512","authenticated-orcid":false,"given":"Max","family":"Bannach","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0131-6771","authenticated-orcid":false,"given":"Markus","family":"Hecher","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,5,26]]},"reference":[{"key":"1_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1007\/978-3-319-59776-8_30","volume-title":"Integration of AI and OR Techniques in Constraint Programming","author":"M Abseher","year":"2017","unstructured":"Abseher, M., Musliu, N., Woltran, S.: htd - a free, open-source framework for (customized) tree decompositions and beyond. In: Salvagnin, D., Lombardi, M. (eds.) CPAIOR 2017. LNCS, vol. 10335, pp. 376\u2013386. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-59776-8_30"},{"key":"1_CR2","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/s10732-022-09495-3","volume":"28","author":"C Ans\u00f3tegui","year":"2022","unstructured":"Ans\u00f3tegui, C., Many\u00e0, F., Ojeda, J., Salvia, J.M., Torres, E.: Incomplete MaxSAT approaches for combinatorial testing. J. Heuristics 28, 377\u2013431 (2022). https:\/\/doi.org\/10.1007\/s10732-022-09495-3","journal-title":"J. Heuristics"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Bannach, M., Skambath, M., Tantau, T.: On the parallel parameterized complexity of MaxSAT variants. In: SAT (2022)","DOI":"10.1613\/jair.1.14748"},{"key":"1_CR4","unstructured":"Bannach, M., Hecher, M.: Torsomaxsat. http:\/\/github.com\/maxbannach\/TorsoMaxSAT"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-031-38499-8_1","volume-title":"Automated Deduction","author":"J Berg","year":"2023","unstructured":"Berg, J., Bogaerts, B., Nordstr\u00f6m, J., Oertel, A., Vandesande, D.: Certified core-guided MaxSAT solving. In: Pientka, B., Tinelli, C. (eds.) CADE 2023. LNCS, vol. 14132, pp. 1\u201322. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-38499-8_1"},{"key":"1_CR6","unstructured":"Berg, J., Hyttinen, A., J\u00e4rvisalo, M.: Applications of MaxSAT in data analysis. In: SAT (2018)"},{"key":"1_CR7","unstructured":"Berg, J., J\u00e4rvisalo, M., Martins, R., Niskanen, A. (eds.): MaxSAT Evaluation 2023: Solver and Benchmark Descriptions. University of Helsinki (2023)"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Bestuzheva, K., et\u00a0al.: Enabling research through the SCIP optimization suite 8.0. ACM Trans. Math. Softw. (2023)","DOI":"10.1145\/3585516"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Biere, A.: Preprocessing and inprocessing techniques in SAT. In: HVC (2011)","DOI":"10.1007\/978-3-642-34188-5_1"},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, 2nd edn. IOS Press (2021)","DOI":"10.3233\/FAIA336"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Bofill, M., et al.: Constraint solving approaches to the business-to-business meeting scheduling problem. J. Artif. Intell. Res. (2022)","DOI":"10.24963\/ijcai.2023\/768"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"Ciampiconi, L., Ghosh, B., Scarlett, J., Meel, K.S.: A MaxSAT-based framework for group testing. In: IAAI (2020)","DOI":"10.1609\/aaai.v34i06.6574"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"D\u2019Almeida, D., Gr\u00e9goire, \u00c9.: Model-based diagnosis with default information implemented through MaxSAT technology. In: IEEE (2012)","DOI":"10.1109\/IRI.2012.6302987"},{"key":"1_CR14","unstructured":"Davies, J.: Solving MaxSAT by decoupling optimization and satisfaction. Ph.D. thesis, University of Toronto (2014)"},{"key":"1_CR15","unstructured":"Dell, H., Husfeldt, T., Jansen, B.M.P., Kaski, P., Komusiewicz, C., Rosamond, F.A.: The first parameterized algorithms and computational experiments challenge. In: IPEC (2016)"},{"key":"1_CR16","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2022.103810","volume":"314","author":"JK Fichte","year":"2023","unstructured":"Fichte, J.K., Hecher, M., Morak, M., Thier, P., Woltran, S.: Solving projected model counting by utilizing treewidth and its limits. Artif. Intell. 314, 103810 (2023)","journal-title":"Artif. Intell."},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Froleyks, N., et al.: SAT competition 2020. Artif. Intell. (2021)","DOI":"10.1016\/j.artint.2021.103572"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Fu, Z., Malik, S.: On solving the partial MaxSAT problem. In: SAT (2006)","DOI":"10.1007\/11814948_25"},{"key":"1_CR19","unstructured":"Ganian, R., Ramanujan, M.S., Szeider, S.: Combining treewidth and backdoors for CSP. In: STACS. LIPIcs, vol.\u00a066, pp. 36:1\u201336:17. Dagstuhl (2017)"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Gebser, M., Kaminski, R., Kaufmann, B., Schaub, T.: Answer Set Solving in Practice. Morgan & Claypool (2012)","DOI":"10.1007\/978-3-031-01561-8"},{"key":"1_CR21","doi-asserted-by":"crossref","unstructured":"Hagberg, A., Swart, P.J., Schult, D.A.: Exploring Network Structure, Dynamics, and Function Using NetworkX (2008)","DOI":"10.25080\/TCWV9851"},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-642-34188-5_8","volume-title":"Hardware and Software: Verification and Testing","author":"MJH Heule","year":"2012","unstructured":"Heule, M.J.H., Kullmann, O., Wieringa, S., Biere, A.: Cube and conquer: guiding CDCL SAT solvers by lookaheads. In: Eder, K., Lourenco, J., Shehory, O. (eds.) HVC 2011. LNCS, vol. 7261, pp. 50\u201365. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-34188-5_8"},{"key":"1_CR23","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-319-63516-3_2","volume-title":"Handbook of Parallel Constraint Reasoning","author":"MJH Heule","year":"2018","unstructured":"Heule, M.J.H., Kullmann, O., Biere, A.: Cube-and-conquer for satisfiability. In: Hamadi, Y., Sais, L. (eds.) Handbook of Parallel Constraint Reasoning, pp. 31\u201359. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-63516-3_2"},{"key":"1_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/978-3-319-94144-8_26","volume-title":"Theory and Applications of Satisfiability Testing","author":"A Ignatiev","year":"2018","unstructured":"Ignatiev, A., Morgado, A., Marques-Silva, J.: PySAT: a Python toolkit for prototyping with SAT oracles. In: Beyersdorff, O., Wintersteiger, C. (eds.) SAT 2018. LNCS, vol. 10929, pp. 428\u2013437. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94144-8_26"},{"key":"1_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"786","DOI":"10.1007\/978-3-319-57529-2_61","volume-title":"Advances in Knowledge Discovery and Data Mining","author":"S Jabbour","year":"2017","unstructured":"Jabbour, S., Mhadhbi, N., Raddaoui, B., Sais, L.: A SAT-based framework for overlapping community detection in networks. In: Kim, J., Shim, K., Cao, L., Lee, J.G., Lin, X., Moon, Y.S. (eds.) PAKDD 2017. LNCS, vol. 10235, pp. 786\u2013798. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-57529-2_61"},{"key":"1_CR26","volume-title":"Software Abstractions - Logic, Language, and Analysis","author":"D Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions - Logic, Language, and Analysis. MIT Press, Cambridge (2006)"},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"Jose, M., Majumdar, R.: Cause clue clauses: error localization using maximum satisfiability. In: SIGPLAN (2011)","DOI":"10.1145\/1993498.1993550"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Li, Y., Lin, S., Nishizawa, S., Onodera, H.: MCell: multi-row cell layout synthesis with resource constrained MaxSAT based detailed routing. In: ICCAD (2020)","DOI":"10.1145\/3400302.3415612"},{"key":"1_CR29","doi-asserted-by":"crossref","unstructured":"Many\u00e0, F., Negrete, S., Roig, C., Soler, J.R.: Solving the team composition problem in a classroom. Fundam. Informaticae (2020)","DOI":"10.3233\/FI-2020-1933"},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"Marx, D., O\u2019Sullivan, B., Razgon, I.: Finding small separators in linear time via treewidth reduction. ACM Trans. Algorithms (2013)","DOI":"10.1145\/2500119"},{"key":"1_CR31","unstructured":"Orvalho, P., Manquinho, V.M., Martins, R.: UpMax: user partitioning for MaxSAT. In: SAT (2023)"},{"key":"1_CR32","unstructured":"Papadimitriou, C.H.: Computational Complexity. Academic Internet Publ. (2007)"},{"key":"1_CR33","unstructured":"Perron, L., Furnon, V.: Or-tools. https:\/\/developers.google.com\/optimization\/"},{"key":"1_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/11889205_36","volume-title":"Principles and Practice of Constraint Programming","author":"M Samer","year":"2006","unstructured":"Samer, M., Szeider, S.: Constraint satisfaction with bounded treewidth revisited. In: Benhamou, F. (ed.) CP 2006. LNCS, vol. 4204, pp. 499\u2013513. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11889205_36"},{"key":"1_CR35","unstructured":"Strasser, B.: Computing Tree Decompositions with FlowCutter: PACE 2017 Submission. CoRR abs\/1709.08949 (2017)"},{"key":"1_CR36","doi-asserted-by":"crossref","unstructured":"Zhang, C., et\u00a0al.: AlloyMax: bringing maximum satisfaction to relational specifications. In: ESEC\/FSE (2021)","DOI":"10.1145\/3468264.3468587"},{"key":"1_CR37","unstructured":"Zhang, L., Bacchus, F.: MaxSAT heuristics for cost optimal planning. In: AAAI (2012)"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-60698-4_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,20]],"date-time":"2024-11-20T01:24:02Z","timestamp":1732065842000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-60698-4_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031606977","9783031606984"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-60698-4_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 May 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Moffett Field, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 June 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 June 2024","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":"nfm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}