{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,23]],"date-time":"2025-02-23T16:10:28Z","timestamp":1740327028418,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540208518"},{"type":"electronic","value":"9783540246053"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24605-3_30","type":"book-chapter","created":{"date-parts":[[2010,7,29]],"date-time":"2010-07-29T08:50:35Z","timestamp":1280393435000},"page":"398-410","source":"Crossref","is-referenced-by-count":16,"title":["SBSAT: a State-Based, BDD-Based Satisfiability Solver"],"prefix":"10.1007","author":[{"given":"John","family":"Franco","sequence":"first","affiliation":[]},{"given":"Michal","family":"Kouril","sequence":"additional","affiliation":[]},{"given":"John","family":"Schlipf","sequence":"additional","affiliation":[]},{"given":"Jeffrey","family":"Ward","sequence":"additional","affiliation":[]},{"given":"Sean","family":"Weaver","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Dransfield","sequence":"additional","affiliation":[]},{"given":"W. Mark","family":"Vanfleet","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"30_CR1","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, p. 193. Springer, Heidelberg (1999)"},{"key":"30_CR2","doi-asserted-by":"crossref","unstructured":"Brace, K.S., Rudell, R.L., Bryant, R.E.: Efficient Implementation of a BDD Package. In: ACM Proceedings of the 27th ACM\/IEEE Design Automation Conference, pp. 40\u201345 (1990)","DOI":"10.1145\/123186.123222"},{"key":"30_CR3","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 C\u00a035, 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers C"},{"key":"30_CR4","unstructured":"Cimatti, A., Giunchiglia, E., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV Version 2: BDD-Based + SAT-Based Symbolic Model Checking, Available from http:\/\/sra.itc.it\/people\/roveri\/papers\/IJCAR01.ps.gz"},{"key":"30_CR5","doi-asserted-by":"crossref","unstructured":"Coudert, O., Madre, J.C.: A Unified Framework for the Formal Verification of Sequential Circuits. In: Proc. of Int\u2019l Conf. on Computer-Aided Design, pp. 126\u2013129 (1990)","DOI":"10.1109\/ICCAD.1990.129859"},{"key":"30_CR6","unstructured":"Coudert, O., Madre, J.C.: Symbolic Computation of the Valid States of a Sequential Machine: Algorithms and Discussion. In: Proc. of Int\u2019l Worshop on Formal Methods in VLSI Design, Miami FL, USA (January 1991)"},{"key":"30_CR7","doi-asserted-by":"crossref","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 Association of Computing Machinery\u00a05, 394\u2013397 (1962)","journal-title":"Communications of the Association of Computing Machinery"},{"key":"30_CR8","unstructured":"Freeman, J.: Improvements to Propositional Satisfiability Search Algorithms. Ph.D. Dissertation in Computer and Information Science, University of Pennsylvania (1995)"},{"key":"30_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/3-540-46238-4_8","volume-title":"AI*IA 99:Advances in Artificial Intelligence","author":"E. Giunchiglia","year":"2000","unstructured":"Giunchiglia, E., Sebastiani, R.: Applying the Davis-Putnam Procedure to Non-Clausal Formulas. In: Lamma, E., Mello, P. (eds.) AI*IA 1999. LNCS (LNAI), vol.\u00a01792, p. 84. Springer, Heidelberg (2000)"},{"key":"30_CR10","doi-asserted-by":"crossref","unstructured":"Goldberg, E.: Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points. In: Proceedings of the Fifth International Symposium on the Theory and Applications of Satisfiability Testing, pp. 54\u201369 (2002) (Expanded version submitted for publication), Available from: http:\/\/gauss.ececs.uc.edu\/Conferences\/SAT2002\/Abstracts\/goldberg.ps","DOI":"10.1007\/3-540-45620-1_15"},{"key":"30_CR11","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: BerkMin: A Fast and Robust Sat-Solver Design. In: Proceedings Design, Automation, and Test in Europe, pp. 142\u2013149 (2002)","DOI":"10.1109\/DATE.2002.998262"},{"key":"30_CR12","doi-asserted-by":"crossref","unstructured":"Gupta, A., Ashar, P.: Integrating a Boolean Satisfiability Checker and BDDs for Combinational Equivalence Checking. In: Proceedings 11th IEEE International Conference on VLSI Design: VLSI for Signal Processing, pp. 222\u2013225 (1998)","DOI":"10.1109\/ICVD.1998.646606"},{"key":"30_CR13","doi-asserted-by":"crossref","unstructured":"Kalla, P., Zeng, Z., Ciesielski, M.J., Huang, C.: A BDD-based Satisfiability Infrastructure Using the Unate Recursive Paradigm. In: Proceedings Design, Automation, and Test in Europe 2000, pp. 232\u2013236 (2000)","DOI":"10.1145\/343647.343769"},{"key":"30_CR14","unstructured":"Kautz, H., McAllester, D., Selman, B.: Exploiting Variable Dependency in Local Search, Available from http:\/\/www.cs.washington.edu\/homes\/kautz\/papers\/dagsat.ps"},{"key":"30_CR15","unstructured":"Kullmann, O.: Heuristics for SAT Algorithms: Searching for Some Foundations (submitted for publication), Available from http:\/\/cs-svr1.swan.ac.uk\/~csoliver\/heur2letter.ps.gz"},{"key":"30_CR16","unstructured":"Lynce, I., Marques-Silva, J.: Efficient Data Structures for Backtrack Search SAT Solvers. In: Proceedings of the Fifth International Symposium on the Theory and Applications of Satisfiability Testing, pp. 308\u2013315 (2002), Available from: http:\/\/gauss.ececs.uc.edu\/Conferences\/SAT2002\/Abstracts\/lynce.ps"},{"key":"30_CR17","unstructured":"Moskewicz, M.W., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Engineering a (Super?) Efficient SAT Solver. In: Proceedings of the 38th ACM\/IEEE Design Automation Conference (2001)"},{"key":"30_CR18","doi-asserted-by":"crossref","unstructured":"Paruthi, V., Kuehlmann, A.: Equivalence Checking Combining a Structural SAT-Solver, BDDs, and Simulation. In: Proceedings of the IEEE International Conference on Computer Design: VLSI in Computers and Processors 2000, pp. 459\u2013 464 (2000)","DOI":"10.1109\/ICCD.2000.878323"},{"key":"30_CR19","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/BF02127973","volume":"17","author":"R. Puri","year":"1996","unstructured":"Puri, R., Gu, J.: A BDD SAT Solver for Satisfiability Testing: An Industrial Case Study. Annals of Mathematics and Artificial Intelligence\u00a017, 315\u2013337 (1996)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"30_CR20","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/0020-0190(95)00019-9","volume":"54","author":"J.S. Schlipf","year":"1995","unstructured":"Schlipf, J.S., Annexstein, F., Franco, J., Swaminathan, R.: On finding solutions for extended Horn formulas. Information Processing Letters\u00a054, 133\u2013137 (1995)","journal-title":"Information Processing Letters"},{"key":"30_CR21","volume-title":"Logic for Computer Scientists","author":"U. Sch\u00f6ning","year":"1980","unstructured":"Sch\u00f6ning, U.: Logic for Computer Scientists, vol.\u00a022. Springer, Heidelberg (1980)"},{"key":"30_CR22","doi-asserted-by":"crossref","unstructured":"Shtrichman, O.: Tuning SAT Checkers for Bounded Model Checking. In: Proceedings of the 12th International Computer Aided Verification Conference 2000 (2000)","DOI":"10.1007\/10722167_36"},{"key":"30_CR23","unstructured":"St\u00e5lmarck, G.: A System for Determining Propositional Logic Theorems by Applying Values and Rules to Triplets that are Generated from a Formula. Swedish Patent No. 467,076 (approved 1992), U.S. Patent No. 5,276,897 (1994), European Patent No. 0403,454 (1995)"},{"key":"30_CR24","unstructured":"Velev, M.N.: Superscalar Suite 1.0., Available from http:\/\/www.ece.cmu.edu\/~mvelev"},{"key":"30_CR25","doi-asserted-by":"crossref","unstructured":"Zhang, L., Madigan, C., Moskewicz, M., Malik, S.: Efficient Conflict Driven Learning in a Boolean Satisfiability Solver. In: Proceedings of ICCAD 2001 (2001)","DOI":"10.1145\/774572.774637"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24605-3_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,23]],"date-time":"2025-02-23T15:30:09Z","timestamp":1740324609000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24605-3_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540208518","9783540246053"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24605-3_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}