{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T11:24:09Z","timestamp":1763724249499},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540237389"},{"type":"electronic","value":"9783540304944"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30494-4_20","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T14:42:14Z","timestamp":1277822534000},"page":"275-289","source":"Crossref","is-referenced-by-count":29,"title":["Memory Efficient All-Solutions SAT Solver and Its Application for Reachability Analysis"],"prefix":"10.1007","author":[{"given":"Orna","family":"Grumberg","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Assaf","family":"Schuster","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Avi","family":"Yadgar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"20_CR1","doi-asserted-by":"crossref","unstructured":"Beer, I., Ben-David, S., Landver, A.: On-the-fly model checking of RCTL formulas. In: 10th Computer Aided Verification, pp. 184\u2013194 (1998)","DOI":"10.1007\/BFb0028744"},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: D. (ed.) IEEE Computer Society Press (June 1999)","DOI":"10.21236\/ADA360973"},{"key":"20_CR3","doi-asserted-by":"crossref","first-page":"457","DOI":"10.1613\/jair.601","volume":"10","author":"E. Birnbaum","year":"1999","unstructured":"Birnbaum, E., Lozinskii, E.L.: The good old davis-putnam procedure helps counting models. Journal of Artificial Intelligence Research\u00a010, 457\u2013477 (1999)","journal-title":"Journal of Artificial Intelligence Research"},{"issue":"8","key":"20_CR4","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"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"},{"issue":"2","key":"20_CR5","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Information and Computation\u00a098(2), 142\u2013170 (1992)","journal-title":"Information and Computation"},{"key":"20_CR6","unstructured":"Chauhan, P., Clarke, E.M., Kroening, D.: Using SAT based image computation for reachability analysis. Technical Report CMU-CS-03-151, Carnegie Mellon University (2003)"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Chauhan, P.P., Clarke, E.M., Kroening, D.: A SAT-based algorithm for reparameterization in symbolic simulation. In: DAC (2004)","DOI":"10.21236\/ADA461257"},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. CACM\u00a05(7) (July 1962)","DOI":"10.1145\/368273.368557"},{"issue":"3","key":"20_CR9","doi-asserted-by":"publisher","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. JACM\u00a07(3), 201\u2013215 (1960)","journal-title":"JACM"},{"key":"20_CR10","unstructured":"Goldberg, E., Novikov, Y.: Berkmin: A fast and robust SAT-solver. In: DATE (2002)"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/3-540-40922-X_22","volume-title":"Formal Methods in Computer-Aided Design","author":"A. Gupta","year":"2000","unstructured":"Gupta, A., Yang, Z., Ashar, P., Gupta, A.: SAT-based image computation with application in reachability analysis. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 354\u2013371. Springer, Heidelberg (2000)"},{"key":"20_CR12","first-page":"157","volume-title":"IAAI","author":"R.J. Bayardo Jr.","year":"2000","unstructured":"Bayardo Jr., R.J., Pehoushek, J.D.: Counting models using connected components. In: IAAI, pp. 157\u2013162. AAAI, Menlo Park (2000)"},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"Kang, H.J., Park, I.C.: SAT-based unbounded symbolic model checking. In: DAC (2003)","DOI":"10.1145\/776038.776043"},{"key":"20_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-540-45069-6_15","volume-title":"Computer Aided Verification","author":"S.K. Lahiri","year":"2003","unstructured":"Lahiri, S.K., Bryant, R.E., Cook, B.: A symbolic approach to predicate abstraction. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 141\u2013153. Springer, Heidelberg (2003)"},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"Letz, R.: Advances in decision procedures for quantified boolean formulas. In: IJCAR (2001)","DOI":"10.1007\/3-540-45616-3_12"},{"key":"20_CR16","first-page":"366","volume":"1","author":"C.M. Li","year":"1997","unstructured":"Li, C.M., Anbulagan: Heuristics based on unit propagation for satisfiability problems. IJCAI\u00a01, 366\u2013371 (1997)","journal-title":"IJCAI"},{"key":"20_CR17","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: Conflict analysis in search algorithms for propositional satisfiability. In: IEEE ICTAI (1996)"},{"key":"20_CR18","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Applying SAT methods in unbounded symbolic model checking. In: Computer Aided Verification (2002)","DOI":"10.1007\/3-540-45657-0_19"},{"key":"20_CR19","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: 39th Design Aotomation Conference, DAC 2001 (2001)","DOI":"10.1145\/378239.379017"},{"key":"20_CR20","unstructured":"Plaisted, D.: Method for design verification of hardware and non-hardware systems. United States Patents, 6,131, 078 (October 2000)"},{"key":"20_CR21","doi-asserted-by":"crossref","unstructured":"Roth, D.: On the hardness of approximate reasoning. Artificial Intelligence\u00a082(1-2) (1996)","DOI":"10.1016\/0004-3702(94)00092-1"},{"key":"20_CR22","unstructured":"Sapra, S., Theobald, M., Clarke, E.M.: SAT-based algorithms for logic minimization. In: ICCD (2003)"},{"key":"20_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_36","volume-title":"Computer Aided Verification","author":"O. Shtrichman","year":"2000","unstructured":"Shtrichman, O.: Tuning SAT checkers for bounded model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855. Springer, Heidelberg (2000)"},{"key":"20_CR24","unstructured":"Berkeley University of California. Espresso, two level boolean minimizer (1990)"},{"key":"20_CR25","unstructured":"Yadgar, A.: Solving All-SAT problem for reachability analysis. M.Sc. thesis, Technion, Israel Institute of Technology, Department of Computer Schience (2004)"},{"key":"20_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030077","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, vol.\u00a01249, Springer, Heidelberg (1997)"},{"key":"20_CR27","doi-asserted-by":"crossref","unstructured":"Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient conflict driven learning in boolean satisfiability solver. In: ICCAD (2001)","DOI":"10.1145\/774572.774637"}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30494-4_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T15:25:21Z","timestamp":1558279521000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30494-4_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540237389","9783540304944"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30494-4_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}