{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:32:20Z","timestamp":1742913140452,"version":"3.40.3"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030300470"},{"type":"electronic","value":"9783030300487"}],"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-30048-7_15","type":"book-chapter","created":{"date-parts":[[2019,9,22]],"date-time":"2019-09-22T19:03:06Z","timestamp":1569178986000},"page":"251-267","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Trimming Graphs Using Clausal Proof Optimization"],"prefix":"10.1007","author":[{"given":"Marijn J. H.","family":"Heule","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,9,23]]},"reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-540-89439-1_2","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R As\u00edn","year":"2008","unstructured":"As\u00edn, R., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E.: Efficient generation of unsatisfiability proofs and cores in SAT. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 16\u201330. Springer, Heidelberg (2008)"},{"key":"15_CR2","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: 21st International Joint Conference on Artificial Intelligence, pp. 399\u2013404 (2009)"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-319-09284-3_5","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"A Belov","year":"2014","unstructured":"Belov, A., Heule, M.J.H., Marques-Silva, J.: MUS extraction using clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 48\u201357. Springer, Cham (2014)"},{"key":"15_CR4","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1016\/S1385-7258(51)50053-7","volume":"54","author":"NG Bruijn de","year":"1951","unstructured":"de Bruijn, N.G., Erd\u0151s, P.: A colour problem for infinite graphs and a problem in the theory of relations. Nederl. Akad. Wetensch. Proc. Ser. A 54, 371\u2013373 (1951)","journal-title":"Nederl. Akad. Wetensch. Proc. Ser. A"},{"key":"15_CR5","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1287\/ijoc.3.2.157","volume":"3","author":"JW Chinneck","year":"1991","unstructured":"Chinneck, J.W., Dravnieks, E.W.: Locating minimal infeasible constraint sets in linear programs. INFORMS J. Comput. 3, 157\u2013168 (1991)","journal-title":"INFORMS J. Comput."},{"key":"15_CR6","unstructured":"Crawford, J.M., Ginsberg, M.L., Luks, E.M., Roy, A.: Symmetry-breaking predicates for search problems. In: Knowledge Representation and Reasoning - KR 1996, pp. 148\u2013159. Morgan Kaufmann (1996)"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-319-63046-5_14","volume-title":"Automated Deduction \u2013 CADE 26","author":"L Cruz-Filipe","year":"2017","unstructured":"Cruz-Filipe, L., Heule, M.J.H., Hunt Jr., W.A., Kaufmann, M., Schneider-Kamp, P.: Efficient certified RAT verification. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 220\u2013236. Springer, Cham (2017)"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-662-54577-5_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Cruz-Filipe","year":"2017","unstructured":"Cruz-Filipe, L., Marques-Silva, J.P., Schneider-Kamp, P.: Efficient certified resolution proof checking. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 118\u2013135. Springer, Heidelberg (2017)"},{"key":"15_CR9","unstructured":"Goldberg, E.I., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: DATE, pp. 10886\u201310891 (2003)"},{"key":"15_CR10","first-page":"18","volume":"XXVIII","author":"ADNJ Grey de","year":"2018","unstructured":"de Grey, A.D.N.J.: The chromatic number of the plane is at least 5. Geombinatorics XXVIII, 18\u201331 (2018)","journal-title":"Geombinatorics"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Gurfinkel, A., Vizel, Y.: DRUPing for interpolants. In: Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design, FMCAD 2014, pp. 19:99\u201319:106. FMCAD Inc., Austin (2014)","DOI":"10.1109\/FMCAD.2014.6987601"},{"issue":"3","key":"15_CR12","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/BF01175656","volume":"53","author":"H Hadwiger","year":"1950","unstructured":"Hadwiger, H.: Minkowskische addition und subtraktion beliebiger punktmengen und die theoreme von erhard schmidt. Math. Z. 53(3), 210\u2013218 (1950)","journal-title":"Math. Z."},{"key":"15_CR13","first-page":"32","volume":"XXVIII","author":"MJH Heule","year":"2018","unstructured":"Heule, M.J.H.: Computing small unit-distance graphs with chromatic number 5. Geombinatorics XXVIII, 32\u201350 (2018)","journal-title":"Geombinatorics"},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-319-66107-0_18","volume-title":"Interactive Theorem Proving","author":"MJH Heule","year":"2017","unstructured":"Heule, M.J.H., Hunt Jr., W.A., Kaufmann, M., Wetzler, N.D.: Efficient, verified checking of propositional proofs. In: Ayala-Rinc\u00f3n, M., Mu\u00f1oz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 269\u2013284. Springer, Cham (2017)"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Hunt Jr., W.A., Wetzler, N.D.: Trimming while checking clausal proofs. In: Formal Methods in Computer-Aided Design, pp. 181\u2013188. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679408"},{"issue":"8","key":"15_CR16","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1002\/stvr.1549","volume":"24","author":"MJH Heule","year":"2014","unstructured":"Heule, M.J.H., Hunt Jr., W.A., Wetzler, N.D.: Bridging the gap between easy generation and efficient verification of unsatisfiability proofs. Softw. Test. Verif. Reliab. (STVR) 24(8), 593\u2013607 (2014)","journal-title":"Softw. Test. Verif. Reliab. (STVR)"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-319-23219-5_13","volume-title":"Principles and Practice of Constraint Programming","author":"A Ignatiev","year":"2015","unstructured":"Ignatiev, A., Previti, A., Liffiton, M., Marques-Silva, J.: Smallest MUS extraction with minimal hitting set dualization. In: Pesant, G. (ed.) CP 2015. LNCS, vol. 9255, pp. 173\u2013182. Springer, Cham (2015)"},{"issue":"4","key":"15_CR18","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1007\/s10817-011-9239-9","volume":"49","author":"M J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Biere, A., Heule, M.J.H.: Simulating circuit-level simplifications on CNF. J. Autom. Reason. 49(4), 583\u2013619 (2012)","journal-title":"J. Autom. Reason."},{"key":"15_CR19","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-319-63046-5_15","volume-title":"Automated Deduction \u2013 CADE 26","author":"P Lammich","year":"2017","unstructured":"Lammich, P.: Efficient verified (UN)SAT certificate checking. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 237\u2013254. Springer, Cham (2017)"},{"issue":"4","key":"15_CR20","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/s10601-008-9058-8","volume":"14","author":"M Liffiton","year":"2008","unstructured":"Liffiton, M., Mneimneh, M., Lynce, I., Andraus, Z., Marques-Silva, J., Sakallah, K.: A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas. Constraints 14(4), 415 (2008)","journal-title":"Constraints"},{"key":"15_CR21","unstructured":"Lynce, I., Marques Silva, J.P.: On computing minimum unsatisfiable cores. In: The Seventh International Conference on Theory and Applications of Satisfiability Testing, SAT 2004, 10\u201313 May 2004, Vancouver, BC, Canada, Online Proceedings (2004)"},{"key":"15_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/978-3-642-21581-0_14","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"J Marques-Silva","year":"2011","unstructured":"Marques-Silva, J., Lynce, I.: On improving MUS extraction algorithms. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 159\u2013173. Springer, Heidelberg (2011)"},{"key":"15_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/11499107_40","volume-title":"Theory and Applications of Satisfiability Testing","author":"M Mneimneh","year":"2005","unstructured":"Mneimneh, M., Lynce, I., Andraus, Z., Marques-Silva, J., Sakallah, K.: A Branch-and-Bound algorithm for extracting smallest minimal unsatisfiable formulas. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 467\u2013474. Springer, Heidelberg (2005)"},{"key":"15_CR24","first-page":"187","volume":"4","author":"L Moser","year":"1961","unstructured":"Moser, L., Moser, W.: Solution to problem 10. Can. Math. Bull. 4, 187\u2013189 (1961)","journal-title":"Can. Math. Bull."},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"Soifer, A.: The Mathematical Coloring Book (2008). ISBN-13: 978\u20130387746401","DOI":"10.1007\/978-0-387-74642-5_2"},{"key":"15_CR26","doi-asserted-by":"crossref","unstructured":"Van Gelder, A.: Verifying RUP proofs of propositional unsatisfiability. In: ISAIM (2008)","DOI":"10.1007\/978-3-540-72788-0_31"},{"key":"15_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-319-09284-3_31","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"ND Wetzler","year":"2014","unstructured":"Wetzler, N.D., Heule, M.J.H., Hunt Jr., W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422\u2013429. Springer, Cham (2014)"},{"key":"15_CR28","unstructured":"Zhang, L.: Searching for truth: techniques for satisfiability of Boolean formulas. Ph.D. thesis, Princeton University, Princeton, NJ, USA (2003)"}],"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-030-30048-7_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,25]],"date-time":"2019-09-25T16:05:01Z","timestamp":1569427501000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-30048-7_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030300470","9783030300487"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-30048-7_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"23 September 2019","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":"Stamford, CT","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":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 September 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cp2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/cp2019.a4cp.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-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":"118","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":"46","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":"39% - 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.2","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":"4","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)"}}]}}