{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T05:58:13Z","timestamp":1725602293839},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642238772"},{"type":"electronic","value":"9783642238789"}],"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-23878-9_22","type":"book-chapter","created":{"date-parts":[[2011,8,24]],"date-time":"2011-08-24T03:54:01Z","timestamp":1314158041000},"page":"178-185","source":"Crossref","is-referenced-by-count":3,"title":["Finding First-Order Minimal Unsatisfiable Cores with a Heuristic Depth-First-Search Algorithm"],"prefix":"10.1007","author":[{"given":"Jianmin","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Weixia","family":"Xu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jun","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shengyu","family":"Shen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhengbin","family":"Pang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tiejun","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jun","family":"Xia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sikun","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"22_CR1","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1016\/j.artint.2006.01.003","volume":"170","author":"H. Jorg","year":"2006","unstructured":"Jorg, H., Ri, B.: Conformant planning via heuristic forward search: A new approach. Artificial Intelligence\u00a0170, 507\u2013541 (2006)","journal-title":"Artificial Intelligence"},{"key":"22_CR2","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 (DAC 2005), pp. 445\u2013450 (2005)","DOI":"10.1145\/1065579.1065697"},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"Simmonds, J., et al.: Exploiting resolution proofs to speed up LTL vacuity detection for BMC. In: Proceedings of the 7th International Conference on Formal Methods in Computer Aided Design (FMCAD 2007), pp. 3\u201312 (2007)","DOI":"10.1109\/FAMCAD.2007.16"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Oh, Y., Mneimneh, M.N., Andraus, Z.S., Sakallah, K.A., Markov, I.L.: AMUSE: a minimally-unsatisfiable subformula extractor. In: Proceedings of the 41st Design Automation Conference (DAC 2004), pp. 518\u2013523 (2004)","DOI":"10.1145\/996566.996710"},{"key":"22_CR5","unstructured":"Lynce, I., Marques-Silva, J.P.: On computing minimum unsatisfiable cores. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 305\u2013310. Springer, Heidelberg (2004)"},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/11499107_13","volume-title":"Theory and Applications of Satisfiability Testing","author":"M.H. Liffiton","year":"2005","unstructured":"Liffiton, M.H., Sakallah, K.A.: On finding all minimally unsatisfiable subformulas. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 173\u2013186. Springer, Heidelberg (2005)"},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/11817963_13","volume-title":"Computer Aided Verification","author":"R. Gershman","year":"2006","unstructured":"Gershman, R., Koifman, M., Strichman, O.: Deriving small unsatisfiable cores with dominators. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 109\u2013122. Springer, Heidelberg (2006)"},{"key":"22_CR8","unstructured":"Gregoire, E., Mazuer, B., Piette, C.: Boosting a complete technique to find MSS and MUS thanks to a local search oracle. In: Proceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI 2007), pp. 2300\u20132305 (2007)"},{"key":"22_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-540-79719-7_27","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2008","author":"H. Maaren van","year":"2008","unstructured":"van Maaren, H., Wieringa, S.: Finding guaranteed mUSes\u00a0fast. In: B\u00fcning, K.H., Zhao, X. (eds.) SAT 2008. LNCS, vol.\u00a04996, pp. 291\u2013304. Springer, Heidelberg (2008)"},{"issue":"4","key":"22_CR10","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/s10601-008-9058-8","volume":"14","author":"M.H. Liffiton","year":"2009","unstructured":"Liffiton, M.H., Mneimneh, M.N., Lynce, I., Andraus, Z.S., Marques-Silva, J.P., Sakallah, K.A.: A branch and bound algorithm for extracting smallest minimal unsatisfiable formulas. Constraints\u00a014(4), 415\u2013442 (2009)","journal-title":"Constraints"},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/978-3-642-04222-5_21","volume-title":"Frontiers of Combining Systems","author":"C. Piette","year":"2009","unstructured":"Piette, C., Hamadi, Y., Sa\u00efs, L.: Efficient combination of decision procedures for MUS computation. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol.\u00a05749, pp. 335\u2013349. Springer, Heidelberg (2009)"},{"key":"22_CR12","unstructured":"Nadel, A.: Boosting minimal unsatisfiable core extraction. In: Proceedings of the 10th International Conference on Formal Methods in Computer Aided Design (FMCAD 2010), pp. 221\u2013229 (2010)"},{"key":"22_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/978-3-540-27813-9_49","volume-title":"Computer Aided Verification","author":"C.W. Barrett","year":"2004","unstructured":"Barrett, C.W., Berezin, S.: CVC Lite: A New Implementation of the Cooperating Validity Checker Category B. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 515\u2013518. Springer, Heidelberg (2004)"},{"key":"22_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-540-31980-1_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Bozzano","year":"2005","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Schulz, S., Sebastiani, R.: An incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic. In: Halbwachs, N., Zuck, L. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 317\u2013333. Springer, Heidelberg (2005)"},{"key":"22_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A Fast Linear-Arithmetic Solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"key":"22_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-540-72788-0_32","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"A. Cimatti","year":"2007","unstructured":"Cimatti, A., Griggio, A., Sebastiani, R.: A simple and flexible way of computing small unsatisfiable cores in SAT modulo theories. In: Marques-Silva, J., Sakallah, K. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 334\u2013339. Springer, Heidelberg (2007)"},{"key":"22_CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/978-3-540-25984-8_13","volume-title":"Automated Reasoning","author":"F. Mari\u0107","year":"2004","unstructured":"Mari\u0107, F., Jani\u010di\u0107, P.: argo-lib: A generic platform for decision procedures. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 213\u2013217. Springer, Heidelberg (2004)"},{"key":"22_CR18","unstructured":"Barret, C., Deters, M., Oliveras, A., et al.: \n                  \n                    http:\/\/www.smtcomp.org\/2010\/bench-marks.shtml\n                  \n                  \n                 (accessed in 2010)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Data Engineering and Automated Learning - IDEAL 2011"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-23878-9_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,31]],"date-time":"2019-03-31T21:28:43Z","timestamp":1554067723000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-23878-9_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642238772","9783642238789"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-23878-9_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}