{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:45:18Z","timestamp":1725497118011},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540772255"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-77226-2_40","type":"book-chapter","created":{"date-parts":[[2007,12,6]],"date-time":"2007-12-06T14:55:58Z","timestamp":1196952958000},"page":"385-394","source":"Crossref","is-referenced-by-count":0,"title":["Finding Unsatisfiable Subformulas with Stochastic Method"],"prefix":"10.1007","author":[{"given":"Jianmin","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shengyu","family":"Shen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sikun","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3-4","key":"40_CR1","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1023\/A:1018999721141","volume":"22","author":"B. Mazure","year":"1998","unstructured":"Mazure, B., Sais, L., Gregoire, E.: Boosting complete techniques thanks to local search methods. Annals of Mathematics and Artificial Intelligence\u00a022(3-4), 319\u2013331 (1998)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"40_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/3-540-36577-X_2","volume-title":"TACAS 2003","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L., Amla, N.: Automatic abstraction without counterexamples. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol.\u00a02619, pp. 2\u201317. Springer, Heidelberg (2003)"},{"key":"40_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"298","DOI":"10.1007\/978-3-540-30579-8_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Shen","year":"2005","unstructured":"Shen, S., Qin, Y., Li, S.: Minimizing counterexample with unit core extraction and incremental SAT. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 298\u2013312. Springer, Heidelberg (2005)"},{"doi-asserted-by":"crossref","unstructured":"Nam, G-J., Aloul, F., Sakallah, K., Rutenbar, R.: A comparative study of two Boolean formulations of FPGA detailed routing constraints. In: ISPD 2001. Proceedings of the 2001 International Symposium on Physical Design, pp. 222\u2013227 (2001)","key":"40_CR4","DOI":"10.1145\/369691.369777"},{"key":"40_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"Theory and Applications of Satisfiability Testing","author":"L. Zhang","year":"2004","unstructured":"Zhang, L., Malik, S.: Extracting small unsatisfiable cores from unsatisfiable Boolean formula. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, Springer, Heidelberg (2004)"},{"key":"40_CR6","series-title":"Lecture Notes in Computer Science","first-page":"305","volume-title":"Theory and Applications of Satisfiability Testing","author":"I. Lynce","year":"2005","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 (2005)"},{"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: DAC 2004. Proceedings of the 41st Design Automation Conference, pp. 518\u2013523 (2004)","key":"40_CR7","DOI":"10.1145\/996566.996710"},{"key":"40_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"40_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"174","DOI":"10.1007\/978-3-540-30557-6_14","volume-title":"PADL 2005","author":"J. Bailey","year":"2005","unstructured":"Bailey, J., Stuckey, P.J.: Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. In: Hermenegildo, M.V., Cabeza, D. (eds.) PADL 2005. LNCS, vol.\u00a03350, pp. 174\u2013186. Springer, Heidelberg (2005)"},{"key":"40_CR10","series-title":"Lecture Notes in Computer Science","first-page":"393","volume-title":"Theory and Applications of Satisfiability Testing","author":"M.N. Mneimneh","year":"2005","unstructured":"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. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 393\u2013399. Springer, Heidelberg (2005)"},{"key":"40_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"847","DOI":"10.1007\/11941439_89","volume-title":"AI 2006: Advances in Artificial Intelligence","author":"J. Zhang","year":"2006","unstructured":"Zhang, J., Li, S., Shen, S.: Extracting minimum unsatisfiable cores with a greedy genetic algorithm. In: Sattar, A., Kang, B.-H. (eds.) AI 2006. LNCS (LNAI), vol.\u00a04304, pp. 847\u2013856. Springer, Heidelberg (2006)"},{"key":"40_CR12","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 dominator. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 109\u2013122. Springer, Heidelberg (2006)"},{"key":"40_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/11814948_5","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"N. Dershowitz","year":"2006","unstructured":"Dershowitz, N., Hanna, Z., Nadel, A.: A scalable algorithm for minimal unsatisfiable core extraction. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 36\u201341. Springer, Heidelberg (2006)"},{"doi-asserted-by":"crossref","unstructured":"Gregoire, E., Mazuer, B., Piette, C.: Tracking MUSes and strict inconsistent covers. In: FMCAD 2006. Proceedings of the the Sixth Conference on Formal Methods in Computer-Aided Design, pp. 39\u201346 (2006)","key":"40_CR14","DOI":"10.1109\/FMCAD.2006.34"},{"key":"40_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/11814948_28","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"S. Prestwich","year":"2006","unstructured":"Prestwich, S., Lynce, I.: Local search for unsatisfiability. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 283\u2013296. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Data Engineering and Automated Learning - IDEAL 2007"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-77226-2_40.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:05:11Z","timestamp":1619521511000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-77226-2_40"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540772255"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-77226-2_40","relation":{},"subject":[]}}