{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T02:04:16Z","timestamp":1769738656351,"version":"3.49.0"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030242572","type":"print"},{"value":"9783030242589","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","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":[[2019]]},"DOI":"10.1007\/978-3-030-24258-9_17","type":"book-chapter","created":{"date-parts":[[2019,6,28]],"date-time":"2019-06-28T21:02:31Z","timestamp":1561755751000},"page":"239-249","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["DRMaxSAT with MaxHS: First Contact"],"prefix":"10.1007","author":[{"given":"Antonio","family":"Morgado","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexey","family":"Ignatiev","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maria Luisa","family":"Bonet","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joao","family":"Marques-Silva","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sam","family":"Buss","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,6,29]]},"reference":[{"key":"17_CR1","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":"17_CR2","doi-asserted-by":"crossref","unstructured":"Audemard, G., Katsirelos, G., Simon, L.: A restriction of extended resolution for clause learning SAT solvers. In: AAAI (2010)","DOI":"10.1609\/aaai.v24i1.7553"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"641","DOI":"10.1007\/978-3-319-66158-2_41","volume-title":"Principles and Practice of Constraint Programming","author":"F Bacchus","year":"2017","unstructured":"Bacchus, F., Hyttinen, A., J\u00e4rvisalo, M., Saikko, P.: Reduced cost fixing in MaxSAT. In: Beck, J.C. (ed.) CP 2017. LNCS, vol. 10416, pp. 641\u2013651. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66158-2_41"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Berre, D.L., Parrain, A.: The Sat4j library, release 2.2. JSAT 7(2\u20133), 59\u20136 (2010)","DOI":"10.3233\/SAT190075"},{"key":"17_CR5","unstructured":"Biere, A.: Lingeling, plingeling and treengeling entering the SAT competition 2013. In: Balint, A., Belov, A., Heule, M., J\u00e4rvisalo, M. (eds.) Proceedings of SAT Competition 2013, Department of Computer Science Series of Publications B, vol. B-2013-1, pp. 51\u201352. University of Helsinki (2013)"},{"key":"17_CR6","unstructured":"Biere, A.: Lingeling essentials, a tutorial on design and implementation aspects of the SAT solver lingeling. In: Pragmatics of SAT workshop, p. 88 (2014)"},{"key":"17_CR7","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol.\u00a0185. IOS Press (2009)"},{"issue":"1","key":"17_CR8","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1080\/0952813021000026795","volume":"15","author":"E Birnbaum","year":"2003","unstructured":"Birnbaum, E., Lozinskii, E.L.: Consistent subsets of inconsistent systems: structure and behaviour. J. Exp. Theor. Artif. Intell. 15(1), 25\u201346 (2003)","journal-title":"J. Exp. Theor. Artif. Intell."},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Bonet, M.L., Buss, S., Ignatiev, A., Marques-Silva, J., Morgado, A.: Maxsat resolution with the dual rail encoding. In: AAAI. pp. 6565\u20136572 (2018)","DOI":"10.1609\/aaai.v32i1.12204"},{"issue":"8\u20139","key":"17_CR10","doi-asserted-by":"publisher","first-page":"606","DOI":"10.1016\/j.artint.2007.03.001","volume":"171","author":"ML Bonet","year":"2007","unstructured":"Bonet, M.L., Levy, J., Many\u00e0, F.: Resolution for Max-SAT. Artif. Intell. 171(8\u20139), 606\u2013618 (2007)","journal-title":"Artif. Intell."},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Bryant, R.E., Beatty, D.L., Brace, K.S., Cho, K., Sheffler, T.J.: COSMOS: a compiled simulator for MOS circuits. In: DAC, pp. 9\u201316 (1987)","DOI":"10.1145\/37888.37890"},{"issue":"1","key":"17_CR12","doi-asserted-by":"publisher","first-page":"36","DOI":"10.2307\/2273702","volume":"44","author":"SA Cook","year":"1979","unstructured":"Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb. Log. 44(1), 36\u201350 (1979)","journal-title":"J. Symb. Log."},{"key":"17_CR13","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). https:\/\/doi.org\/10.1007\/978-3-642-23786-7_19"},{"key":"17_CR14","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). https:\/\/doi.org\/10.1007\/978-3-642-39071-5_13"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-642-40627-0_21","volume-title":"Principles and Practice of Constraint Programming","author":"J Davies","year":"2013","unstructured":"Davies, J., Bacchus, F.: Postponing optimization to speed Up MAXSAT solving. In: Schulte, C. (ed.) CP 2013. LNCS, vol. 8124, pp. 247\u2013262. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40627-0_21"},{"issue":"1\u20134","key":"17_CR16","first-page":"1","volume":"2","author":"N E\u00e9n","year":"2006","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Translating pseudo-boolean constraints into SAT. JSAT 2(1\u20134), 1\u201326 (2006)","journal-title":"JSAT"},{"key":"17_CR17","unstructured":"Elffers, J., Nordstr\u00f6m, J.: Divide and conquer: towards faster pseudo-boolean solving. In: IJCAI, pp. 1291\u20131299 (2018). www.ijcai.org"},{"key":"17_CR18","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). https:\/\/doi.org\/10.1007\/11814948_25"},{"issue":"15","key":"17_CR19","doi-asserted-by":"publisher","first-page":"1277","DOI":"10.1016\/j.artint.2010.07.008","volume":"174","author":"J Huang","year":"2010","unstructured":"Huang, J.: Extended clause learning. Artif. Intell. 174(15), 1277\u20131284 (2010)","journal-title":"Artif. Intell."},{"key":"17_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-319-66263-3_11","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2017","author":"A Ignatiev","year":"2017","unstructured":"Ignatiev, A., Morgado, A., Marques-Silva, J.: On Tackling the limits of resolution in SAT solving. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 164\u2013183. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66263-3_11"},{"key":"17_CR21","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"516","DOI":"10.1007\/978-3-319-94205-6_34","volume-title":"Automated Reasoning","author":"B Kiesl","year":"2018","unstructured":"Kiesl, B., Rebola-Pardo, A., Heule, M.J.H.: Extended resolution simulates DRAT. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 516\u2013531. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_34"},{"issue":"1\/2","key":"17_CR22","first-page":"95","volume":"8","author":"M Koshimura","year":"2012","unstructured":"Koshimura, M., Zhang, T., Fujita, H., Hasegawa, R.: QMaxSAT: a partial Max-SAT solver. JSAT 8(1\/2), 95\u2013100 (2012)","journal-title":"JSAT"},{"issue":"2\u20133","key":"17_CR23","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1016\/j.artint.2007.05.006","volume":"172","author":"J Larrosa","year":"2008","unstructured":"Larrosa, J., Heras, F., de Givry, S.: A logical approach to efficient Max-SAT solving. Artif. Intell. 172(2\u20133), 204\u2013233 (2008)","journal-title":"Artif. Intell."},{"key":"17_CR24","unstructured":"Li, C.M., Many\u00e0, F.: MaxSAT. In: Biere et al. [7], pp. 613\u2013631"},{"key":"17_CR25","unstructured":"Marques-Silva, J., Planes, J.: On using unsatisfiability for solving maximum satisfiability CoRR abs\/0712.1097 (2007)"},{"key":"17_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10428-7_39"},{"key":"17_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-09284-3_33"},{"key":"17_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10428-7_41"},{"issue":"4","key":"17_CR29","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.H., 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":"17_CR30","first-page":"129","volume":"9","author":"A Morgado","year":"2015","unstructured":"Morgado, A., Ignatiev, A., Marques-Silva, J.: MSCG: robust core-guided MaxSAT solving. JSAT 9, 129\u2013134 (2015)","journal-title":"JSAT"},{"key":"17_CR31","doi-asserted-by":"crossref","unstructured":"Narodytska, N., Bacchus, F.: Maximum satisfiability using core-guided MaxSAT resolution. In: AAAI, pp. 2717\u20132723 (2014)","DOI":"10.1609\/aaai.v28i1.9124"},{"issue":"1\u20132","key":"17_CR32","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/S0004-3702(99)00035-1","volume":"111","author":"L Palopoli","year":"1999","unstructured":"Palopoli, L., Pirri, F., Pizzuti, C.: Algorithms for selective enumeration of prime implicants. Artif. Intell. 111(1\u20132), 41\u201372 (1999)","journal-title":"Artif. Intell."},{"issue":"1","key":"17_CR33","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/0004-3702(87)90062-2","volume":"32","author":"R Reiter","year":"1987","unstructured":"Reiter, R.: A theory of diagnosis from first principles. Artif. Intell. 32(1), 57\u201395 (1987)","journal-title":"Artif. Intell."},{"key":"17_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"539","DOI":"10.1007\/978-3-319-40970-2_34","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"P Saikko","year":"2016","unstructured":"Saikko, P., Berg, J., J\u00e4rvisalo, M.: LMHS: a SAT-IP hybrid MaxSAT solver. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 539\u2013546. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_34"},{"key":"17_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"827","DOI":"10.1007\/11564751_73","volume-title":"Principles and Practice of Constraint Programming - CP 2005","author":"C Sinz","year":"2005","unstructured":"Sinz, C.: Towards an optimal CNF encoding of boolean cardinality constraints. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 827\u2013831. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11564751_73"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2019"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-24258-9_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,22]],"date-time":"2022-09-22T10:33:02Z","timestamp":1663842782000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-24258-9_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030242572","9783030242589"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-24258-9_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"29 June 2019","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":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2019","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":"sat2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/sat2019.tecnico.ulisboa.pt\/","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":"64","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":"19","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":"7","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":"30% - 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":"6","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":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}