{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,20]],"date-time":"2026-01-20T06:36:22Z","timestamp":1768890982580,"version":"3.49.0"},"reference-count":50,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2003,3,1]],"date-time":"2003-03-01T00:00:00Z","timestamp":1046476800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,3,1]],"date-time":"2003-03-01T00:00:00Z","timestamp":1046476800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Annals of Mathematics and Artificial Intelligence"],"published-print":{"date-parts":[[2003,3]]},"DOI":"10.1023\/a:1021264516079","type":"journal-article","created":{"date-parts":[[2003,3,21]],"date-time":"2003-03-21T00:56:49Z","timestamp":1048208209000},"page":"307-326","source":"Crossref","is-referenced-by-count":12,"title":["An Overview of Backtrack Search Satisfiability Algorithms"],"prefix":"10.1007","volume":"37","author":[{"given":"In\u00eas","family":"Lynce","sequence":"first","affiliation":[]},{"given":"Jo\u00e3o P.","family":"Marques-Silva","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5098010_CR1","doi-asserted-by":"crossref","unstructured":"L. Baptista and J.P. Marques-Silva, Using randomization and learning to solve hard real-world instances of satisfiability, in: International Conference on Principles and Practice of Constraint Programming (September 2000) pp. 489\u2013494.","DOI":"10.1007\/3-540-45349-0_36"},{"key":"5098010_CR2","unstructured":"P. Barth, ADavis-Putnam enumeration procedure for linear pseudo-Boolean optimization, Technical Report MPI-I-2-003, MPI (January 1995)."},{"key":"5098010_CR3","unstructured":"R. Bayardo Jr. and R. Schrag, Using CSP look-back techniques to solve real-world SAT instances, in: Proceedings of the National Conference on Artificial Intelligence (1997) pp. 203\u2013208."},{"issue":"5","key":"5098010_CR4","doi-asserted-by":"crossref","first-page":"633","DOI":"10.1016\/0305-0548(86)90056-0","volume":"13","author":"C.E. Blair","year":"1986","unstructured":"C.E. Blair, R.G. Jeroslow and J.K. Lowe, Some results and experiments in programming techniques for propositional logic, Computers and Operations Research 13(5) (1986) 633\u2013645.","journal-title":"Computers and Operations Research"},{"key":"5098010_CR5","unstructured":"M. B\u00f6hm and E. Speckenmeyer, A fast parallel SAT-solver - efficient workload balancing, in: Third International Symposium on Artificial Intelligence and Mathematics (1994)."},{"key":"5098010_CR6","unstructured":"M. Buro and H. Kleine-B\u00fcning, Report on a SAT competition, Technical Report, University of Paderborn (November 1992)."},{"key":"5098010_CR7","doi-asserted-by":"crossref","unstructured":"O. Coudert, On solving covering problems, in: Proceedings of the ACM\/IEEE Design Automation Conference (June 1996) pp. 197\u2013202.","DOI":"10.1109\/DAC.1996.545572"},{"key":"5098010_CR8","doi-asserted-by":"crossref","unstructured":"O. Coudert and J.C. Madre, New ideas for solving covering problems, in: Proceedings of the ACM\/IEEE Design Automation Conference (June 1995).","DOI":"10.1145\/217474.217603"},{"key":"5098010_CR9","unstructured":"J. Crawford and L. Auton, Experimental results on the cross-over point in satisfiability problems, in: Proceedings of the National Conference on Artificial Intelligence (1993) pp. 22\u201328."},{"key":"5098010_CR10","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"M. Davis, G. Logemann and D. Loveland, A machine program for theorem-proving, Communications of the ACM 5 (July 1962) 394\u2013397.","journal-title":"Communications of the ACM"},{"key":"5098010_CR11","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"M. Davis and H. Putnam, A computing procedure for quantification theory, Journal of the ACM 7 (1960) 201\u2013215.","journal-title":"Journal of the ACM"},{"key":"5098010_CR12","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1016\/0004-3702(86)90080-9","volume":"28","author":"J. de Kleer","year":"1986","unstructured":"J. de Kleer, An assumption-based TMS, Artificial Intelligence 28 (1986) 127\u2013162.","journal-title":"Artificial Intelligence"},{"key":"5098010_CR13","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1016\/0004-3702(90)90046-3","volume":"41","author":"R. Dechter","year":"1989","unstructured":"R. Dechter, Enhancement schemes for constraint processing: Backjumping, learning, and cutset decomposition, Artificial Intelligence 41 (1989\/1990) 273\u2013312.","journal-title":"Artificial Intelligence"},{"key":"5098010_CR14","unstructured":"O. Dubois, P. Andre, Y. Boufkhad and J. Carlier, SAT versus UNSAT, in: Second DIMACS Implementation Challenge, eds. D.S. Johnson and M.A. Trick (American Mathematical Society, 1993)."},{"key":"5098010_CR15","volume-title":"Improvements to propositional satisfiability search algorithms","author":"J.W. Freeman","year":"1995","unstructured":"J.W. Freeman, Improvements to propositional satisfiability search algorithms, PhD thesis, University of Pennsylvania, Philadelphia, PA (May 1995)."},{"key":"5098010_CR16","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/0743-1066(89)90009-5","volume":"7","author":"G. Gallo","year":"1989","unstructured":"G. Gallo and G. Urbani, Algorithms for testing the satisfiability of propositional formulae, Journal of Logic Programming 7 (1989) 45\u201361.","journal-title":"Journal of Logic Programming"},{"key":"5098010_CR17","volume-title":"Performance measurement and analysis of certain search algorithms","author":"J. Gaschnig","year":"1979","unstructured":"J. Gaschnig, Performance measurement and analysis of certain search algorithms, PhD thesis, Carnegie-Mellon University, Pittsburgh, PA (May 1979)."},{"key":"5098010_CR18","unstructured":"A.V. Gelder and Y.K. Tsuji, Satisfiability testing with more reasoning and less guessing, in: Second DIMACS Implementation Challenge, eds. D.S. Johnson and M.A. Trick (American Mathematical Society, 1993)."},{"key":"5098010_CR19","unstructured":"C.P. Gomes and B. Selman, Algorithm portfolio design: theory vs. practice. in: Proceedings of the Thirteenth Conference on Uncertainty in Artificial Intelligence (1997)."},{"issue":"1\/2","key":"5098010_CR20","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1023\/A:1006314320276","volume":"24","author":"C.P. Gomes","year":"2000","unstructured":"C.P. Gomes, B. Selman, N. Crato and H. Kautz, Heavy-tailed phenomena in satisfiability and constraint satisfaction problems, Journal of Automated Reasoning 24(1\/2) (2000) 67\u2013100.","journal-title":"Journal of Automated Reasoning"},{"key":"5098010_CR21","unstructured":"C.P. Gomes, B. Selman and H. Kautz, Boosting combinatorial search through randomization, in: Proceedings of the National Conference on Artificial Intelligence (July 1998)."},{"key":"5098010_CR22","unstructured":"J.F. Groote and J.P. Warners, The propositional formula checker Heerhugo, in: SAT 2000, eds. I. Gent, H. van Maaren and T. Walsh (IOS Press, 2000) pp. 261\u2013281."},{"key":"5098010_CR23","doi-asserted-by":"crossref","unstructured":"J. Franco, J. Gu, P.W. Purdom and B.W. Wah, Algorithms for the satisfiability (SAT) problem: A survey, in: Satisfiability Problem: Theory and Applications, DIMACS Series in Discrete Mathematics and Theoretical Computer Science (American Mathematical Society, 1997) pp. 19\u2013152.","DOI":"10.1090\/dimacs\/035\/02"},{"key":"5098010_CR24","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/BF00881805","volume":"15","author":"J.N. Hooker","year":"1995","unstructured":"J.N. Hooker and V. Vinay, Branching rules for satisfiability, Journal of Automated Reasoning 15 (1995) 359\u2013383.","journal-title":"Journal of Automated Reasoning"},{"key":"5098010_CR25","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/BF01531077","volume":"1","author":"R.G. Jeroslow","year":"1990","unstructured":"R.G. Jeroslow and J. Wang, Solving propositional satisfiability problems, Annals of Mathematics and Artificial Intelligence 1 (1990) 167\u2013187.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"5098010_CR26","unstructured":"D.S. Johnson and M.A. Trick (eds.), Second DIMACS Implementation Challenge (American Mathematical Society, 1993). DIMACS SAT instances available from URL ftp:\/\/dimacs.rutgers.edu\/pub\/challenge\/sat\/benchmarks\/cnf."},{"key":"5098010_CR27","unstructured":"S. Kim and H. Zhang, ModGen: Theorem proving by model generation, in: Proceedings of the National Conference on Artificial Intelligence (1994) pp. 162\u2013167."},{"key":"5098010_CR28","doi-asserted-by":"crossref","unstructured":"W. Kunz and D. Stoffel, Reasoning in Boolean Networks (Kluwer Academic, 1997).","DOI":"10.1007\/978-1-4757-2572-8"},{"issue":"1","key":"5098010_CR29","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1109\/43.108614","volume":"11","author":"T. Larrabee","year":"1992","unstructured":"T. Larrabee, Test pattern generation using Boolean satisfiability, IEEE Transactions on Computer-Aided Design 11(1) (1992) 4\u201315.","journal-title":"IEEE Transactions on Computer-Aided Design"},{"key":"5098010_CR30","unstructured":"C.-M. Li, Integrating equivalency reasoning into Davis-Putnam procedure, in: Proceedings of the National Conference on Artificial Intelligence (July 2000) pp. 291\u2013296."},{"key":"5098010_CR31","unstructured":"C.-M. Li and Anbulagan, Look-ahead versus look-back for satisfiability problems, in: International Conference on Principles and Practice of Constraint Programming (1997)."},{"key":"5098010_CR32","unstructured":"J.P. Marques-Silva, Improving satisfiability algorithms by using recursive learning, in: Proceedings of the International Workshop on Boolean Problems (September 1998) pp. 47\u201358."},{"key":"5098010_CR33","doi-asserted-by":"crossref","unstructured":"J.P. Marques-Silva, Algebraic simplification techniques for propositional satisfiability, in: International Conference on Principles and Practice of Constraint Programming (September 2000) pp. 537\u2013542.","DOI":"10.1007\/3-540-45349-0_45"},{"key":"5098010_CR34","unstructured":"J.P. Marques-Silva and A.L. Oliveira, Improving satisfiability algorithms with dominance and partitioning, in: Proceedings of the ACM\/IEEE International Workshop on Logic Synthesis (May 1997)."},{"key":"5098010_CR35","doi-asserted-by":"crossref","unstructured":"J.P. Marques-Silva and K.A. Sakallah, GRASP: A new search algorithm for satisfiability, in: Proceedings of the ACM\/IEEE International Conference on Computer-Aided Design (November 1996) pp. 220\u2013227.","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"5098010_CR36","unstructured":"M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang and S. Malik, Engineering an efficient SAT solver, in: Proceedings of the Design Automation Conference (2001)."},{"key":"5098010_CR37","unstructured":"D. Pretolani, Efficiency and stability of hypergraph SAT algorithms, in: Second DIMACS Implementation Challenge, eds. D.S. Johnson and M.A. Trick (American Mathematical Society, 1993)."},{"key":"5098010_CR38","unstructured":"A. Saldanha and V. Singhal, Solving satisfiability in CAD problems, in: Proceedings of the Cadence Technical Conference (May 1997) pp. 191\u2013195."},{"key":"5098010_CR39","doi-asserted-by":"crossref","unstructured":"T. Schiex and G. Verfaillie, Nogood recording for static and dynamic constraint satisfaction problems, in: Proceedings of the International Conference on Tools with Artificial Intelligence (1993) pp. 48\u201355.","DOI":"10.1109\/TAI.1993.633935"},{"key":"5098010_CR40","unstructured":"B. Selman and H. Kautz, Domain-independent extensions to GSAT: Solving large structured satisfiability problems, in: Proceedings of the International Joint Conference on Artificial Intelligence (1993) pp. 290\u2013295."},{"key":"5098010_CR41","unstructured":"B. Selman, H. Levesque and D. Mitchell, A new method for solving hard satisfiability problems, in: Proceedings of the National Conference on Artificial Intelligence (1992) pp. 440\u2013446."},{"key":"5098010_CR42","doi-asserted-by":"crossref","unstructured":"C. Sinz, W. Blochinger and W. K\u00fcchlin, PaSAT: Parallel SAT-checking with lemma exchange: implementation and applications, in: LICS Workshop on Theory and Applications of Satisfiability Testing, Electronic Notes in Discrete Mathematics (Elsevier Science, June 2001).","DOI":"10.1016\/S1571-0653(04)00323-3"},{"key":"5098010_CR43","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0004-3702(77)90029-7","volume":"9","author":"R.M. Stallman","year":"1977","unstructured":"R.M. Stallman and G.J. Sussman, Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis, Artificial Intelligence 9 (October 1977) 135\u2013196.","journal-title":"Artificial Intelligence"},{"key":"5098010_CR44","unstructured":"G. St\u00e5lmarck, A system for determining propositional logic theorems by applying values and rules to triplets that are generated from a formula (1989). Swedish Patent 467 076 (approved 1992); US Patent 5 276 897 (approved 1994); European Patent 0 403 454 (approved 1995)."},{"issue":"9","key":"5098010_CR45","doi-asserted-by":"crossref","first-page":"1167","DOI":"10.1109\/43.536723","volume":"15","author":"P.R. Stephan","year":"1996","unstructured":"P.R. Stephan, R.K. Brayton and A.L. Sangiovanni-Vincentelli, Combinational test generation using satisfiability, IEEE Transactions on Computer-Aided Design 15(9) (September 1996) 1167\u20131176.","journal-title":"IEEE Transactions on Computer-Aided Design"},{"issue":"1","key":"5098010_CR46","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1137\/0203006","volume":"3","author":"R.E. Tarjan","year":"1974","unstructured":"R.E. Tarjan, Finding dominators in directed graphs, SIAM Journal on Computing 3(1) (1974) 62\u201389.","journal-title":"SIAM Journal on Computing"},{"key":"5098010_CR47","doi-asserted-by":"crossref","unstructured":"M. Yokoo, Asynchronous weak-commitment search for solving distributed constraint satisfaction problems, in: Proceedings of International Conference on Principles and Practice of Constraint Programming (1995).","DOI":"10.1007\/3-540-60299-2_6"},{"key":"5098010_CR48","unstructured":"R. Zabih and D.A. McAllester, A rearrangement search strategy for determining propositional satisfiability, in: Proceedings of the National Conference on Artificial Intelligence (1988) pp. 155\u2013160."},{"key":"5098010_CR49","doi-asserted-by":"crossref","unstructured":"H. Zhang, SATO: An efficient propositional prover, in: Proceedings of the International Conference on Automated Deduction (July 1997) pp. 272\u2013275.","DOI":"10.1007\/3-540-63104-6_28"},{"key":"5098010_CR50","doi-asserted-by":"crossref","unstructured":"H. Zhang, M.P. Bonacina and J. Hsiang, PSATO: a distributed propositional prover and its application to quasigroup problems, Journal of Symbolic Computation (1996) 1\u201318.","DOI":"10.1006\/jsco.1996.0030"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1021264516079.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1021264516079\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1021264516079.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T05:49:18Z","timestamp":1747547358000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1021264516079"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,3]]},"references-count":50,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2003,3]]}},"alternative-id":["5098010"],"URL":"https:\/\/doi.org\/10.1023\/a:1021264516079","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003,3]]}}}