{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,2]],"date-time":"2025-11-02T16:30:58Z","timestamp":1762101058854},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540253334"},{"type":"electronic","value":"9783540319801"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-31980-1_19","type":"book-chapter","created":{"date-parts":[[2010,7,11]],"date-time":"2010-07-11T18:44:59Z","timestamp":1278873899000},"page":"287-300","source":"Crossref","is-referenced-by-count":15,"title":["Efficient Conflict Analysis for Finding All Satisfying Assignments of a Boolean Circuit"],"prefix":"10.1007","author":[{"given":"HoonSang","family":"Jin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"HyoJung","family":"Han","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fabio","family":"Somenzi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"Audemard, G., Bertoli, P., Cimatti, A., Kornilowicz, A., Sebastiani, R.: A SAT based approach for solving formulas over boolean and linear mathematical propositions. In: International Conference on Automated Deduction (July 2002)","DOI":"10.1007\/3-540-45620-1_17"},{"key":"19_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"428","DOI":"10.1007\/3-540-61474-5_95","volume-title":"Computer Aided Verification","author":"R.K. Brayton","year":"1996","unstructured":"Brayton, R.K., et al.: VIS: A system for verification and synthesis. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 428\u2013432. Springer, Heidelberg (1996)"},{"issue":"8","key":"19_CR4","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers\u00a0C-35(8), 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"Chai, D., Kuehlmann, A.: A fast pseudo-Boolean constraint solver. In: Proceedings of the Design Automation Conference, Anaheim, CA, pp. 830\u2013835 (June 2003)","DOI":"10.1145\/775832.776041"},{"key":"19_CR6","unstructured":"Chauhan, P., Clarke, E.M., Kroening, D.: Using SAT based image computation for reachability analysis. Technical Report CMU-CS-03-151 (2003)"},{"key":"19_CR7","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM\u00a05, 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"issue":"3","key":"19_CR8","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the Association for Computing Machinery\u00a07(3), 201\u2013215 (1960)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: BerkMin: A fast and robust SAT-solver. In: Proceedings of the Conference on Design, Automation and Test in Europe, Paris, France, pp. 142\u2013149 (March 2002)","DOI":"10.1109\/DATE.2002.998262"},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: Design, Automation and Test in Europe (DATE 2003), Munich, Germany, pp. 886\u2013891 (March 2003)","DOI":"10.1109\/DATE.2003.1253718"},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Prasad, M., Brayton, R.: Using SAT for combinational equivalence checking. In: Proceedings of the Conference on Design, Automation and Test in Europe, pp. 114\u2013121 (June 2001)","DOI":"10.1109\/DATE.2001.915010"},{"key":"19_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/978-3-540-30494-4_20","volume-title":"Proceedings of FMCAD","author":"O. Grumberg","year":"2004","unstructured":"Grumberg, O., Schuster, A., Yadgar, A.: Memory efficient all-solutions SAT solver and its application for reachability analysis. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 275\u2013289. Springer, Heidelberg (2004)"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Iyer, M.K., Parthasarathy, G., Cheng, K.-T.: SATORI \u2013 a fast sequential SAT engine for circuits. In: Proceedings of the International Conference on Computer-Aided Design, San Jose, CA, pp. 320\u2013325 (November 2003)","DOI":"10.1109\/ICCAD.2003.159706"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"Jin, H., Awedh, M., Somenzi, F.: CirCUs: A satisfiability solver geared towards bounded model checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 519\u2013522. Springer, Berlin (2004) (to appear)","DOI":"10.1007\/978-3-540-27813-9_50"},{"key":"19_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/11527695_17","volume-title":"Theory and Applications of Satisfiability Testing","author":"H. Jin","year":"2005","unstructured":"Jin, H., Somenzi, F.: CirCUs: A hybrid satisfiability solver. In: H. Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 211\u2013223. Springer, Heidelberg (2005)"},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"Kang, H.-J., Park, I.-C.: SAT-based unbounded symbolic model checking. In: Proceedings of the Design Automation Conference, Anaheim, CA, pp. 840\u2013843 (June 2003)","DOI":"10.1145\/775832.776043"},{"key":"19_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/978-3-540-27813-9_24","volume-title":"Computer Aided Verification","author":"D. Kroening","year":"2004","unstructured":"Kroening, D., Ouaknine, J., Seshia, S.A., Strichman, O.: Abstraction-based satisfiability solving of Presburger arithmetic. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 308\u2013320. Springer, Heidelberg (2004)"},{"key":"19_CR18","doi-asserted-by":"crossref","unstructured":"Kuehlmann, A., Ganai, M.K., Paruthi, V.: Circuit-based Boolean reasoning. In: Proceedings of the Design Automation Conference, Las Vegas, NV, pp. 232\u2013237 (June 2001)","DOI":"10.1145\/378239.378470"},{"key":"19_CR19","unstructured":"Li, B., Hsiao, M.S., Sheng, S.: A novel SAT all-solutions for efficient preimage computation. In: Proceedings of the Conference on Design, Automation and Test in Europe, pp. 380\u2013384 (March 2004)"},{"key":"19_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/3-540-45657-0_19","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2002","unstructured":"McMillan, K.L.: Applying SAT methods in unbounded symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 250\u2013264. Springer, Berlin (2002)"},{"key":"19_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Berlin (2003)"},{"key":"19_CR22","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the Design Automation Conference, Las Vegas, NV, pp. 530\u2013535 (June 2001)","DOI":"10.1145\/378239.379017"},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"Nam, G., Aloul, F., Sakallah, K., Rutenbar, R.: A comparative study of two boolean formulations of FPGA detailed routing constaraints. IEEE Transactions on Computer-Aided Design of Integrated Circuits, 688\u2013696 (June 2004)","DOI":"10.1109\/TC.2004.1"},{"key":"19_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-540-24730-2_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Ravi","year":"2004","unstructured":"Ravi, K., Somenzi, F.: Minimal assignments for bounded model checking. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 31\u201345. Springer, Heidelberg (2004)"},{"key":"19_CR25","doi-asserted-by":"crossref","unstructured":"Silva, J.P.M., Sakallah, K.A.: Grasp\u2014a new search algorithm for satisfiability. In: Proceedings of the International Conference on Computer-Aided Design, San Jose, CA, pp. 220\u2013227 (November 1996)","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"19_CR26","unstructured":"http:\/\/vlsi.colorado.edu\/~vis"},{"key":"19_CR27","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1007\/3-540-63104-6_28","volume-title":"Automated Deduction - CADE-14","author":"H. Zhang","year":"1997","unstructured":"Zhang, H.: SATO: An efficient propositional prover. In: McCune, W. (ed.) CADE 1997. LNCS (LNAI), vol.\u00a01249, pp. 272\u2013275. Springer, Heidelberg (1997)"},{"key":"19_CR28","unstructured":"Zhang, L., Madigan, C., Moskewicz, M., Malik, S.: Efficient conflict driven learning in Boolean satisfiability solver. In: Proceedings of the International Conference on Computer-Aided Design, San Jose, CA, pp. 279\u2013285 (November 2001)"},{"key":"19_CR29","unstructured":"Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In: Design, Automation and Test in Europe (DATE 2003), Munich, Germany, pp. 880\u2013885 (March 2003)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-31980-1_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,18]],"date-time":"2020-11-18T23:32:44Z","timestamp":1605742364000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-31980-1_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540253334","9783540319801"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-31980-1_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}