{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,15]],"date-time":"2026-01-15T05:20:32Z","timestamp":1768454432348,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642215803","type":"print"},{"value":"9783642215810","type":"electronic"}],"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:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-21581-0_13","type":"book-chapter","created":{"date-parts":[[2011,6,10]],"date-time":"2011-06-10T13:30:19Z","timestamp":1307712619000},"page":"145-158","source":"Crossref","is-referenced-by-count":5,"title":["Minimally Unsatisfiable Boolean Circuits"],"prefix":"10.1007","author":[{"given":"Anton","family":"Belov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joao","family":"Marques-Silva","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","doi-asserted-by":"crossref","first-page":"75","DOI":"10.3233\/SAT190039","volume":"4","author":"A. Biere","year":"2008","unstructured":"Biere, A.: Picosat essentials. Journal on Satisfiability, Boolean Modeling and Computation\u00a04, 75\u201397 (2008)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"issue":"2","key":"13_CR2","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/s10878-008-9142-4","volume":"18","author":"C. Desrosiers","year":"2009","unstructured":"Desrosiers, C., Galinier, P., Hertz, A., Paroz, S.: Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems. J. Comb. Optim.\u00a018(2), 124\u2013150 (2009)","journal-title":"J. Comb. Optim."},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Gr\u00e9goire, \u00c9., Mazure, B., Piette, C.: On approaches to explaining infeasibility of sets of Boolean clauses. In: Int\u2019l. Conf. on Tools with Artificial Intelligence, pp. 74\u201383 (2008)","DOI":"10.1109\/ICTAI.2008.39"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Jain, H., Clarke, E.M.: Efficient SAT solving for non-clausal formulas using DPLL, graphs, and watched cuts. In: Proc. of the 46th Annual Design Automation Conference, pp. 563\u2013568 (2009)","DOI":"10.1145\/1629911.1630057"},{"key":"13_CR5","unstructured":"J\u00e4rvisalo, M., Le Berre, D., Roussel, O.: Rules of the 2011 SAT Competition (2011), http:\/\/www.satcompetition.org\/2011\/"},{"key":"13_CR6","first-page":"339","volume-title":"Handbook of Satisfiability, ch. 11","author":"H. Kleine B\u00fcuning","year":"2009","unstructured":"Kleine B\u00fcuning, H., Kullmann, O.: Minimal unsatisfiability and autarkies. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, ch. 11, pp. 339\u2013401. IOS Press, Amsterdam (2009)"},{"key":"13_CR7","doi-asserted-by":"crossref","first-page":"59","DOI":"10.3233\/SAT190075","volume":"7","author":"D. Berre Le","year":"2010","unstructured":"Le Berre, D., Parrain, A.: The Sat4j library, release 2.2. Journal on Satisfiability, Boolean Modeling and Computation\u00a07, 59\u201364 (2010)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.: Minimal unsatisfiability: Models, algorithms and applications. In: Int\u2019l Symposium on Multiple-Valued Logic, pp. 9\u201314 (2010)","DOI":"10.1109\/ISMVL.2010.11"},{"key":"13_CR9","series-title":"LNCS","first-page":"156","volume-title":"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.\u00a06695, pp. 156\u2013170. Springer, Heidelberg (2011)"},{"key":"13_CR10","unstructured":"Nadel, A.: Boosting minimal unsatisfiable core extraction. In: Formal Methods in Computer- Aided Design (2010)"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Schuppan, V.: Towards a notion of unsatisfiable cores for LTL. In: Fundamentals of Software Engineering. In: Third IPM Int\u2019l Conference, pp. 129\u2013145 (2010)","DOI":"10.1007\/978-3-642-11623-0_7"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Tseitin, G.S.: On the complexity of derivations in the propositional calculus. Studies in Mathematics and Mathematical Logic, Part II, pp. 115\u2013125 (1968)","DOI":"10.1007\/978-1-4899-5327-8_25"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing - SAT 2011"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21581-0_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,20]],"date-time":"2020-06-20T01:16:11Z","timestamp":1592615771000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21581-0_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642215803","9783642215810"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21581-0_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}