{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,2]],"date-time":"2025-11-02T16:33:24Z","timestamp":1762101204415},"reference-count":7,"publisher":"National Library of Serbia","issue":"3","license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["ComSIS","COMPUT SCI INF SYST","COMPUT SCI INFORM SY","COMPUTER SCI INFORM","COMSIS J"],"published-print":{"date-parts":[[2011]]},"abstract":"<jats:p>Explaining the causes of infeasibility of formulas has practical applications\n   in various fields, such as formal verification and electronic design\n   automation. A minimal unsatisfiable subformula provides a succinct\n   explanation of infeasibility and is valuable for applications. The problem of\n   deriving minimal unsatisfiable cores from Boolean formulas has been addressed\n   rather frequently in recent years. However little attention has been\n   concentrated on extraction of unsatisfiable subformulas in Satisfiability\n   Modulo Theories(SMT). In this paper, we propose a depth-firstsearch algorithm\n   and a breadth-first-search algorithm to compute minimal unsatisfiable cores\n   in SMT, adopting different searching strategy. We report and analyze\n   experimental results obtaining from a very extensive test on SMT-LIB\n   benchmarks.<\/jats:p>","DOI":"10.2298\/csis101019024z","type":"journal-article","created":{"date-parts":[[2011,7,7]],"date-time":"2011-07-07T11:10:09Z","timestamp":1310037009000},"page":"693-710","source":"Crossref","is-referenced-by-count":6,"title":["Extracting minimal unsatisfiable subformulas in satisfiability modulo theories"],"prefix":"10.2298","volume":"8","author":[{"given":"Jianmin","family":"Zhang","sequence":"first","affiliation":[{"name":"Dept. of Computer Science, National University of Defense Technology Changsha, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shengyu","family":"Shen","sequence":"additional","affiliation":[{"name":"Dept. of Computer Science, National University of Defense Technology Changsha, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jun","family":"Zhang","sequence":"additional","affiliation":[{"name":"Dept. of Computer Science, National University of Defense Technology Changsha, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Weixia","family":"Xu","sequence":"additional","affiliation":[{"name":"Dept. of Computer Science, National University of Defense Technology Changsha, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"LI.","family":"Sikun","sequence":"additional","affiliation":[{"name":"Dept. of Computer Science, National University of Defense Technology Changsha, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1078","reference":[{"key":"1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0653(04)00320-8"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1016\/S0166-218X(02)00399-2"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-008-9058-8"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-008-0051-z"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-007-9019-7"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1016\/j.ejor.2007.06.066"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1145\/1217856.1217859"}],"container-title":["Computer Science and Information Systems"],"original-title":[],"language":"en","deposited":{"date-parts":[[2023,5,29]],"date-time":"2023-05-29T08:30:16Z","timestamp":1685349016000},"score":1,"resource":{"primary":{"URL":"https:\/\/doiserbia.nb.rs\/Article.aspx?ID=1820-02141100024Z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"references-count":7,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2011]]}},"URL":"https:\/\/doi.org\/10.2298\/csis101019024z","relation":{},"ISSN":["1820-0214","2406-1018"],"issn-type":[{"value":"1820-0214","type":"print"},{"value":"2406-1018","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}