{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:55:19Z","timestamp":1725490519907},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540744825"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74484-9_56","type":"book-chapter","created":{"date-parts":[[2007,8,28]],"date-time":"2007-08-28T21:48:03Z","timestamp":1188337683000},"page":"649-659","source":"Crossref","is-referenced-by-count":0,"title":["A Heuristic Local Search Algorithm for Unsatisfiable Cores Extraction"],"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":[{"key":"56_CR1","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference (DAC\u201901) (2001)","DOI":"10.1145\/378239.379017"},{"key":"56_CR2","series-title":"Lecture Notes in Computer Science","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. Een","year":"2004","unstructured":"Een, N., Sorensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, Springer, Heidelberg (2004)"},{"key":"56_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","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, Springer, Heidelberg (2003)"},{"issue":"3-4","key":"56_CR4","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":"56_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/11568421","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, Springer, Heidelberg (2005)"},{"key":"56_CR6","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: Proceedings of the 2001 International Symposium on Physical Design (ISPD\u201901) (2001)","DOI":"10.1145\/369691.369777"},{"key":"56_CR7","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":"56_CR8","doi-asserted-by":"crossref","unstructured":"Bruni, R., Sassano, A.: Restoring satisfiability or maintaining unsatisfiability by finding small unsatisfiable subformulae. In: Proceedings of the Fourth Workshop on Theory and Application of Satisfiability Testing (SAT\u201901) (2001)","DOI":"10.1016\/S1571-0653(04)00320-8"},{"key":"56_CR9","series-title":"Lecture Notes in Computer Science","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, Springer, Heidelberg (2005)"},{"key":"56_CR10","doi-asserted-by":"crossref","unstructured":"de la Banda, M., Stuckey, P., Wazny, J.: Finding all minimal unsatisfiable subsets. In: Proceedings of the Fifth ACM-SIGPLAN International Symposium on Principles and Practice of Declarative Programming (PPDP\u201903) (2003)","DOI":"10.1145\/888251.888256"},{"key":"56_CR11","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\u201904) (2004)","DOI":"10.1145\/996566.996710"},{"key":"56_CR12","doi-asserted-by":"crossref","unstructured":"Huang, J.: MUP: A minimal unsatisfiability prover. In: Proceedings of the Tenth Asia and South Pacific Design Automation Conference (ASP-DAC\u201905) (2005)","DOI":"10.1145\/1120725.1120907"},{"key":"56_CR13","series-title":"Lecture Notes in Computer Science","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, Springer, Heidelberg (2005)"},{"key":"56_CR14","doi-asserted-by":"crossref","unstructured":"Bailey, J., Stuckey, P.J.: Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. In: Proceedings of the Seventh International Symposium on Practical Aspects of Declarative Languages (PADL\u201905) (2005)","DOI":"10.1007\/978-3-540-30557-6_14"},{"key":"56_CR15","series-title":"Lecture Notes in Computer Science","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, Springer, Heidelberg (2005)"},{"key":"56_CR16","doi-asserted-by":"crossref","unstructured":"Zhang, J., Li, S., Shen, S.: Extracting minimum unsatisfiable cores with a greedy genetic algorithm. In: Proceedings of the 19th Australian Joint Conference on Artificial Intelligence (AUS-AI\u201906) (2006)","DOI":"10.1007\/11941439_89"},{"key":"56_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Springer, Heidelberg (2006)"},{"key":"56_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Springer, Heidelberg (2006)"},{"key":"56_CR19","doi-asserted-by":"crossref","unstructured":"Gregoire, E., Mazuer, B., Piette, C.: Tracking MUSes and strict inconsistent covers. In: Proceedings of the the Sixth Conference on Formal Methods in Computer-Aided Design (FMCAD\u201906) (2006)","DOI":"10.1109\/FMCAD.2006.34"},{"key":"56_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Computational Science and Its Applications \u2013 ICCSA 2007"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74484-9_56.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:33:34Z","timestamp":1619519614000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74484-9_56"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540744825"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74484-9_56","relation":{},"subject":[]}}