{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,14]],"date-time":"2025-11-14T07:26:21Z","timestamp":1763105181564},"publisher-location":"Berlin, Heidelberg","reference-count":57,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439974"},{"type":"electronic","value":"9783540456575"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45657-0_2","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T14:59:43Z","timestamp":1179586783000},"page":"17-36","source":"Crossref","is-referenced-by-count":82,"title":["The Quest for Efficient Boolean Satisfiability Solvers"],"prefix":"10.1007","author":[{"given":"Lintao","family":"Zhang","sequence":"first","affiliation":[]},{"given":"Sharad","family":"Malik","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,9,20]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"S. A. Cook, \u201cThe complexity of theorem-proving procedures,\u201d presented at Third Annual ACM Symposium on Theory of Computing, 1971.","DOI":"10.1145\/800157.805047"},{"key":"2_CR2","unstructured":"H. Kautz and B. Selman, \u201cPlanning as Satisfiability,\u201d presented at European Conference on Artificial Intelligence(ECAI-92), 1992."},{"key":"2_CR3","doi-asserted-by":"publisher","first-page":"1167","DOI":"10.1109\/43.536723","volume":"15","author":"P. Stephan","year":"1996","unstructured":"P. Stephan, R. Brayton, and A. Sangiovanni-Vencentelli, \u201cCombinational Test Generation Using Satisfiability,\u201d IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 15, pp. 1167\u20131176, 1996.","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"D. Jackson and M. Vaziri, \u201cFinding Bugs with a Constraint Solver,\u201d presented at International Symposium on Software Testing and Analysis, Portland, OR, 2000.","DOI":"10.1145\/347324.383378"},{"key":"2_CR5","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"M. Davis and H. Putnam, \u201cA computing procedure for quantification theory,\u201d Journal of ACM, vol. 7, pp. 201\u2013215, 1960.","journal-title":"Journal of ACM"},{"key":"2_CR6","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"M. Davis, G. Logemann, and D. Loveland, \u201cA machine program for theorem proving,\u201d Communications of the ACM, vol. 5, pp. 394\u2013397, 1962.","journal-title":"Communications of the ACM"},{"key":"2_CR7","unstructured":"B. Selman, H. Kautz, and B. Cohen, \u201cLocal Search Strategies for Satisfiability Testing,\u201d in Cliques, Coloring, and Satisfiability: Second DIMACS Implementation Challenge, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 26, D. S. Johnson and M. A. Trick, Eds.: American Methematical Society, 1996."},{"key":"2_CR8","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant, \u201cGraph-Based Algorithms for Boolean Function Manipulation,\u201d IEEE Transactions on Computers, vol. C-35, pp. 677\u2013691, 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"2_CR9","unstructured":"G. St\u00e5lmarck, \u201cA system for determining prepositional logic theorems by applying values and rules to triplets that are generated from a formula.\u201d US Patent N 5 27689, 1995."},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"J. Gu, P. W. Purdom, J. Franco, and B. W. Wah, \u201cAlgorithms for the Satisfiability (SAT) Problem: A Survey,\u201d in DIMACS Series in Discrete Mathematics and Theoretical Computer Science: American Mathematical Society, 1997.","DOI":"10.1090\/dimacs\/035\/02"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"G.-J. Nam, K. A. Sakallah, and R. A. Rutenbar, \u201cSatisfiability-Based Layout Revisited: Detailed Routing of Complex FPGAs Via Search-Based Boolean SAT,\u201d presented at ACM\/SIGDA International Symposium on Field-Programmable Gate Arrays (FPGA\u201999), Monterey, California, 1999.","DOI":"10.1145\/296399.296450"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu, \u201cSymbolic Model Checking without BDDs,\u201d presented at Tools and Algorithms for the Analysis and Construction of Systems (TACAS\u201999), 1999.","DOI":"10.21236\/ADA360973"},{"key":"2_CR13","unstructured":"J. Crawford and L. Auton, \u201cExperimental results on the cross-over point in satisfiability problems,\u201d presented at National Conference on Artificial Intelligence (AAAI), 1993."},{"key":"2_CR14","unstructured":"J. W. Freeman, \u201cImprovements to Propositional Satisfiability Search Algorithms,\u201d in Ph.D. Thesis, Department of Computer and Information Science: University of Pennsylvania, 1995."},{"key":"2_CR15","unstructured":"A. V. Gelder and Y. K. Tsuji, \u201cSatisfiability Testing with more Reasoning and Less guessing,\u201d in Cliques, Coloring and Satisfiability: Second DIMACS Implementation Challenge, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, M. Trick, Ed.: American Mathematical Society, 1995."},{"key":"2_CR16","unstructured":"O. Dubois, P. Andre, Y. Boufkhad, and J. Carlier, \u201cSAT v.s. UNSAT,\u201d in Cliques, Coloring and Satisfiability: Second DIMACS Implementation Challenge, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, D. S. Johnson and M. Trick, Eds., 1993."},{"key":"2_CR17","unstructured":"J. P. Marques-Silva and K. A. Sakallah, \u201cConflict Analysis in Search Algorithms for Propositional Satisfiability,\u201d presented at IEEE International Conference on Tools with Artificial Intelligence, 1996."},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"R. Bayardo and R. Schrag, \u201cUsing CSP look-back techniques to solve real-world SAT instances,\u201d presented at National Conference on Artificial Intelligence (AAAI), 1997.","DOI":"10.1007\/3-540-61551-2_65"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"H. Zhang, \u201cSATO: An efficient propositional prover,\u201d presented at International Conference on Automated Deduction (CADE), 1997.","DOI":"10.1007\/3-540-63104-6_28"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik, \u201cChaff: Engineering an Efficient SAT Solver,\u201d presented at 39th Design Automation Conference, 2001.","DOI":"10.1145\/378239.379017"},{"key":"2_CR21","unstructured":"E. Goldberg and Y. Novikov, \u201cBerkMin: a Fast and Robust SAT-Solver,\u201d presented at Design Automation & Test in Europe (DATE 2002), 2002."},{"key":"2_CR22","unstructured":"C. M. Li and Anbulagan, \u201cHeuristics based on unit propagation for satisfiability problems, \u201d presented at the fifteenth International Joint Conference on Artificial Intelligence (IJCAI\u201997), Nagayo, Japan, 1997."},{"key":"2_CR23","unstructured":"O. Dubois and G. Dequen, \u201cA backbone-search heuristic for efficient solving of hard 3-SAT formulae,\u201d presented at International Joint Conference on Artificial Intelligence (IJCAI), 2001."},{"key":"2_CR24","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D. A. Plaisted","year":"1986","unstructured":"D. A. Plaisted and S. Greenbaum, \u201cA Stucture-preserving Clause Form Translation,\u201d Journal of Symbolic Computation, vol. 2, pp. 293\u2013304, 1986.","journal-title":"Journal of Symbolic Computation"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"J. P. Marques-Silva and K. A. Sakallah, \u201cGRASP\u2014 A New Search Algorithm for Satisfiability,\u201d presented at IEEE International Conference on Tools with Artificial Intelligence, 1996.","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"J. P. Marques-Silva, \u201cThe Impact of Branching Heuristics in Propositional Satisfiability Algorithms,\u201d presented at the 9th Portuguese Conference on Artificial Intelligence (EPIA), 1999.","DOI":"10.1007\/3-540-48159-1_5"},{"key":"2_CR27","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/BF00881805","volume":"15","author":"J. N. Hooker","year":"1995","unstructured":"J. N. Hooker and V. Vinay, \u201cBranching rules for satisfiability,\u201d Journal of Automated Reasoning, vol. 15, pp. 359\u2013383, 1995.","journal-title":"Journal of Automated Reasoning"},{"key":"2_CR28","unstructured":"M. Buro and H. Kleine-Buning, \u201cReport on a SAT competition,\u201d Technical Report, University of Paderborn 1992."},{"key":"2_CR29","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BF01531077","volume":"1","author":"R. G. Jeroslow","year":"1990","unstructured":"R. G. Jeroslow and J. Wang, \u201cSolving propositional satisfiability problems,\u201d Annals of Mathematics and Artificial Intelligence, vol. 1, pp. 167\u2013187, 1990.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"2_CR30","unstructured":"H. Zhang and M. Stickel, \u201cAn efficient algorithm for unit-propagation,\u201d presented at International Symposium on Artificial Intelligence and Mathematics, Ft. Lauderdale, Florida, 1996."},{"key":"2_CR31","unstructured":"I. Lynce and J. P. Marques-Silva, \u201cEfficient data structures for backtrack search SAT solvers,\u201d presented at Fifth International Symposium on the Theory and Applications of Satisfiability Testing, 2002."},{"key":"2_CR32","unstructured":"C. M. Li, \u201cIntegrating equivalency reasoning into Davis-Putnam Procedure,\u201d presented at National Conference on Artificial Intelligence (AAAI), 2000."},{"key":"2_CR33","unstructured":"I. Lynce and J. P. Marques-Silva, \u201cIntegrating Simplification Techniques in SAT Algorithms,\u201d presented at Logic in Computer Science Short Paper Session (LICS-SP), 2001."},{"key":"2_CR34","unstructured":"A. V. Gelder and Y. K. Tsuji, \u201cSatisfiability Testing with more Reasoning and Less guessing,\u201d in Cliques, Coloring and Satisfiability: Second DIMACS Implementation Challenge, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, D. S. Johnson and M. Trick, Eds.: American Mathematical Society, 1993."},{"key":"2_CR35","doi-asserted-by":"crossref","unstructured":"S. T. Chakradhar and V. D. Agrawal, \u201cA Transitive Closure Based Algorithm for Test Generation,\u201d presented at Design Automation Conference (DAC), 1991.","DOI":"10.1145\/127601.127693"},{"key":"2_CR36","doi-asserted-by":"publisher","first-page":"1143","DOI":"10.1109\/43.310903","volume":"13","author":"W. Kunz","year":"1994","unstructured":"W. Kunz and D. K. Pradhan, \u201cRecursive Learning: A New Implication Technique for Efficient Solutions to CAD-problems: Test, Verification and Optimization,\u201d IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 13, pp. 1143\u20131158, 1994.","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"2_CR37","unstructured":"J. P. Marques-Silva, \u201cImproving Satisfiability Algorithms by Using Recursive Learning, \u201d presented at International Workshop on Boolean Problems (IWBP), 1998."},{"key":"2_CR38","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1111\/j.1467-8640.1993.tb00310.x","volume":"9","author":"P. Prosser","year":"1993","unstructured":"P. Prosser, \u201cHybrid algorithms for the constraint satisfaction problem,\u201d Computational Intelligence, vol. 9, pp. 268\u2013299, 1993.","journal-title":"Computational Intelligence"},{"key":"2_CR39","doi-asserted-by":"crossref","unstructured":"L. Zhang, C. Madigan, M. Moskewicz, and S. Malik, \u201cEfficient Conflict Driven Learning in a Boolean Satisfiability Solver,\u201d presented at International Conference on Computer Aided Design (ICCAD), San Jose, CA, 2001.","DOI":"10.1145\/774572.774637"},{"key":"2_CR40","unstructured":"G. Hachtel and F. Somenzi, Logic Sysntheiss and Verification Algorithms: Kluwer Academic Publishers, 1996."},{"key":"2_CR41","unstructured":"H. Zhang and M. Stickel, \u201cImplementing Davis-Putnam\u2019s method,\u201d Technical Report, University of Iowa 1994."},{"key":"2_CR42","doi-asserted-by":"crossref","unstructured":"P. Chatalic and L. Simon, \u201cMulti-Resolution on Compressed Sets of Clauses,\u201d presented at International Conference on Tools with Artificial Intelligence, 2000.","DOI":"10.1109\/TAI.2000.889839"},{"key":"2_CR43","unstructured":"F. Aloul, M. Mneimneh, and K. Sakallah, \u201cBacktrack Search Using ZBDDs,\u201d presented at International Workshop on Logic Synthesis (IWLS), 2001."},{"key":"2_CR44","doi-asserted-by":"crossref","unstructured":"S. I. Minato, \u201cZero-Suppressed BDDs for Set Manipulation in Combinatorial Problems,\u201d presented at 30th Design Automation Conference (DAC), 1993.","DOI":"10.1145\/157485.164890"},{"key":"2_CR45","unstructured":"I. Lynce and J. P. Marques-Silva, \u201cThe Puzzling Role of Simplification in Propositional Satisfiability,\u201d presented at EPIA\u201901 Workshop on Constraint Satisfaction and Operational Research Techniques for Problem Solving (EPIA-CSOR), 2001."},{"key":"2_CR46","unstructured":"C. P. Gomes, B. Selman, and H. Kautz, \u201cBoosting Combinatorial Search Through Randomization,\u201d presented at National Conference on Artificial Intelligence (AAAI), Madison, WI, 1998."},{"key":"2_CR47","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1126\/science.275.5296.51","volume":"275","author":"B. A. Huberman","year":"1997","unstructured":"B. A. Huberman, R. M. Lukose, and T. Hogg, \u201cAn Economics approach to hard computational problems,\u201d Science, vol. 275, pp. 51\u201354, 1997.","journal-title":"Science"},{"key":"2_CR48","unstructured":"I. Lynce and J. P. Marques-Silva, \u201cComplete unrestricted backtracking algorithms for Satisfiability,\u201d presented at Fifth International Symposium on the Theory and Applications of Satisfiability Testing, 2002."},{"issue":"1\/2","key":"2_CR49","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1023\/A:1006314320276","volume":"24","author":"C. P. Gomes","year":"1999","unstructured":"C. P. Gomes, B. Selman, N. Crator, and H. Kautz, \u201cHeavy-tailed phenomena in satisfiability and constraint satisfaction problems,\u201d Journal of Automated Reasoning, vol. 24(1\/2), pp. 67\u2013100, 1999.","journal-title":"Journal of Automated Reasoning"},{"key":"2_CR50","unstructured":"\u201cProver Proof Engine,\u201d Prover Technology."},{"key":"2_CR51","doi-asserted-by":"crossref","unstructured":"J. F. Groote and J. P. Warners, \u201cThe propositional formula checker HeerHugo,\u201d Journal of Automated Reasoning, vol. 24, 2000.","DOI":"10.1023\/A:1006366304347"},{"key":"2_CR52","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1023\/A:1008287028851","volume":"12","author":"Y. Shang","year":"1998","unstructured":"Y. Shang and B. W. Wah, \u201cA Discrete Lagrangian-Based Global-Search Method for Solving Satisfiability Problems,\u201d Journal of Global Optimization, vol. 12, pp. 61\u201399, 1998.","journal-title":"Journal of Global Optimization"},{"key":"2_CR53","unstructured":"I. Gent and T. Walsh, \u201cThe SAT Phase Transition,\u201d presented at European Conference on Artificial Intelligence (ECAI-94), 1994."},{"key":"2_CR54","doi-asserted-by":"crossref","unstructured":"M. Prasad, P. Chong, and K. Keutzer, \u201cWhy is ATPG easy?,\u201d presented at Design Automation Conference (DAC99), 1999.","DOI":"10.1145\/309847.309857"},{"key":"2_CR55","unstructured":"F. Brglez, X. Li, and M. Stallmann, \u201cThe role of a skeptic agent in testing and benchmarking of SAT algorithms,\u201d presented at Fifth International Symposium on theTheory and Applications of Satisfiability Testing, 2002."},{"key":"2_CR56","doi-asserted-by":"crossref","unstructured":"O. Strichman, \u201cPruning techniques for the SAT-based Bounded Model Checking Problem,\u201d presented at 11th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARM\u201901), 2001.","DOI":"10.1007\/3-540-44798-9_4"},{"key":"2_CR57","doi-asserted-by":"crossref","unstructured":"M. Ganai, L. Zhang, P. Ashar, A. Gupta, and S. Malik, \u201cCombining Strengths of Circuit-based and CNF-based Algorithms for a High-Performance SAT Solver,\u201d presented at Design Automation Conference (DAC\u201902), 2002.","DOI":"10.1145\/514100.514105"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45657-0_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,11]],"date-time":"2023-05-11T22:35:05Z","timestamp":1683844505000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45657-0_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439974","9783540456575"],"references-count":57,"URL":"https:\/\/doi.org\/10.1007\/3-540-45657-0_2","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}