{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:04:45Z","timestamp":1742911485888,"version":"3.40.3"},"publisher-location":"Singapore","reference-count":25,"publisher":"Springer Singapore","isbn-type":[{"type":"print","value":"9789811618765"},{"type":"electronic","value":"9789811618772"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"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":[[2021]]},"DOI":"10.1007\/978-981-16-1877-2_1","type":"book-chapter","created":{"date-parts":[[2021,4,8]],"date-time":"2021-04-08T06:03:53Z","timestamp":1617861833000},"page":"3-13","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Accelerating Predicate Abstraction by Minimum Unsatisfiable Cores Extraction"],"prefix":"10.1007","author":[{"given":"Jianmin","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tiejun","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kefan","family":"Ma","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,4,9]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao Y., et al.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference, pp. 530\u2013535. ACM, Las Vegas, USA (2001)","key":"1_CR1","DOI":"10.1145\/378239.379017"},{"key":"1_CR2","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). https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37"},{"doi-asserted-by":"crossref","unstructured":"Jain, H., Kroening, D.: Word level predicate abstraction and refinement for verifying RTL Verilog. In: Proceedings of the 42nd Design Automation Conference, pp. 445\u2013450. ACM, Anaheim, San Diego, USA (2005)","key":"1_CR3","DOI":"10.1145\/1065579.1065697"},{"issue":"4","key":"1_CR4","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/s10601-008-9058-8","volume":"14","author":"MH Liffiton","year":"2009","unstructured":"Liffiton, M.H., Mneimneh, M.N., Lynce, I., et al.: A branch and bound algorithm for extracting smallest minimal unsatisfiable formulas. Constraints 14(4), 415\u2013442 (2009)","journal-title":"Constraints"},{"issue":"3","key":"1_CR5","first-page":"56","volume":"37","author":"JM Zhang","year":"2009","unstructured":"Zhang, J.M., Li, S.K., Shen, S.Y.: Algorithms for Deriving minimum unsatisfiable Boolean subformulae. Acta Electronica Sinica 37(3), 56\u201359 (2009)","journal-title":"Acta Electronica Sinica"},{"unstructured":"Lynce, I., Marques-silva, J.: On computing minimum unsatisfiable cores, In: Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing, pp. 305\u2013310. Springer, Vancouver (2004)","key":"1_CR6"},{"key":"1_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-007-9084-z","volume":"40","author":"MH Liffiton","year":"2008","unstructured":"Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reason. 40, 1\u201330 (2008)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"1_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10703-008-0051-z","volume":"33","author":"R Gershman","year":"2008","unstructured":"Gershman, R., Koifman, M., Strichman, O.: An approach for extracting a small unsatisfiable core. Formal Method Syst. Des. 33(1), 1\u201327 (2008)","journal-title":"Formal Method Syst. Des."},{"issue":"3","key":"1_CR9","doi-asserted-by":"publisher","first-page":"640","DOI":"10.1016\/j.ejor.2007.06.066","volume":"199","author":"E Gregoire","year":"2009","unstructured":"Gregoire, E., Mazuer, B., Piette, C.: Using local search to find MSSes and MUSes. Eur. J. Oper. Res. 199(3), 640\u2013646 (2009)","journal-title":"Eur. J. Oper. Res."},{"unstructured":"Nadel, A.: Boosting minimal unsatisfiable core extraction. In: Proceedings of 10th International Conference Formal Methods in Computer Aided Design, pp. 221\u2013229. IEEE, Lugano, Switzerland (2010)","key":"1_CR10"},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-21581-0_15","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"V Ryvchin","year":"2011","unstructured":"Ryvchin, V., Strichman, O.: Faster extraction of high-level minimal unsatisfiable cores. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 174\u2013187. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21581-0_15"},{"issue":"2","key":"1_CR12","doi-asserted-by":"publisher","first-page":"97","DOI":"10.3233\/AIC-2012-0523","volume":"25","author":"A Belov","year":"2012","unstructured":"Belov, A., Lynce, I., Marques-Silva, J.: Towards efficient MUS extraction. J. AI Commun. 25(2), 97\u2013116 (2012)","journal-title":"J. AI Commun."},{"doi-asserted-by":"crossref","unstructured":"Nadel, A., Ryvchin, V., Strichman, O.: Efficient MUS extraction with resolution. In: Proceedings 13th International Conference Formal Methods in Computer Aided Design, pp. 197\u2013200. IEEE, Portland, OR, USA (2013)","key":"1_CR13","DOI":"10.1109\/FMCAD.2013.6679410"},{"key":"1_CR14","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). https:\/\/doi.org\/10.1007\/978-3-319-09284-3_5"},{"key":"1_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-319-21668-3_5","volume-title":"Computer Aided Verification","author":"F Bacchus","year":"2015","unstructured":"Bacchus, F., Katsirelos, G.: Using minimal correction sets to more efficiently compute minimal unsatisfiable sets. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 70\u201386. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21668-3_5"},{"key":"1_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-319-33954-2_3","volume-title":"Integration of AI and OR Techniques in Constraint Programming","author":"F Bacchus","year":"2016","unstructured":"Bacchus, F., Katsirelos, G.: Finding a collection of MUSes incrementally. In: Quimper, C.-G. (ed.) CPAIOR 2016. LNCS, vol. 9676, pp. 35\u201344. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33954-2_3"},{"doi-asserted-by":"crossref","unstructured":"Zhao, W., Liffiton, M.H.: Parallelizing partial MUS enumeration. In: Proceedings of IEEE 28th International Conference on Tools with Artificial Intelligence, pp. 464\u2013471. IEEE, San Jose, CA, USA (2016)","key":"1_CR17","DOI":"10.1109\/ICTAI.2016.0077"},{"doi-asserted-by":"crossref","unstructured":"Gregoire, E., Izza Y.: Boosting MCSes enumeration. In: Proceedings of the 27th International Joint Conference on Artificial Intelligence, pp. 1309\u20131315. ACM, Stockholm, Sweden (2018)","key":"1_CR18","DOI":"10.24963\/ijcai.2018\/182"},{"doi-asserted-by":"crossref","unstructured":"Narodytska, N., Bjorner, N., Marinescu, M.C., et al.: Core-guided minimal correction set and core enumeration. In: Proceedings of the 27th International Joint Conference on Artificial Intelligence, pp. 1353\u20131361. ACM, Stockholm, Sweden (2018)","key":"1_CR19","DOI":"10.24963\/ijcai.2018\/188"},{"key":"1_CR20","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-319-99957-9_7","volume-title":"Artificial Intelligence and Symbolic Computation","author":"S Liu","year":"2018","unstructured":"Liu, S., Luo, J.: FMUS2: an efficient algorithm to compute minimal unsatisfiable subsets. In: Fleuriot, J., Wang, D., Calmet, J. (eds.) AISC 2018. LNCS (LNAI), vol. 11110, pp. 104\u2013118. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-99957-9_7"},{"issue":"11","key":"1_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s11432-019-9881-0","volume":"62","author":"J Luo","year":"2019","unstructured":"Luo, J., Liu, S.: Accelerating MUS enumeration by inconsistency graph partitioning. Sci. China Inf. Sci. 62(11), 1\u201311 (2019). https:\/\/doi.org\/10.1007\/s11432-019-9881-0","journal-title":"Sci. China Inf. Sci."},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-030-24258-9_15","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2019","author":"C Menc\u00eda","year":"2019","unstructured":"Menc\u00eda, C., Kullmann, O., Ignatiev, A., Marques-Silva, J.: On computing the union of MUSes. In: Janota, M., Lynce, I. (eds.) SAT 2019. LNCS, vol. 11628, pp. 211\u2013221. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-24258-9_15"},{"key":"1_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1007\/978-3-030-53288-8_21","volume-title":"Computer Aided Verification","author":"J Bend\u00edk","year":"2020","unstructured":"Bend\u00edk, J., Meel, K.S.: Approximate counting of minimal unsatisfiable subsets. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 439\u2013462. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_21"},{"unstructured":"Jaroslav, B., Cerna, I.: Rotation based MSS\/MCS enumeration. In: Proceedings of the 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 120\u2013137. EasyChair, Alicante, Spain (2020)","key":"1_CR24"},{"key":"1_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-030-45190-5_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Bend\u00edk","year":"2020","unstructured":"Bend\u00edk, J., \u010cern\u00e1, I.: MUST: minimal unsatisfiable subsets enumeration tool. TACAS 2020. LNCS, vol. 12078, pp. 135\u2013152. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_8"}],"container-title":["Communications in Computer and Information Science","Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-16-1877-2_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,8]],"date-time":"2021-04-08T06:14:00Z","timestamp":1617862440000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-981-16-1877-2_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9789811618765","9789811618772"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-981-16-1877-2_1","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"9 April 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NCTCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"National Conference of Theoretical Computer Science","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Nanning","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","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":"13 November 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 November 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nctcs2020","order":10,"name":"conference_id","label":"Conference ID","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":"https:\/\/conf.ccf.org.cn\/TCS2020","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"28","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":"13","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":"46% - 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-5","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":"3-5","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)"}}]}}