{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,20]],"date-time":"2025-09-20T20:20:52Z","timestamp":1758399652608,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540278290"},{"type":"electronic","value":"9783540315803"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11527695_27","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T17:06:47Z","timestamp":1292864807000},"page":"360-375","source":"Crossref","is-referenced-by-count":63,"title":["Zchaff2004: An Efficient SAT Solver"],"prefix":"10.1007","author":[{"given":"Yogesh S.","family":"Mahajan","sequence":"first","affiliation":[]},{"given":"Zhaohui","family":"Fu","sequence":"additional","affiliation":[]},{"given":"Sharad","family":"Malik","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"27_CR1","doi-asserted-by":"crossref","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: Third Annual ACM Symposium on Theory of Computing (1971)","DOI":"10.1145\/800157.805047"},{"key":"27_CR2","unstructured":"Kautz, H., Selman, B.: Planning as Satisfiability. In: European Conference on Artificial Intelligence (1992)"},{"key":"27_CR3","doi-asserted-by":"publisher","first-page":"1167","DOI":"10.1109\/43.536723","volume":"15","author":"P. Stephan","year":"1996","unstructured":"Stephan, P., Brayton, R., Sangiovanni-Vencentelli, A.: Combinational test generation using satisfiability. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems\u00a015, 1167\u20131176 (1996)","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"27_CR4","doi-asserted-by":"crossref","unstructured":"Jackson, D., Vaziri, M.: Finding bugs with a constraint solver. In: International Symposium on Software Testing and Analysis, Portland, OR (2000)","DOI":"10.1145\/347324.383378"},{"key":"27_CR5","first-page":"226","volume-title":"38th DAC","author":"M.N. Velev","year":"2001","unstructured":"Velev, M.N., Bryant, R.E.: Effective use of boolean satisfiability procedures in the formal verification of superscalar and VLIW. In: 38th DAC, pp. 226\u2013231. ACM Press, New York (2001)"},{"key":"27_CR6","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.M., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, p. 193. Springer, Heidelberg (1999)"},{"key":"27_CR7","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. Journal of ACM\u00a07, 201\u2013215 (1960)","journal-title":"Journal of ACM"},{"key":"27_CR8","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"},{"key":"27_CR9","unstructured":"Selman, B., Kautz, H., Cohen, B.: Local search strategies for satisfiability testing. In: Proceedings of the Second DIMACS Challange on Cliques, Coloring, and Satisfiability (1993)"},{"key":"27_CR10","first-page":"394","volume":"C-35","author":"R.E. Bryant","year":"1962","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers\u00a0C-35, 394\u2013397 (1962)","journal-title":"IEEE Transactions on Computers"},{"key":"27_CR11","unstructured":"Gunnar St\u00e5lmarck: System for Determining Propositional Logic Theorems by Applying Values and Rules to Triplets that are Generated from Boolean Formula, United States Patent. Patent Number 5,276,897 (1994)"},{"key":"27_CR12","doi-asserted-by":"crossref","unstructured":"Gu, J., Purdom, P.W., Franco, J., Wah, B.W.: Algorithms for the Satisfiability (SAT) Problem: A Survey. In: DIMACS Series in Discrete Mathematics and Theoretical Computer Science (1997)","DOI":"10.1090\/dimacs\/035\/02"},{"key":"27_CR13","doi-asserted-by":"crossref","unstructured":"Nam, G.J., Sakallah, K.A., Rutenbar, R.A.: Satisfiability-Based Layout Revisited: Detailed Routing of Complex FPGAs Via Search-Based Boolean SAT. In: ACM\/SIGDA International Symposium on FPGAs (1999)","DOI":"10.1145\/296399.296450"},{"key":"27_CR14","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: Conflict Analysis in Search Algorithms for Propositional Satisfiability. In: IEEE International Conference on Tools with Artificial Intelligence (1996)"},{"key":"27_CR15","doi-asserted-by":"crossref","unstructured":"Bayardo, R., Schrag, R.: Using CSP look-back techniques to solve real-world SAT instances. In: National Conference on Artificial Intelligence, AAAI (1997)","DOI":"10.1007\/3-540-61551-2_65"},{"key":"27_CR16","doi-asserted-by":"crossref","unstructured":"Zhang, H.: SATO: An efficient propositional prover. In: International Conference on Automated Deduction (1997)","DOI":"10.1007\/3-540-63104-6_28"},{"key":"27_CR17","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: 38th DAC (2001)","DOI":"10.1145\/378239.379017"},{"key":"27_CR18","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: BerkMin: A Fast and Robust SAT Solver. In: DATE (2002)","DOI":"10.1109\/DATE.2002.998262"},{"key":"27_CR19","unstructured":"Siege Satisfiability Solver (2004), http:\/\/www.cs.sfu.ca\/~loryan\/personal\/"},{"key":"27_CR20","unstructured":"SAT Competition (2003), http:\/\/www.satlive.org\/SATCompetition\/2003\/ (2004)"},{"key":"27_CR21","unstructured":"SAT Competition (2004), http:\/\/www.satlive.org\/SATCompetition\/2004\/"},{"key":"27_CR22","unstructured":"http:\/\/www.cs.washington.edu\/homes\/kautz\/satplan\/blackbox\/ (2004)"},{"key":"27_CR23","unstructured":"NuSMW Home Page (2004), http:\/\/nusmv.irst.itc.it\/"},{"key":"27_CR24","unstructured":"GrAnDe (2004), http:\/\/www.cs.miami.edu\/~tptp\/ATPSystems\/GrAnDe\/"},{"key":"27_CR25","doi-asserted-by":"crossref","unstructured":"SAT Competition (2002), http:\/\/www.satlive.org\/SATCompetition\/2002\/ (2004)","DOI":"10.1145\/504689.504690"},{"key":"27_CR26","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D.A. Plaisted","year":"1986","unstructured":"Plaisted, D.A., Greenbaum, S.: A stucture-preserving clause form translation. Journal of Symbolic Computation\u00a02, 293\u2013304 (1986)","journal-title":"Journal of Symbolic Computation"},{"key":"27_CR27","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP - A New Search Algorithm for Satisfiability. In: IEEE International Conf. on Tools with Artificial Intelligence (1996)","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"27_CR28","unstructured":"Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient conflict driven learning in boolean satisfiability solver. In: ICCAD, pp. 279\u2013285 (2001)"},{"key":"27_CR29","unstructured":"Li, C.M.: Integrating Equivalency reasoning into Davis-Putnam procedure. In: AAAI 2000 (2000)"},{"key":"27_CR30","unstructured":"Freeman, J.W.: Improvements to propositional satisfiability search algorithms. PhD thesis, University of Pennsylvania (1995)"},{"key":"27_CR31","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.P.: The impact of branching heuristics in propositional satisfiability algorithms. In: 9th Portuguese Conf. on Artificial Intelligence (1999)","DOI":"10.1007\/3-540-48159-1_5"},{"key":"27_CR32","series-title":"PhD thesis","volume-title":"Searching for Truth: Techniques for Satisfiability of Boolean Formulas","author":"L. Zhang","year":"2003","unstructured":"Zhang, L.: Searching for Truth: Techniques for Satisfiability of Boolean Formulas. PhD thesis. Princeton University, Princeton (2003)"},{"key":"27_CR33","unstructured":"Crawford, J., Auton, L.: Experimental results on the cross-over point in satisfiability problems. In: National Conf. on Artificial Intelligence, AAAI 1993 (1993)"},{"key":"27_CR34","unstructured":"Zhang, H., Stickel, M.: An efficient algorithm for unit-propagation. In: Fourth International Symposium on Artificial Intelligence and Mathematics, Florida (1996)"},{"key":"27_CR35","unstructured":"Nadel, A.: The Jerusat SAT Solver. Master\u2019s thesis. Hebrew University of Jerusalem (2002)"},{"key":"27_CR36","doi-asserted-by":"crossref","unstructured":"Pilarski, S., Hu, G.: Speeding up SAT for EDA. In: DATE (2002)","DOI":"10.1109\/DATE.2002.998437"},{"key":"27_CR37","unstructured":"Kautz, H., Horvitz, E., Ruan, Y., Gomes, C., Selman, B.: Dynamic restart policies. In: The 18th National Conf. on Artificial Intelligence (2002)"},{"key":"27_CR38","unstructured":"http:\/\/www2.inf.ethz.ch\/personal\/biere\/projects\/limmat\/ (2004)"}],"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\/11527695_27.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,28]],"date-time":"2025-02-28T23:57:24Z","timestamp":1740787044000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11527695_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540278290","9783540315803"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/11527695_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}