{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,11]],"date-time":"2025-06-11T04:08:33Z","timestamp":1749614913875,"version":"3.41.0"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319449524"},{"type":"electronic","value":"9783319449531"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","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":[[2016]]},"DOI":"10.1007\/978-3-319-44953-1_30","type":"book-chapter","created":{"date-parts":[[2016,8,22]],"date-time":"2016-08-22T15:12:23Z","timestamp":1471878743000},"page":"473-482","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["On Incremental Core-Guided MaxSAT Solving"],"prefix":"10.1007","author":[{"given":"Xujie","family":"Si","sequence":"first","affiliation":[]},{"given":"Xin","family":"Zhang","sequence":"additional","affiliation":[]},{"given":"Vasco","family":"Manquinho","sequence":"additional","affiliation":[]},{"given":"Mikol\u00e1\u0161","family":"Janota","sequence":"additional","affiliation":[]},{"given":"Alexey","family":"Ignatiev","sequence":"additional","affiliation":[]},{"given":"Mayur","family":"Naik","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,8,23]]},"reference":[{"key":"30_CR1","unstructured":"Alviano, M., Dodaro, C., Ricca, F.: A MaxSAT algorithm using cardinality constraints of bounded size. In: IJCAI (2015)"},{"key":"30_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-642-33558-7_9","volume-title":"Principles and Practice of Constraint Programming","author":"C Ans\u00f3tegui","year":"2012","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., Gab\u00e0s, J., Levy, J.: Improving SAT-Based weighted MaxSAT solvers. In: Milano, M. (ed.) CP 2012. LNCS, vol. 7514, pp. 86\u2013101. Springer, Heidelberg (2012)"},{"key":"30_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-642-02777-2_39","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"C Ans\u00f3tegui","year":"2009","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., Levy, J.: Solving (weighted) partial MaxSAT through satisfiability testing. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 427\u2013440. Springer, Heidelberg (2009)"},{"key":"30_CR4","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/j.artint.2013.01.002","volume":"196","author":"C Ans\u00f3tegui","year":"2013","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., Levy, J.: SAT-based MaxSAT algorithms. Artif. Intell. 196, 77\u2013105 (2013)","journal-title":"Artif. Intell."},{"key":"30_CR5","unstructured":"Ans\u00f3tegui, C., Didier, F., Gab\u00e0s, J.: Exploiting the structure of unsatisfiable cores in MaxSAT. In: IJCAI (2015)"},{"key":"30_CR6","doi-asserted-by":"crossref","unstructured":"Bjorner, N., Narodytska, N.: Maximum satisfiability using cores and correction sets. In: IJCAI (2015)","DOI":"10.1609\/aaai.v28i1.9124"},{"key":"30_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-642-39071-5_12","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"A Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: A modular approach to MaxSAT modulo theories. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 150\u2013165. Springer, Heidelberg (2013)"},{"key":"30_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-642-23786-7_19","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2011","author":"J Davies","year":"2011","unstructured":"Davies, J., Bacchus, F.: Solving MAXSAT by solving a sequence of simpler SAT instances. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 225\u2013239. Springer, Heidelberg (2011)"},{"key":"30_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-642-39071-5_13","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"J Davies","year":"2013","unstructured":"Davies, J., Bacchus, F.: Exploiting the power of mip solvers in maxsat. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 166\u2013181. Springer, Heidelberg (2013)"},{"key":"30_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)"},{"issue":"4","key":"30_CR11","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1016\/S1571-0661(05)82542-3","volume":"89","author":"N E\u00e9n","year":"2003","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Temporal induction by incremental SAT solving. Electr. Notes Theor. Comput. Sci. 89(4), 543\u2013560 (2003)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"30_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/11814948_25","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"Z Fu","year":"2006","unstructured":"Fu, Z., Malik, S.: On solving the partial MAX-SAT problem. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 252\u2013265. Springer, Heidelberg (2006)"},{"key":"30_CR13","doi-asserted-by":"crossref","unstructured":"Grigore, R., Yang, H.: Abstraction refinement guided by a learnt probabilistic model. In: POPL (2016)","DOI":"10.1145\/2837614.2837663"},{"key":"30_CR14","doi-asserted-by":"crossref","unstructured":"Heras, F., Morgado, A., Marques-Silva, J.: Core-guided binary search algorithms for maximum satisfiability. In: AAAI (2011)","DOI":"10.1609\/aaai.v25i1.7822"},{"key":"30_CR15","doi-asserted-by":"crossref","unstructured":"Ignatiev, A., Morgado, A., Manquinho, V.M., Lynce, I., Marques-Silva, J.: Progression in maximum satisfiability. In: ECAI (2014)","DOI":"10.3233\/978-1-61499-419-0-453"},{"key":"30_CR16","doi-asserted-by":"crossref","unstructured":"Mangal, R., Zhang, X., Kamath, A., Nori, A.V., Naik, M.: Scaling relational inference using proofs and refutations. In: AAAI (2016)","DOI":"10.1609\/aaai.v30i1.10426"},{"key":"30_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-319-24318-4_22","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"R Mangal","year":"2015","unstructured":"Mangal, R., Zhang, X., Nori, A.V., Naik, M.: Volt: a lazy grounding framework for solving very large MaxSAT instances. In: Heule, M., et al. (eds.) SAT 2015. LNCS, vol. 9340, pp. 299\u2013306. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-24318-4_22"},{"key":"30_CR18","doi-asserted-by":"crossref","unstructured":"Mangal, R., Zhang, X., Nori, A.V., Naik, M.: A user-guided approach to program analysis. In: FSE (2015)","DOI":"10.1145\/2786805.2786851"},{"key":"30_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/978-3-642-02777-2_45","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"V Manquinho","year":"2009","unstructured":"Manquinho, V., Marques-Silva, J., Planes, J.: Algorithms for weighted boolean optimization. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 495\u2013508. Springer, Heidelberg (2009)"},{"key":"30_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"531","DOI":"10.1007\/978-3-319-10428-7_39","volume-title":"Principles and Practice of Constraint Programming","author":"R Martins","year":"2014","unstructured":"Martins, R., Joshi, S., Manquinho, V., Lynce, I.: Incremental cardinality constraints for MaxSAT. In: O\u2019Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 531\u2013548. Springer, Heidelberg (2014)"},{"key":"30_CR21","doi-asserted-by":"crossref","unstructured":"Martins, R., Manquinho, V.M., Lynce, I.: On partitioning for maximum satisfiability. In: ECAI 2012 (2012)","DOI":"10.3233\/AIC-2012-0517"},{"key":"30_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"438","DOI":"10.1007\/978-3-319-09284-3_33","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"R Martins","year":"2014","unstructured":"Martins, R., Manquinho, V., Lynce, I.: Open-WBO: a modular MaxSAT solver. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 438\u2013445. Springer, Heidelberg (2014)"},{"key":"30_CR23","unstructured":"MaxSAT evaluations. http:\/\/www.maxsat.udl.cat\/"},{"key":"30_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"564","DOI":"10.1007\/978-3-319-10428-7_41","volume-title":"Principles and Practice of Constraint Programming","author":"A Morgado","year":"2014","unstructured":"Morgado, A., Dodaro, C., Marques-Silva, J.: Core-guided MaxSAT with soft cardinality constraints. In: O\u2019Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 564\u2013573. Springer, Heidelberg (2014)"},{"issue":"4","key":"30_CR25","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/s10601-013-9146-2","volume":"18","author":"A Morgado","year":"2013","unstructured":"Morgado, A., Heras, F., Liffiton, M., Planes, J., Marques-Silva, J.: Iterative and core-guided MaxSAT solving: a survey and assessment. Constraints 18(4), 478\u2013534 (2013)","journal-title":"Constraints"},{"key":"30_CR26","doi-asserted-by":"crossref","unstructured":"Narodytska, N., Bacchus, F.: Maximum satisfiability using core-guided MaxSAT resolution. In: AAAI (2014)","DOI":"10.1609\/aaai.v28i1.9124"},{"issue":"1\u20132","key":"30_CR27","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/s10994-006-5833-1","volume":"62","author":"M Richardson","year":"2006","unstructured":"Richardson, M., Domingos, P.: Markov logic networks. Mach. Learn. 62(1\u20132), 107\u2013136 (2006)","journal-title":"Mach. Learn."},{"key":"30_CR28","doi-asserted-by":"crossref","unstructured":"Zhang, X., Mangal, R., Grigore, R., Naik, M., Yang, H.: On abstraction refinement for program analyses in Datalog. In: PLDI (2014)","DOI":"10.1145\/2594291.2594327"},{"key":"30_CR29","doi-asserted-by":"crossref","unstructured":"Zhang, X., Mangal, R., Nori, A.V., Naik, M.: Query-guided maximum satisfiability. In: POPL (2016)","DOI":"10.1145\/2837614.2837658"}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-44953-1_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,10]],"date-time":"2025-06-10T11:50:50Z","timestamp":1749556250000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-44953-1_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319449524","9783319449531"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-44953-1_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"23 August 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Principles and Practice of Constraint Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Toulouse","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 September 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cp2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}