{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T06:17:44Z","timestamp":1773901064043,"version":"3.50.1"},"reference-count":200,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2006,12,25]],"date-time":"2006-12-25T00:00:00Z","timestamp":1167004800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Comput. Surv."],"published-print":{"date-parts":[[2006,12,25]]},"abstract":"<jats:p>Propositional Satisfiability (SAT) and Constraint Programming (CP) have developed as two relatively independent threads of research cross-fertilizing occasionally. These two approaches to problem solving have a lot in common as evidenced by similar ideas underlying the branch and prune algorithms that are most successful at solving both kinds of problems. They also exhibit differences in the way they are used to state and solve problems since SAT's approach is, in general, a black-box approach, while CP aims at being tunable and programmable. This survey overviews the two areas in a comparative way, emphasizing the similarities and differences between the two and the points where we feel that one technology can benefit from ideas or experience acquired from the other.<\/jats:p>","DOI":"10.1145\/1177352.1177354","type":"journal-article","created":{"date-parts":[[2007,1,16]],"date-time":"2007-01-16T19:38:29Z","timestamp":1168976309000},"page":"12","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":65,"title":["Propositional Satisfiability and Constraint Programming"],"prefix":"10.1145","volume":"38","author":[{"given":"Lucas","family":"Bordeaux","sequence":"first","affiliation":[{"name":"Microsoft Research, Cambridge, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Youssef","family":"Hamadi","sequence":"additional","affiliation":[{"name":"Microsoft Research, Cambridge, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lintao","family":"Zhang","sequence":"additional","affiliation":[{"name":"Microsoft Research, La Avenida Mountain View, CA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2006,12,25]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/309847.310028"},{"key":"e_1_2_1_2_1","volume-title":"International Joint Conference on Artificial Intelligence (IJCAI). 351--356","author":"Adjiman P.","unstructured":"Adjiman , P. , Chatalic , P. , Goasdou E, F. , Rousset , M.-C. , and Simon , L . 2005. Scalability study of peer-to-peer consequence finding . International Joint Conference on Artificial Intelligence (IJCAI). 351--356 .]] Adjiman, P., Chatalic, P., GoasdouE, F., Rousset, M.-C., and Simon, L. 2005. Scalability study of peer-to-peer consequence finding. International Joint Conference on Artificial Intelligence (IJCAI). 351--356.]]"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/775832.776042"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00032-8"},{"key":"e_1_2_1_5_1","volume-title":"International Joint. Conference on Artificial Intelligence (IJCAI). 35--40","author":"Bacchus F.","unstructured":"Bacchus , F. and Walsh , T . 2005. Propagating logical combinations of constraints . International Joint. Conference on Artificial Intelligence (IJCAI). 35--40 .]] Bacchus, F. and Walsh, T. 2005. Propagating logical combinations of constraints. International Joint. Conference on Artificial Intelligence (IJCAI). 35--40.]]"},{"key":"e_1_2_1_6_1","volume-title":"International Conference on Theory and Applications of Satisfiability Testing (SAT). 341--355","author":"Bacchus F.","unstructured":"Bacchus , F. and Winter , J . 2003. Effective preprocessing with hyper-resolution and equality reduction . International Conference on Theory and Applications of Satisfiability Testing (SAT). 341--355 .]] Bacchus, F. and Winter, J. 2003. Effective preprocessing with hyper-resolution and equality reduction. International Conference on Theory and Applications of Satisfiability Testing (SAT). 341--355.]]"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_4"},{"key":"e_1_2_1_8_1","volume-title":"International Conference on Computer-Aided Verification (CAV). 236--249","author":"Barrett C.","unstructured":"Barrett , C. , Dill , D. , and Stump , A . 2002. Checking satisfiability of first-order formulas by incremental translation to SAT . In International Conference on Computer-Aided Verification (CAV). 236--249 .]] Barrett, C., Dill, D., and Stump, A. 2002. Checking satisfiability of first-order formulas by incremental translation to SAT. In International Conference on Computer-Aided Verification (CAV). 236--249.]]"},{"key":"e_1_2_1_9_1","volume-title":"A Davis-Putnam based enumeration algorithm for linear pseudo-Boolean optimization. Tech. rep. 95-2-003","author":"Bart P.","unstructured":"Bart , P. 1995. A Davis-Putnam based enumeration algorithm for linear pseudo-Boolean optimization. Tech. rep. 95-2-003 , Max Planck Institute .]] Bart, P. 1995. A Davis-Putnam based enumeration algorithm for linear pseudo-Boolean optimization. Tech. rep. 95-2-003, Max Planck Institute.]]"},{"key":"e_1_2_1_10_1","volume-title":"North American National Conference on Artificial Intelligence (AAAI). 203--208","author":"Bayardo R. J.","unstructured":"Bayardo , R. J. and Schrag , R. C . 1997. Using CSP look-back techniques to solve real world SAT instances . North American National Conference on Artificial Intelligence (AAAI). 203--208 .]] Bayardo, R. J. and Schrag, R. C. 1997. Using CSP look-back techniques to solve real world SAT instances. North American National Conference on Artificial Intelligence (AAAI). 203--208.]]"},{"key":"e_1_2_1_11_1","volume-title":"-X","author":"Beldiceanu N.","year":"2005","unstructured":"Beldiceanu , N. , Carlsson , M. , and Rampon , J . -X . 2005 . Global constraint catalog. Tech. rep. T2005-08, Swedish Institute of Computer Science .]] Beldiceanu, N., Carlsson, M., and Rampon, J.-X. 2005. Global constraint catalog. Tech. rep. T2005-08, Swedish Institute of Computer Science.]]"},{"key":"e_1_2_1_12_1","first-page":"87","article-title":"Introducing global constraints in CHIP","volume":"20","author":"Beldiceanu N.","year":"1994","unstructured":"Beldiceanu , N. and Contejean , E. 1994 . Introducing global constraints in CHIP . Mathem. Comput. model. 20 , 12, 87 -- 123 .]] Beldiceanu, N. and Contejean, E. 1994. Introducing global constraints in CHIP. Mathem. Comput. model. 20, 12, 87--123.]]","journal-title":"Mathem. Comput. model."},{"key":"e_1_2_1_13_1","volume-title":"Dynamic Programming","author":"Bellman R.","unstructured":"Bellman , R. 1957. Dynamic Programming . Princeton University Press .]] Bellman, R. 1957. Dynamic Programming. Princeton University Press.]]"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(96)00142-2"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(94)90041-8"},{"key":"e_1_2_1_16_1","volume-title":"International Joint Conference on Artificial Intelligence (IJCAI). 592--599","author":"Bessi\u00e8re C.","unstructured":"Bessi\u00e8re , C. , Freuder , E. C. , and R\u00e9gin , J . -C. 1995. Using inference to reduce arc consistency computation . International Joint Conference on Artificial Intelligence (IJCAI). 592--599 .]] Bessi\u00e8re, C., Freuder, E. C., and R\u00e9gin, J.-C. 1995. Using inference to reduce arc consistency computation. International Joint Conference on Artificial Intelligence (IJCAI). 592--599.]]"},{"key":"e_1_2_1_17_1","volume-title":"International Conference on Theory and Applications of Satisfiability Testing (SAT). 299--314","author":"Bessi\u00e8re C.","unstructured":"Bessi\u00e8re , C. , H\u00e9brard , E. , and Walsh , T . 2003. Local consistencies in SAT . International Conference on Theory and Applications of Satisfiability Testing (SAT). 299--314 .]] Bessi\u00e8re, C., H\u00e9brard, E., and Walsh, T. 2003. Local consistencies in SAT. International Conference on Theory and Applications of Satisfiability Testing (SAT). 299--314.]]"},{"key":"e_1_2_1_18_1","volume-title":"International Conference on Principles and Practice of Constraint Programming (CP). 61--75","author":"Bessi\u00e8re C.","unstructured":"Bessi\u00e8re , C. and R\u00e9gin , J . -C. 1996. MAC and combined heuristics: Two reasons to forsake FC (and CBJ&quest;) on hard problems . In International Conference on Principles and Practice of Constraint Programming (CP). 61--75 .]] Bessi\u00e8re, C. and R\u00e9gin, J.-C. 1996. MAC and combined heuristics: Two reasons to forsake FC (and CBJ&quest;) on hard problems. In International Conference on Principles and Practice of Constraint Programming (CP). 61--75.]]"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/1099149.1644564"},{"key":"e_1_2_1_20_1","volume-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 193--207","author":"Biere A.","unstructured":"Biere , A. , Cimatti , A. , Clarke , E. M. , and Zhu , Y . 1999. Symbolic model checking without BDDs . International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 193--207 .]] Biere, A., Cimatti, A., Clarke, E. M., and Zhu, Y. 1999. Symbolic model checking without BDDs. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 193--207.]]"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1026441215081"},{"key":"e_1_2_1_22_1","volume-title":"IEEE\/ACM International Symposium on Cluster Computing and the Grid.]]","author":"Blochinger W.","unstructured":"Blochinger , W. , Westje , W. , K\u00fcchlin , W. , and Wedeniwski , S . 2005. ZetaSAT---Boolean satisfiability solving on desktop grids . In IEEE\/ACM International Symposium on Cluster Computing and the Grid.]] Blochinger, W., Westje, W., K\u00fcchlin, W., and Wedeniwski, S. 2005. ZetaSAT---Boolean satisfiability solving on desktop grids. In IEEE\/ACM International Symposium on Cluster Computing and the Grid.]]"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/359094.359101"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(81)90074-0"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_1_26_1","volume-title":"International Conference on Computer-Aided Verification (CAV). 209--222","author":"Bryant R. E.","unstructured":"Bryant , R. E. , Lahiri , S. K. , and Seshia , S. A . 2002. Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions . In International Conference on Computer-Aided Verification (CAV). 209--222 .]] Bryant, R. E., Lahiri, S. K., and Seshia, S. A. 2002. Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In International Conference on Computer-Aided Verification (CAV). 209--222.]]"},{"key":"e_1_2_1_27_1","volume-title":"International Conference on Computer-Aided Verification (CAV). 68--80","author":"Burch J. R.","unstructured":"Burch , J. R. and Dill , D . 1994. Automatic verification of pipelined microprocessor control . In International Conference on Computer-Aided Verification (CAV). 68--80 .]] Burch, J. R. and Dill, D. 1994. Automatic verification of pipelined microprocessor control. In International Conference on Computer-Aided Verification (CAV). 68--80.]]"},{"key":"e_1_2_1_28_1","first-page":"143","article-title":"Report on a SAT competition","volume":"49","author":"Buro M.","year":"1993","unstructured":"Buro , M. and B\u00fcning , H. K. 1993 . Report on a SAT competition . Bull. Europ. Assoc. Theoret. Comput. Science 49 , 143 -- 151 .]] Buro, M. and B\u00fcning, H. K. 1993. Report on a SAT competition. Bull. Europ. Assoc. Theoret. Comput. Science 49, 143--151.]]","journal-title":"Bull. Europ. Assoc. Theoret. Comput. Science"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2006.01.008"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/127601.127693"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0218213001000611"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1048935.1050188"},{"key":"e_1_2_1_33_1","volume-title":"Linear Programming","author":"Chvatal V.","unstructured":"Chvatal , V. 1983. Linear Programming . W. H. Freeman Co. ]] Chvatal, V. 1983. Linear Programming. W. H. Freeman Co.]]"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"e_1_2_1_35_1","first-page":"125","article-title":"Logical arithmetic","volume":"2","author":"Cleary J. G.","year":"1987","unstructured":"Cleary , J. G. 1987 . Logical arithmetic . Future Comput. Syst. 2 , 2, 125 -- 149 .]] Cleary, J. G. 1987. Logical arithmetic. Future Comput. Syst. 2, 2, 125--149.]]","journal-title":"Future Comput. Syst."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(95)00121-2"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_12"},{"key":"e_1_2_1_38_1","volume-title":"International Conference on Fifth Generation Computing. 85--99","author":"Colmerauer A.","year":"1984","unstructured":"Colmerauer , A. 1984 . Equations and inequations on finite and infinite tress . International Conference on Fifth Generation Computing. 85--99 .]] Colmerauer, A. 1984. Equations and inequations on finite and infinite tress. International Conference on Fifth Generation Computing. 85--99.]]"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/79204.79210"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/800228.806926"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/605440.605444"},{"key":"e_1_2_1_42_1","volume-title":"Computing and Combinatorics Conference (COCOON). 171--180","author":"Dantsin E.","unstructured":"Dantsin , E. and Wolpert , A . 2002. Solving constraint satisfaction problems with DNA computing . Computing and Combinatorics Conference (COCOON). 171--180 .]] Dantsin, E. and Wolpert, A. 2002. Solving constraint satisfaction problems with DNA computing. Computing and Combinatorics Conference (COCOON). 171--180.]]"},{"key":"e_1_2_1_43_1","volume-title":"North American National Conference on Artificial Intelligence (AAAI). 325--330","author":"Davenport A. J.","unstructured":"Davenport , A. J. , Tsang , E. P. K. , Wang , C. J. , and Zhu , K . 1994. GENET: A connectionist architecture for solving constraint satisfaction problems by iterative improvement . North American National Conference on Artificial Intelligence (AAAI). 325--330 .]] Davenport, A. J., Tsang, E. P. K., Wang, C. J., and Zhu, K. 1994. GENET: A connectionist architecture for solving constraint satisfaction problems by iterative improvement. North American National Conference on Artificial Intelligence (AAAI). 325--330.]]"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(87)90091-9"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.5555\/1622394.1622402"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(90)90046-3"},{"key":"e_1_2_1_49_1","unstructured":"Dechter R. 2003. Constraint Processing. Morgan Kaufmann.]] Dechter R. 2003. Constraint Processing. Morgan Kaufmann.]]"},{"key":"e_1_2_1_50_1","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/s100090100049","article-title":"Constraint-based deductive model checking","volume":"3","author":"Delzanno G.","year":"2001","unstructured":"Delzanno , G. and Podelski , A. 2001 . Constraint-based deductive model checking . Int. J. Softw. Tools Technol. Transfer 3 , 3, 250 -- 270 .]] Delzanno, G. and Podelski, A. 2001. Constraint-based deductive model checking. Int. J. Softw. Tools Technol. Transfer 3, 3, 250--270.]]","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/11499107_4"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.5555\/1622487.1622502"},{"key":"e_1_2_1_53_1","doi-asserted-by":"crossref","unstructured":"Dorigo M. and Stutzle T. 2004. Ant Colony Optimization. MIT Press.]] Dorigo M. and Stutzle T. 2004. Ant Colony Optimization. MIT Press.]]","DOI":"10.7551\/mitpress\/1290.001.0001"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/11499107_5"},{"key":"e_1_2_1_55_1","volume-title":"North American National Conference on Artificial Intelligence (AAAI). 161--166","author":"Fang H.","unstructured":"Fang , H. and Ruml , W . 2004. Complete local search for propositional satisfiability . North American National Conference on Artificial Intelligence (AAAI). 161--166 .]] Fang, H. and Ruml, W. 2004. Complete local search for propositional satisfiability. North American National Conference on Artificial Intelligence (AAAI). 161--166.]]"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.10.020"},{"key":"e_1_2_1_57_1","doi-asserted-by":"crossref","unstructured":"Fikes R. 1970. REF-ARF: A system for solving problems stated as procedures. Artific. Intell. 1 1\/2 27--120.]] Fikes R. 1970. REF-ARF: A system for solving problems stated as procedures. Artific. Intell. 1 1\/2 27--120.]]","DOI":"10.1016\/0004-3702(70)90003-2"},{"key":"e_1_2_1_58_1","volume-title":"International Conference on Computer-Aided Verification (CAV). 355--367","author":"Flanagan C.","unstructured":"Flanagan , C. , Joshi , R. , Ou , X. , and Saxe , J. B . 2003. Theorem proving using lazy proof explication . International Conference on Computer-Aided Verification (CAV). 355--367 .]] Flanagan, C., Joshi, R., Ou, X., and Saxe, J. B. 2003. Theorem proving using lazy proof explication. International Conference on Computer-Aided Verification (CAV). 355--367.]]"},{"key":"e_1_2_1_59_1","volume-title":"AMPL: A Modeling Language for Mathematical Programming","author":"Fourer R.","year":"1993","unstructured":"Fourer , R. , Gay , D. , and Kernighan , B . 1993 . AMPL: A Modeling Language for Mathematical Programming . Duxbury Press .]] Fourer, R., Gay, D., and Kernighan, B. 1993. AMPL: A Modeling Language for Mathematical Programming. Duxbury Press.]]"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/359642.359654"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(92)90004-H"},{"key":"e_1_2_1_63_1","volume-title":"International Joint Conference on Artificial Intelligence (IJCAI). 109--117","author":"Frisch A. M.","unstructured":"Frisch , A. M. , Jefferson , C. , Martinez-Hernandez , B. , and Miguel , I . 2005. The rules of constraint modeling . International Joint Conference on Artificial Intelligence (IJCAI). 109--117 .]] Frisch, A. M., Jefferson, C., Martinez-Hernandez, B., and Miguel, I. 2005. The rules of constraint modeling. International Joint Conference on Artificial Intelligence (IJCAI). 109--117.]]"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/513918.514105"},{"key":"e_1_2_1_65_1","volume-title":"International Conference on Computer-Aided Verification (CAV). 440--452","author":"Ganai M. K.","unstructured":"Ganai , M. K. , Gupta , A. , and Ashar , P . 2004. Efficient modeling of embedded memories in bounded model checking . International Conference on Computer-Aided Verification (CAV). 440--452 .]] Ganai, M. K., Gupta, A., and Ashar, P. 2004. Efficient modeling of embedded memories in bounded model checking. International Conference on Computer-Aided Verification (CAV). 440--452.]]"},{"key":"e_1_2_1_66_1","volume-title":"Performance measurement and analysis of certain search algorithms. Tech. rep. CMU-CS-79-124","author":"Gaschnig J.","unstructured":"Gaschnig , J. 1979. Performance measurement and analysis of certain search algorithms. Tech. rep. CMU-CS-79-124 , Carnegie-Mellon University .]] Gaschnig, J. 1979. Performance measurement and analysis of certain search algorithms. Tech. rep. CMU-CS-79-124, Carnegie-Mellon University.]]"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0166-218X(99)00205-X"},{"key":"e_1_2_1_68_1","volume-title":"European Conference on Artificial Intelligence (ECAI). 599--603","author":"Gent I. P.","unstructured":"Gent , I. P. and Smith , B. M . 2000. Symmetry breaking in constraint programming . In European Conference on Artificial Intelligence (ECAI). 599--603 .]] Gent, I. P. and Smith, B. M. 2000. Symmetry breaking in constraint programming. In European Conference on Artificial Intelligence (ECAI). 599--603.]]"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.5555\/1618595.1618597"},{"key":"e_1_2_1_70_1","volume-title":"North American National Conference on Artificial Intelligence (AAAI). 334--339","author":"Ginsberg M. L.","unstructured":"Ginsberg , M. L. , Parkes , A. J. , and Roy , A . 1998. Supermodels and robustness . North American National Conference on Artificial Intelligence (AAAI). 334--339 .]] Ginsberg, M. L., Parkes, A. J., and Roy, A. 1998. Supermodels and robustness. North American National Conference on Artificial Intelligence (AAAI). 334--339.]]"},{"key":"e_1_2_1_71_1","volume-title":"European Conference on Logic in Artificial Intelligence (JELIA). 296--307","author":"Giunchiglia E.","unstructured":"Giunchiglia , E. , Maratea , M. , and Tacchella , A . 2002. Dependent and independent variables for propositional satisfiability . European Conference on Logic in Artificial Intelligence (JELIA). 296--307 .]] Giunchiglia, E., Maratea, M., and Tacchella, A. 2002. Dependent and independent variables for propositional satisfiability. European Conference on Logic in Artificial Intelligence (JELIA). 296--307.]]"},{"key":"e_1_2_1_72_1","unstructured":"Glover F. and Laguna M. 1995. Tabu search. In Modern Heuristic Techniques for Combinatorial Problems. McGraw-Hill 70--150.]] Glover F. and Laguna M. 1995. Tabu search. In Modern Heuristic Techniques for Combinatorial Problems. McGraw-Hill 70--150.]]"},{"key":"e_1_2_1_73_1","doi-asserted-by":"crossref","unstructured":"Goldberg E. and Novikov Y. 2002. BerkMin: A fast and robust SAT-solver. IEEE\/ACM Design Automation and Test in Europe (DATE). 142--149.]] Goldberg E. and Novikov Y. 2002. BerkMin: A fast and robust SAT-solver. IEEE\/ACM Design Automation and Test in Europe (DATE). 142--149.]]","DOI":"10.1109\/DATE.2002.998262"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/321296.321300"},{"key":"e_1_2_1_75_1","volume-title":"North American National Conference on Artificial Intelligence (AAAI). 431--437","author":"Gomes C. P.","unstructured":"Gomes , C. P. , Selman , B. , and Kautz , H. A . 1998. Boosting combinatorial search through randomization . North American National Conference on Artificial Intelligence (AAAI). 431--437 .]] Gomes, C. P., Selman, B., and Kautz, H. A. 1998. Boosting combinatorial search through randomization. North American National Conference on Artificial Intelligence (AAAI). 431--437.]]"},{"key":"e_1_2_1_76_1","volume-title":"International Joint Conference on Artificial Intelligence (IJCAI). 72--77","author":"Graf T.","unstructured":"Graf , T. , Hentenryck , P. V. , Pradelles , C. , and Zimmer , L . 1989. Simulation of hybrid circuits in constraint logic programming . International Joint Conference on Artificial Intelligence (IJCAI). 72--77 .]] Graf, T., Hentenryck, P. V., Pradelles, C., and Zimmer, L. 1989. Simulation of hybrid circuits in constraint logic programming. International Joint Conference on Artificial Intelligence (IJCAI). 72--77.]]"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1090\/dimacs\/022\/06"},{"key":"e_1_2_1_78_1","doi-asserted-by":"crossref","unstructured":"Gu J. Purdom P. W. Franco J. and Wah B. W. 1997. Algorithms for the satisfiability (SAT) problem: A survey. In Satisfiability Problem: Theory and Applications. DIMACS Series in Discrete Mathematics and Theoretical Computer Science. AMS 19--152.]] Gu J. Purdom P. W. Franco J. and Wah B. W. 1997. Algorithms for the satisfiability (SAT) problem: A survey. In Satisfiability Problem: Theory and Applications. DIMACS Series in Discrete Mathematics and Theoretical Computer Science. AMS 19--152.]]","DOI":"10.1090\/dimacs\/035\/02"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.5555\/647486.726477"},{"key":"e_1_2_1_81_1","volume-title":"Disolver: A distributed constraint solver. Tech. rep. MSR-TR-2003-91, Microsoft Research.]]","author":"Hamadi Y.","year":"2003","unstructured":"Hamadi , Y. 2003 . Disolver: A distributed constraint solver. Tech. rep. MSR-TR-2003-91, Microsoft Research.]] Hamadi, Y. 2003. Disolver: A distributed constraint solver. Tech. rep. MSR-TR-2003-91, Microsoft Research.]]"},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1142\/S021821300500220X"},{"key":"e_1_2_1_83_1","volume-title":"European Conference on Artificial Intelligence (ECAI). 219--223","author":"Hamadi Y.","unstructured":"Hamadi , Y. , Bessi\u00e8re , C. , and Quinqueton , J . 1998. Backtracking in distributed constraint networks . European Conference on Artificial Intelligence (ECAI). 219--223 .]] Hamadi, Y., Bessi\u00e8re, C., and Quinqueton, J. 1998. Backtracking in distributed constraint networks. European Conference on Artificial Intelligence (ECAI). 219--223.]]"},{"key":"e_1_2_1_84_1","doi-asserted-by":"crossref","unstructured":"Hamadi Y. and Merceron D. 1997. Reconfigurable architectures: A new vision for optimization problems. International Conference on Principles and Practice of Constraint Programming (CP). Lecture Notes Computer Science 209--221.]] Hamadi Y. and Merceron D. 1997. Reconfigurable architectures: A new vision for optimization problems. International Conference on Principles and Practice of Constraint Programming (CP). Lecture Notes Computer Science 209--221.]]","DOI":"10.1007\/BFb0017441"},{"key":"e_1_2_1_85_1","unstructured":"Harvey W. D. and Ginsberg M. L. 1995. Limited discrepancy search. J. Artific. Intell. Resear. (JAIR). 607--615.]] Harvey W. D. and Ginsberg M. L. 1995. Limited discrepancy search. J. Artific. Intell. Resear. (JAIR). 607--615.]]"},{"key":"e_1_2_1_86_1","volume-title":"European Conference on Artificial Intelligence (ECAI). 186--190","author":"Hebrard E.","unstructured":"Hebrard , E. , Hnich , B. , and Walsh , T . 2004. Robust solutions for constraint satisfaction and optimization . European Conference on Artificial Intelligence (ECAI). 186--190 .]] Hebrard, E., Hnich, B., and Walsh, T. 2004. Robust solutions for constraint satisfaction and optimization. European Conference on Artificial Intelligence (ECAI). 186--190.]]"},{"key":"e_1_2_1_87_1","volume-title":"International Conference on Principles and Practice of Constraint Programming (CP). 509--523","author":"Henz M.","unstructured":"Henz , M. , Tan , E. , and Yap , R. H. C. 2001. One flip per clock cycle . International Conference on Principles and Practice of Constraint Programming (CP). 509--523 .]] Henz, M., Tan, E., and Yap, R. H. C. 2001. One flip per clock cycle. International Conference on Principles and Practice of Constraint Programming (CP). 509--523.]]"},{"key":"e_1_2_1_88_1","volume-title":"International Conference on Theory and Applications of Satisfiability Testing (SAT). 35--42","author":"Hirsch E. A.","unstructured":"Hirsch , E. A. and Kojevnikov , A . 2001. UnitWalk: A new SAT solver that uses local search guided by unit clause elimination . In International Conference on Theory and Applications of Satisfiability Testing (SAT). 35--42 .]] Hirsch, E. A. and Kojevnikov, A. 2001. UnitWalk: A new SAT solver that uses local search guided by unit clause elimination. In International Conference on Theory and Applications of Satisfiability Testing (SAT). 35--42.]]"},{"key":"e_1_2_1_89_1","volume-title":"Logic-Based Methods for Optimization: Combining Optimization and Constraint Satisfaction","author":"Hooker J.","unstructured":"Hooker , J. 2000. Logic-Based Methods for Optimization: Combining Optimization and Constraint Satisfaction . John Wiley & Sons .]] Hooker, J. 2000. Logic-Based Methods for Optimization: Combining Optimization and Constraint Satisfaction. John Wiley & Sons.]]"},{"key":"e_1_2_1_90_1","volume-title":"North American National Conference on Artificial Intelligence (AAAI). 661--666","author":"Hoos H.","year":"1999","unstructured":"Hoos , H. 1999 . On the run-time behaviour of stochastic local search methods for SAT . North American National Conference on Artificial Intelligence (AAAI). 661--666 .]] Hoos, H. 1999. On the run-time behaviour of stochastic local search methods for SAT. North American National Conference on Artificial Intelligence (AAAI). 661--666.]]"},{"key":"e_1_2_1_91_1","unstructured":"Hoos H. and Stutzle T. 2004. Stochastic Local Search: Foundations and Applications. Morgan Kaufmann.]] Hoos H. and Stutzle T. 2004. Stochastic Local Search: Foundations and Applications. Morgan Kaufmann.]]"},{"key":"e_1_2_1_92_1","doi-asserted-by":"publisher","DOI":"10.1137\/0202019"},{"key":"e_1_2_1_93_1","unstructured":"Hutter F. and Hamadi Y. 2005. Adjustment based on performance prediction: Towards an instance-aware problem solver. Tech. rep. MSR-TR-2005-125 Microsoft Research.]] Hutter F. and Hamadi Y. 2005. Adjustment based on performance prediction: Towards an instance-aware problem solver. Tech. rep. MSR-TR-2005-125 Microsoft Research.]]"},{"key":"e_1_2_1_94_1","doi-asserted-by":"publisher","DOI":"10.1007\/11889205_17"},{"key":"e_1_2_1_95_1","volume-title":"International Conference on Principles and Practice of Constraint Programming (CP). 233--248","author":"Hutter F.","unstructured":"Hutter , F. , Tompkins , D. A. D. , and Hoos , H. H . 2002. Scaling and probabilistic smoothing: Efficient dynamic local search fot SAT . International Conference on Principles and Practice of Constraint Programming (CP). 233--248 .]] Hutter, F., Tompkins, D. A. D., and Hoos, H. H. 2002. Scaling and probabilistic smoothing: Efficient dynamic local search fot SAT. International Conference on Principles and Practice of Constraint Programming (CP). 233--248.]]"},{"key":"e_1_2_1_96_1","volume-title":"International Joint Conference on Artificial Intelligence (IJCAI). 1193--1198","author":"Hyv\u00f6nen E.","year":"1989","unstructured":"Hyv\u00f6nen , E. 1989 . Constraint reasoning based on interval arithmetic . International Joint Conference on Artificial Intelligence (IJCAI). 1193--1198 .]] Hyv\u00f6nen, E. 1989. Constraint reasoning based on interval arithmetic. International Joint Conference on Artificial Intelligence (IJCAI). 1193--1198.]]"},{"key":"e_1_2_1_97_1","doi-asserted-by":"publisher","DOI":"10.1145\/41625.41635"},{"key":"e_1_2_1_98_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01531077"},{"key":"e_1_2_1_99_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(90)90009-O"},{"key":"e_1_2_1_100_1","volume-title":"North American National Conference on Artificial Intelligence (AAAI). 390--396","author":"Katsirelos G.","unstructured":"Katsirelos , G. and Bacchus , F . 2005. Generalized nogood in CSPs . North American National Conference on Artificial Intelligence (AAAI). 390--396 .]] Katsirelos, G. and Bacchus, F. 2005. Generalized nogood in CSPs. North American National Conference on Artificial Intelligence (AAAI). 390--396.]]"},{"key":"e_1_2_1_101_1","volume-title":"North American National Conference on Artificial Intelligence (AAAI). 674--681","author":"Kautz H.","unstructured":"Kautz , H. , Horvitz , E. , Ruan , Y. , Gomes , C. , and Selman , B . 2002. Dynamic restart policies . North American National Conference on Artificial Intelligence (AAAI). 674--681 .]] Kautz, H., Horvitz, E., Ruan, Y., Gomes, C., and Selman, B. 2002. Dynamic restart policies. North American National Conference on Artificial Intelligence (AAAI). 674--681.]]"},{"key":"e_1_2_1_102_1","volume-title":"European Conference on Artificial Intelligence (ECAI). 359--363","author":"Kautz H. A.","unstructured":"Kautz , H. A. and Selman , B . 1992. Planning as satisfiability . European Conference on Artificial Intelligence (ECAI). 359--363 .]] Kautz, H. A. and Selman, B. 1992. Planning as satisfiability. European Conference on Artificial Intelligence (ECAI). 359--363.]]"},{"key":"e_1_2_1_103_1","doi-asserted-by":"publisher","DOI":"10.1126\/science.220.4598.671"},{"key":"e_1_2_1_104_1","doi-asserted-by":"publisher","DOI":"10.1109\/43.310903"},{"key":"e_1_2_1_105_1","doi-asserted-by":"publisher","DOI":"10.1109\/43.108614"},{"key":"e_1_2_1_106_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(78)90029-2"},{"key":"e_1_2_1_107_1","volume-title":"International Conference on Principles and Practice of Constraint Programming (CP). 556--572","author":"Leyton-Brown K.","unstructured":"Leyton-Brown , K. , Nudelman , E. , and Shoham , Y . 2002. Learning the empirical hardness of optimization problems: The case of combinatorial auctions . International Conference on Principles and Practice of Constraint Programming (CP). 556--572 .]] Leyton-Brown, K., Nudelman, E., and Shoham, Y. 2002. Learning the empirical hardness of optimization problems: The case of combinatorial auctions. International Conference on Principles and Practice of Constraint Programming (CP). 556--572.]]"},{"key":"e_1_2_1_108_1","volume-title":"International Joint Conference on Artificial Intelligence (IJCAI). 232--238","author":"Lhomme O.","year":"1993","unstructured":"Lhomme , O. 1993 . Consistency techniques for numeric CSPs . International Joint Conference on Artificial Intelligence (IJCAI). 232--238 .]] Lhomme, O. 1993. Consistency techniques for numeric CSPs. International Joint Conference on Artificial Intelligence (IJCAI). 232--238.]]"},{"key":"e_1_2_1_109_1","volume-title":"North American National Conference on Artificial Intelligence (AAAI). 291--296","author":"Li C.-M.","year":"2000","unstructured":"Li , C.-M. 2000 . Integrating equivalency reasoning into Davis-Putnam procedure . North American National Conference on Artificial Intelligence (AAAI). 291--296 .]] Li, C.-M. 2000. Integrating equivalency reasoning into Davis-Putnam procedure. North American National Conference on Artificial Intelligence (AAAI). 291--296.]]"},{"key":"e_1_2_1_110_1","volume-title":"International Joint Conference on Artificial Intelligence (IJCAI). 245--250","author":"L\u00f3pez-Ortiz A.","year":"2003","unstructured":"L\u00f3pez-Ortiz , A. , Quimper , C.-G. , Tromp , J. , and van Beek , P. 2003 . A fast and simple algorithm for bounds consistency of the alldifferent constraint . International Joint Conference on Artificial Intelligence (IJCAI). 245--250 .]] L\u00f3pez-Ortiz, A., Quimper, C.-G., Tromp, J., and van Beek, P. 2003. A fast and simple algorithm for bounds consistency of the alldifferent constraint. International Joint Conference on Artificial Intelligence (IJCAI). 245--250.]]"},{"key":"e_1_2_1_111_1","volume-title":"-Y","author":"Lu F.","year":"2003","unstructured":"Lu , F. , Wang , L.-C. , Cheng , K.-T. , and Huang , R. C . -Y . 2003 . A circuit SAT solver with signal correlation guided learning. IEEE\/ACM Design, Automation and Test in Europe (DATE) . 10892--10897.]] Lu, F., Wang, L.-C., Cheng, K.-T., and Huang, R. C.-Y. 2003. A circuit SAT solver with signal correlation guided learning. IEEE\/ACM Design, Automation and Test in Europe (DATE). 10892--10897.]]"},{"key":"e_1_2_1_112_1","volume-title":"International Workshop on Constraint Solving and Constraint Logic Programming (CSCLP). 144--158","author":"Lynce I.","unstructured":"Lynce , I. and Marques-Silva , J . 2002. The effect of nogood recording in DPLL-CBJ SAT algorithms . International Workshop on Constraint Solving and Constraint Logic Programming (CSCLP). 144--158 .]] Lynce, I. and Marques-Silva, J. 2002. The effect of nogood recording in DPLL-CBJ SAT algorithms. International Workshop on Constraint Solving and Constraint Logic Programming (CSCLP). 144--158.]]"},{"key":"e_1_2_1_113_1","volume-title":"International Conference on Theory and Applications of Satisfiability Testing (SAT). 305--310","author":"Lynce I.","unstructured":"Lynce , I. and Marques-Silva , J . 2004. On computing minimum unsatisfiable cores . International Conference on Theory and Applications of Satisfiability Testing (SAT). 305--310 .]] Lynce, I. and Marques-Silva, J. 2004. On computing minimum unsatisfiable cores. International Conference on Theory and Applications of Satisfiability Testing (SAT). 305--310.]]"},{"key":"e_1_2_1_114_1","volume-title":"North American National Conference on Artificial Intelligence (AAAI). 1109--1116","author":"Mac Allester D. A.","year":"1990","unstructured":"Mac Allester , D. A. 1990 . Truth maintenance . North American National Conference on Artificial Intelligence (AAAI). 1109--1116 .]] Mac Allester, D. A. 1990. Truth maintenance. North American National Conference on Artificial Intelligence (AAAI). 1109--1116.]]"},{"key":"e_1_2_1_115_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(77)90007-8"},{"key":"e_1_2_1_116_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(85)90041-4"},{"key":"e_1_2_1_117_1","volume-title":"International Workshop on Logic Synthesis.]]","author":"Manquinho V. M.","unstructured":"Manquinho , V. M. amd Marques-Silva , J. P. , Oliveira ., A. L., and Sakallah , K. A . 1998. Satisfiability-based algorithms for 0-1 integer programming . International Workshop on Logic Synthesis.]] Manquinho, V. M. amd Marques-Silva, J. P., Oliveira., A. L., and Sakallah, K. A. 1998. Satisfiability-based algorithms for 0-1 integer programming. International Workshop on Logic Synthesis.]]"},{"key":"e_1_2_1_118_1","doi-asserted-by":"publisher","DOI":"10.1007\/11499107_14"},{"key":"e_1_2_1_119_1","doi-asserted-by":"publisher","DOI":"10.5555\/645377.651196"},{"key":"e_1_2_1_120_1","doi-asserted-by":"publisher","DOI":"10.5555\/647487.726661"},{"key":"e_1_2_1_121_1","doi-asserted-by":"publisher","DOI":"10.1145\/307418.307477"},{"key":"e_1_2_1_122_1","volume-title":"International Conference on Computer Aided Design (ICCAD). 220--227","author":"Marques-Silva J. P.","unstructured":"Marques-Silva , J. P. and Sakallah , K. A . 1996. GRASP - A new search algorithm for satisfiability . International Conference on Computer Aided Design (ICCAD). 220--227 .]] Marques-Silva, J. P. and Sakallah, K. A. 1996. GRASP - A new search algorithm for satisfiability. International Conference on Computer Aided Design (ICCAD). 220--227.]]"},{"key":"e_1_2_1_123_1","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/5625.003.0004"},{"key":"e_1_2_1_124_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"e_1_2_1_125_1","volume-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 2--17","author":"McMillan K. L.","unstructured":"McMillan , K. L. and Amla , N . 2003. Automatic abstraction without counterexamples . International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 2--17 .]] McMillan, K. L. and Amla, N. 2003. Automatic abstraction without counterexamples. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 2--17.]]"},{"key":"e_1_2_1_126_1","volume-title":"International Joint Conference on Artificial Intelligence (IJCAI). 1382--1387","author":"Meseguer P.","year":"1997","unstructured":"Meseguer , P. 1997 . Interleaved depth-first search . International Joint Conference on Artificial Intelligence (IJCAI). 1382--1387 .]] Meseguer, P. 1997. Interleaved depth-first search. International Joint Conference on Artificial Intelligence (IJCAI). 1382--1387.]]"},{"key":"e_1_2_1_127_1","volume-title":"European Conference on Artificial Intelligence (ECAI). 239--243","author":"Meseguer P.","unstructured":"Meseguer , P. and Walsh , T . 1998. Interleaved and discrepancy based search . European Conference on Artificial Intelligence (ECAI). 239--243 .]] Meseguer, P. and Walsh, T. 1998. Interleaved and discrepancy based search. European Conference on Artificial Intelligence (ECAI). 239--243.]]"},{"key":"e_1_2_1_128_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevE.66.056126"},{"key":"e_1_2_1_129_1","volume-title":"International Conference on Evolutionary Programming (EP). 135--155","author":"Michalewicz Z.","year":"1995","unstructured":"Michalewicz , Z. 1995 . A survey constraint handling techniques in evolutionary computation methods . International Conference on Evolutionary Programming (EP). 135--155 .]] Michalewicz, Z. 1995. A survey constraint handling techniques in evolutionary computation methods. International Conference on Evolutionary Programming (EP). 135--155.]]"},{"key":"e_1_2_1_130_1","volume-title":"Constraint and Integer Programming: toward a unified methodology","author":"Milano M.","unstructured":"Milano , M. 2004. Constraint and Integer Programming: toward a unified methodology . Kluwer .]] Milano, M. 2004. Constraint and Integer Programming: toward a unified methodology. Kluwer.]]"},{"key":"e_1_2_1_131_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006343127545"},{"key":"e_1_2_1_132_1","volume-title":"North American National Conference on Artificial Intelligence (AAAI). 398--405","author":"Mitchell D. G.","year":"1998","unstructured":"Mitchell , D. G. 1998 . Hard problems for CSP algorithms . In North American National Conference on Artificial Intelligence (AAAI). 398--405 .]] Mitchell, D. G. 1998. Hard problems for CSP algorithms. In North American National Conference on Artificial Intelligence (AAAI). 398--405.]]"},{"key":"e_1_2_1_133_1","first-page":"112","article-title":"A SAT solver primer","volume":"85","author":"Mitchell D. G.","year":"2005","unstructured":"Mitchell , D. G. 2005 . A SAT solver primer . Bull. Euro. Ass. Theoret. Comput. Science 85 , 112 -- 133 .]] Mitchell, D. G. 2005. A SAT solver primer. Bull. Euro. Ass. Theoret. Comput. Science 85, 112--133.]]","journal-title":"Bull. Euro. Ass. Theoret. Comput. Science"},{"key":"e_1_2_1_134_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(86)90083-4"},{"key":"e_1_2_1_135_1","doi-asserted-by":"publisher","DOI":"10.1145\/952532.952606"},{"key":"e_1_2_1_136_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0255(74)90008-5"},{"key":"e_1_2_1_137_1","volume-title":"Interval Analysis","author":"Moore R. E.","unstructured":"Moore , R. E. 1966. Interval Analysis . Prentice-Hall .]] Moore, R. E. 1966. Interval Analysis. Prentice-Hall.]]"},{"key":"e_1_2_1_138_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_2_1_139_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2004.1"},{"key":"e_1_2_1_140_1","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"e_1_2_1_141_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_33"},{"key":"e_1_2_1_142_1","doi-asserted-by":"publisher","DOI":"10.1145\/996566.996710"},{"key":"e_1_2_1_143_1","doi-asserted-by":"publisher","DOI":"10.1145\/996566.996710"},{"key":"e_1_2_1_144_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1009694016861"},{"key":"e_1_2_1_145_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0183-4"},{"key":"e_1_2_1_146_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1467-8640.1993.tb00310.x"},{"key":"e_1_2_1_147_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6377(88)90067-3"},{"key":"e_1_2_1_148_1","unstructured":"Puget J.-F. 1994. A C&plus;&plus; implementation of CLP. Tech. rep. ILOG inc. ILOG Solver Collected Papers.]] Puget J.-F. 1994. A C&plus;&plus; implementation of CLP. Tech. rep. ILOG inc. ILOG Solver Collected Papers.]]"},{"key":"e_1_2_1_149_1","volume-title":"International Conference on Principles and Practice of Constraint Programming (CP). invited talk.]]","author":"Puget J. F.","year":"2004","unstructured":"Puget , J. F. 2004 . CP's next challenge: simplicity of use . International Conference on Principles and Practice of Constraint Programming (CP). invited talk.]] Puget, J. F. 2004. CP's next challenge: simplicity of use. International Conference on Principles and Practice of Constraint Programming (CP). invited talk.]]"},{"key":"e_1_2_1_150_1","volume-title":"International Workshop on Pragmatics of Decision Procedures in Automated Reasoning.]]","author":"Ranise S.","unstructured":"Ranise , S. and Tinelli , C . 2003. The SMT-LIB format: An initial proposal . International Workshop on Pragmatics of Decision Procedures in Automated Reasoning.]] Ranise, S. and Tinelli, C. 2003. The SMT-LIB format: An initial proposal. International Workshop on Pragmatics of Decision Procedures in Automated Reasoning.]]"},{"key":"e_1_2_1_151_1","doi-asserted-by":"publisher","DOI":"10.1109\/71.219757"},{"key":"e_1_2_1_152_1","volume-title":"North American National Conference on Artificial Intelligence (AAAI). 362--367","author":"R\u00e9gin J.-C.","year":"1994","unstructured":"R\u00e9gin , J.-C. 1994 . A filtering algorithm for constraints of difference in CSPs . North American National Conference on Artificial Intelligence (AAAI). 362--367 .]] R\u00e9gin, J.-C. 1994. A filtering algorithm for constraints of difference in CSPs. North American National Conference on Artificial Intelligence (AAAI). 362--367.]]"},{"key":"e_1_2_1_153_1","volume-title":"North American National Conference on Artificial Intelligence (AAAI). 209--215","author":"R\u00e9gin J.-C.","year":"1996","unstructured":"R\u00e9gin , J.-C. 1996 . Generalized arc consistency for global cardinality constraint . North American National Conference on Artificial Intelligence (AAAI). 209--215 .]] R\u00e9gin, J.-C. 1996. Generalized arc consistency for global cardinality constraint. North American National Conference on Artificial Intelligence (AAAI). 209--215.]]"},{"key":"e_1_2_1_154_1","volume-title":"International Conference on Principles and Practice of Constraint Programming (CP). 549--562","author":"Ringwelski G.","unstructured":"Ringwelski , G. and Hamadi , Y . 2005. Boosting distributed constraint satisfaction . International Conference on Principles and Practice of Constraint Programming (CP). 549--562 .]] Ringwelski, G. and Hamadi, Y. 2005. Boosting distributed constraint satisfaction. International Conference on Principles and Practice of Constraint Programming (CP). 549--562.]]"},{"key":"e_1_2_1_155_1","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"e_1_2_1_156_1","volume-title":"Efficient algorithms for clause learning SAT solvers. Tech. rep","author":"Ryan L.","unstructured":"Ryan , L. 2004. Efficient algorithms for clause learning SAT solvers. Tech. rep ., Simon Fraser University .]] Ryan, L. 2004. Efficient algorithms for clause learning SAT solvers. Tech. rep., Simon Fraser University.]]"},{"key":"e_1_2_1_157_1","volume-title":"North American National Conference on Artificial Intelligence (AAAI). 467--474","author":"Sabharwal A.","year":"2005","unstructured":"Sabharwal , A. 2005 . Symchaff: A structure-aware satisfiability solver . North American National Conference on Artificial Intelligence (AAAI). 467--474 .]] Sabharwal, A. 2005. Symchaff: A structure-aware satisfiability solver. North American National Conference on Artificial Intelligence (AAAI). 467--474.]]"},{"key":"e_1_2_1_158_1","volume-title":"European Conference on Artificial Intelligence (ECAI). 125--129","author":"Sabin D.","unstructured":"Sabin , D. and Freuder , E . 1994. Contradicting conventional wisdom in constraint satisfaction . European Conference on Artificial Intelligence (ECAI). 125--129 .]] Sabin, D. and Freuder, E. 1994. Contradicting conventional wisdom in constraint satisfaction. European Conference on Artificial Intelligence (ECAI). 125--129.]]"},{"key":"e_1_2_1_159_1","volume-title":"North American National Conference on Artificial Intelligence (AAAI). 337--343","author":"Selman B.","unstructured":"Selman , B. , Kautz , H. , and Cohen , B . 1994. Noise strategies for improving local search . In North American National Conference on Artificial Intelligence (AAAI). 337--343 .]] Selman, B., Kautz, H., and Cohen, B. 1994. Noise strategies for improving local search. In North American National Conference on Artificial Intelligence (AAAI). 337--343.]]"},{"key":"e_1_2_1_160_1","volume-title":"North American National Conference on Artificial Intelligence (AAAI). 440--446","author":"Selman B.","unstructured":"Selman , B. , Levesque , H. J. and Mitchell , D. G . 1992. A new method for solving hard satisfiability problems . North American National Conference on Artificial Intelligence (AAAI). 440--446 .]] Selman, B., Levesque, H. J. and Mitchell, D. G. 1992. A new method for solving hard satisfiability problems. North American National Conference on Artificial Intelligence (AAAI). 440--446.]]"},{"key":"e_1_2_1_161_1","volume-title":"IEEE International Symposium Logic in Computer Science (LICS). 100--109","author":"Seshia S. A.","unstructured":"Seshia , S. A. and Bryant , R. E . 2004. Deciding quantifier-free presburger formulas using parameterized solution bounds . In IEEE International Symposium Logic in Computer Science (LICS). 100--109 .]] Seshia, S. A. and Bryant, R. E. 2004. Deciding quantifier-free presburger formulas using parameterized solution bounds. In IEEE International Symposium Logic in Computer Science (LICS). 100--109.]]"},{"key":"e_1_2_1_162_1","doi-asserted-by":"publisher","DOI":"10.1145\/775832.775945"},{"key":"e_1_2_1_163_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008725524946"},{"key":"e_1_2_1_164_1","doi-asserted-by":"publisher","DOI":"10.1007\/11493853_24"},{"key":"e_1_2_1_165_1","volume-title":"IEEE\/ACM International Conference on Automated Software Engineering (ASE). 94--105","author":"Shlyakhter I.","unstructured":"Shlyakhter , I. , Seater , R. , Jackson , D. , Sridharan , M. , and Taghdiri , M . 2003. Debugging overconstrained declarative models using unsatisfiable cores . IEEE\/ACM International Conference on Automated Software Engineering (ASE). 94--105 .]] Shlyakhter, I., Seater, R., Jackson, D., Sridharan, M., and Taghdiri, M. 2003. Debugging overconstrained declarative models using unsatisfiable cores. IEEE\/ACM International Conference on Automated Software Engineering (ASE). 94--105.]]"},{"key":"e_1_2_1_166_1","doi-asserted-by":"publisher","DOI":"10.1145\/2422.322411"},{"key":"e_1_2_1_167_1","volume-title":"German Workshop on Artificial Intelligence, (GWAI). 139--148","author":"Simonis H.","unstructured":"Simonis , H. and Dincbas , M . 1987. Using logic programming for fault diagnosis in digital circuits . German Workshop on Artificial Intelligence, (GWAI). 139--148 .]] Simonis, H. and Dincbas, M. 1987. Using logic programming for fault diagnosis in digital circuits. German Workshop on Artificial Intelligence, (GWAI). 139--148.]]"},{"key":"e_1_2_1_168_1","doi-asserted-by":"crossref","unstructured":"Sinz C. Blochinger W. and K\u00fcchlin W. 2001. PaSAT---parallel SAT-checking with lemma exchange: Implementation and applications. Elec. Notes in Discrete Math. 9.]] Sinz C. Blochinger W. and K\u00fcchlin W. 2001. PaSAT---parallel SAT-checking with lemma exchange: Implementation and applications. Elec. Notes in Discrete Math. 9.]]","DOI":"10.1016\/S1571-0653(04)00323-3"},{"key":"e_1_2_1_169_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2004.102"},{"key":"e_1_2_1_170_1","volume-title":"International Workshop on Constraint Solving and Constraint Logic Programming (CSCLP). invited talk.]]","author":"Smith B.","year":"2002","unstructured":"Smith , B. 2002 . Solve your problem faster---by changing the model . International Workshop on Constraint Solving and Constraint Logic Programming (CSCLP). invited talk.]] Smith, B. 2002. Solve your problem faster---by changing the model. International Workshop on Constraint Solving and Constraint Logic Programming (CSCLP). invited talk.]]"},{"key":"e_1_2_1_171_1","doi-asserted-by":"crossref","unstructured":"Stallman R. M. and Sussman G. J. 1977. Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis. Artific. Intell. 9 135 135--196.]] Stallman R. M. and Sussman G. J. 1977. Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis. Artific. Intell. 9 135 135--196.]]","DOI":"10.1016\/0004-3702(77)90029-7"},{"key":"e_1_2_1_172_1","volume-title":"International Conference on Computer-Aided Verification (CAV). 480--494","author":"Strichman O.","year":"1999","unstructured":"Strichman , O. 1999 . Tuning SAT checkers for bounded model checking . International Conference on Computer-Aided Verification (CAV). 480--494 .]] Strichman, O. 1999. Tuning SAT checkers for bounded model checking. International Conference on Computer-Aided Verification (CAV). 480--494.]]"},{"key":"e_1_2_1_173_1","volume-title":"International Conference on Computer-Aided Verification (CAV). 209--222","author":"Strichman O.","unstructured":"Strichman , O. , Seshia , S. A. , and Bryant , R. E . 2002. Deciding separation formulas with SAT . International Conference on Computer-Aided Verification (CAV). 209--222 .]] Strichman, O., Seshia, S. A., and Bryant, R. E. 2002. Deciding separation formulas with SAT. International Conference on Computer-Aided Verification (CAV). 209--222.]]"},{"key":"e_1_2_1_174_1","volume-title":"International Conference on Theory and Applications of Satisfiability Testing (SAT). 351--356","author":"Subbarayan S.","unstructured":"Subbarayan , S. and Pradhan , D. K . 2004. NiVER: Non increasing variable elimination resolution for preprocessing SAT instances . International Conference on Theory and Applications of Satisfiability Testing (SAT). 351--356 .]] Subbarayan, S. and Pradhan, D. K. 2004. NiVER: Non increasing variable elimination resolution for preprocessing SAT instances. International Conference on Theory and Applications of Satisfiability Testing (SAT). 351--356.]]"},{"key":"e_1_2_1_175_1","volume-title":"National Conference on Artificial Intelligence","author":"Swain M. J.","unstructured":"Swain , M. J. and Cooper , P. R . 1988. Parallel hardware for constraint satisfaction . National Conference on Artificial Intelligence . Los Altos, CA, 682--686.]] Swain, M. J. and Cooper, P. R. 1988. Parallel hardware for constraint satisfaction. National Conference on Artificial Intelligence. Los Altos, CA, 682--686.]]"},{"key":"e_1_2_1_176_1","volume-title":"International Conference on Principles and Practice of Constraint Programming (CP). 663--678","author":"Thiffault C.","unstructured":"Thiffault , C. , Bacchus , F. , and Walsh , T . 2004. Solving non-clausal formulas with DPLL search . International Conference on Principles and Practice of Constraint Programming (CP). 663--678 .]] Thiffault, C., Bacchus, F., and Walsh, T. 2004. Solving non-clausal formulas with DPLL search. International Conference on Principles and Practice of Constraint Programming (CP). 663--678.]]"},{"key":"e_1_2_1_177_1","doi-asserted-by":"crossref","unstructured":"Tseitin G. 1968. On the complexity of derivation in propositional calculus. Studies in Constructive Mathematics and Mathematical Logic part 2 115--125.]] Tseitin G. 1968. On the complexity of derivation in propositional calculus. Studies in Constructive Mathematics and Mathematical Logic part 2 115--125.]]","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"e_1_2_1_178_1","doi-asserted-by":"crossref","unstructured":"Van Gelder A. and Tsuji Y. K. 1996. Satisfiability testing with more reasoning and less guessing. Cliques Coloring and Satisfiability: Second DIMACS Implementation Challenge. AMS 559--586.]] Van Gelder A. and Tsuji Y. K. 1996. Satisfiability testing with more reasoning and less guessing. Cliques Coloring and Satisfiability: Second DIMACS Implementation Challenge. AMS 559--586.]]","DOI":"10.1090\/dimacs\/026\/27"},{"key":"e_1_2_1_179_1","volume-title":"Constraint Satisfaction in Logic Programming","author":"Van Hentenryck P.","unstructured":"Van Hentenryck , P. 1989. Constraint Satisfaction in Logic Programming . MIT Press .]] Van Hentenryck, P. 1989. Constraint Satisfaction in Logic Programming. MIT Press.]]"},{"key":"e_1_2_1_180_1","volume-title":"International Conference on Logic Programming (ICLP). 745--759","author":"Van Hentenryck P.","unstructured":"Van Hentenryck , P. and Deville , Y . 1991. The cardinality operator: A new logical connective for Constraint Logic Programming . International Conference on Logic Programming (ICLP). 745--759 .]] Van Hentenryck, P. and Deville, Y. 1991. The cardinality operator: A new logical connective for Constraint Logic Programming. International Conference on Logic Programming (ICLP). 745--759.]]"},{"key":"e_1_2_1_181_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(92)90020-X"},{"key":"e_1_2_1_182_1","doi-asserted-by":"publisher","DOI":"10.1145\/582419.582430"},{"key":"e_1_2_1_183_1","unstructured":"Van Hentenryck P. and Michel L. 2005. Constraint-Based Local Search. MIT Press.]] Van Hentenryck P. and Michel L. 2005. Constraint-Based Local Search. MIT Press.]]"},{"key":"e_1_2_1_184_1","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/5073.001.0001"},{"key":"e_1_2_1_185_1","doi-asserted-by":"publisher","DOI":"10.1145\/359496.359529"},{"key":"e_1_2_1_186_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(98)10006-7"},{"key":"e_1_2_1_187_1","volume-title":"Exploiting signal unobservability for efficient translation to CNF in formal verification of microprocessors","author":"Velev M.","unstructured":"Velev , M. 2004. Exploiting signal unobservability for efficient translation to CNF in formal verification of microprocessors . IEEE\/ACM Design, Automation and Test in Europe (DATE) . 266--217.]] Velev, M. 2004. Exploiting signal unobservability for efficient translation to CNF in formal verification of microprocessors. IEEE\/ACM Design, Automation and Test in Europe (DATE). 266--217.]]"},{"key":"e_1_2_1_188_1","volume-title":"North American National Conference on Artificial Intelligence (AAAI). 181--187","author":"Verfaillie G.","unstructured":"Verfaillie , G. , Lema\u00eetre , M. , and Schiex , T . 1996. Russian Doll Search for solving constraint optimization problems . North American National Conference on Artificial Intelligence (AAAI). 181--187 .]] Verfaillie, G., Lema\u00eetre, M., and Schiex, T. 1996. Russian Doll Search for solving constraint optimization problems. North American National Conference on Artificial Intelligence (AAAI). 181--187.]]"},{"key":"e_1_2_1_189_1","volume-title":"International Joint Conference on Artificial Intelligence (IJCAI). 1388--1395","author":"Walsh T.","year":"1997","unstructured":"Walsh , T. 1997 . Depth-bounded discrepancy search . In International Joint Conference on Artificial Intelligence (IJCAI). 1388--1395 .]] Walsh, T. 1997. Depth-bounded discrepancy search. In International Joint Conference on Artificial Intelligence (IJCAI). 1388--1395.]]"},{"key":"e_1_2_1_190_1","doi-asserted-by":"publisher","DOI":"10.5555\/647487.726638"},{"key":"e_1_2_1_191_1","volume-title":"Generating semantic descriptions from drawings of scenes with shadows. The Psychology of Computer Vision","author":"Waltz D. L.","year":"1972","unstructured":"Waltz , D. L. 1975. Generating semantic descriptions from drawings of scenes with shadows. The Psychology of Computer Vision . McGraw-Hill , Chapter 3. (Preliminary version as MIT research report (MAC-AI-TR-271), 1972 .)]] Waltz, D. L. 1975. Generating semantic descriptions from drawings of scenes with shadows. The Psychology of Computer Vision. McGraw-Hill, Chapter 3. (Preliminary version as MIT research report (MAC-AI-TR-271), 1972.)]]"},{"key":"e_1_2_1_192_1","volume-title":"Integer Programming","author":"Wolsey L.","unstructured":"Wolsey , L. 1998. Integer Programming . Wiley Interscience .]] Wolsey, L. 1998. Integer Programming. Wiley Interscience.]]"},{"key":"e_1_2_1_193_1","unstructured":"Xilinx-Inc. 1991. The Programmable Gate Array Data Book. Product Briefs.]] Xilinx-Inc. 1991. The Programmable Gate Array Data Book. Product Briefs.]]"},{"key":"e_1_2_1_194_1","volume-title":"International Workshop on Distributed Artificial Intelligence.]]","author":"Yokoo M.","unstructured":"Yokoo , M. , Ishida , T. , and Kubawara , K . 1990. Distributed constraint satisfaction for DAI problems . International Workshop on Distributed Artificial Intelligence.]] Yokoo, M., Ishida, T., and Kubawara, K. 1990. Distributed constraint satisfaction for DAI problems. International Workshop on Distributed Artificial Intelligence.]]"},{"key":"e_1_2_1_195_1","volume-title":"International Conference on Principles and Practice of Constraint Programming (CP). 497--509","author":"Yokoo M.","unstructured":"Yokoo , M. , Suyama , T. , and Sawada , H . 1996. Solving satisfiability problems using field programmable gate arrays: First results . International Conference on Principles and Practice of Constraint Programming (CP). 497--509 .]] Yokoo, M., Suyama, T., and Sawada, H. 1996. Solving satisfiability problems using field programmable gate arrays: First results. International Conference on Principles and Practice of Constraint Programming (CP). 497--509.]]"},{"key":"e_1_2_1_196_1","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.1996.0030"},{"key":"e_1_2_1_197_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006351428454"},{"key":"e_1_2_1_198_1","volume-title":"International Conference on Theory and Applications of Satisfiability Testing (SAT). 287--298","author":"Zhang L.","unstructured":"Zhang , L. and Malik , S . 2003a. Cache performance of SAT solvers: A case study for efficient implementation of algorithms . International Conference on Theory and Applications of Satisfiability Testing (SAT). 287--298 .]] Zhang, L. and Malik, S. 2003a. Cache performance of SAT solvers: A case study for efficient implementation of algorithms. International Conference on Theory and Applications of Satisfiability Testing (SAT). 287--298.]]"},{"key":"e_1_2_1_199_1","unstructured":"Zhang L. and Malik S. 2003b. Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. IEEE\/ACM Design Automation and Test in Europe (DATE). 10880--10885.]] Zhang L. and Malik S. 2003b. Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. IEEE\/ACM Design Automation and Test in Europe (DATE). 10880--10885.]]"},{"key":"e_1_2_1_200_1","volume-title":"International Conference on Computer Aided Design (ICCAD). 279--285","author":"Zhang L.","unstructured":"Zhang , L. , Moskewicz , M. W. , Madigan , C. F. , and Malik , S . 2001. Efficient conflict driven learning in a Boolean satisfiability solver . International Conference on Computer Aided Design (ICCAD). 279--285 .]] Zhang, L., Moskewicz, M. W., Madigan, C. F., and Malik, S. 2001. Efficient conflict driven learning in a Boolean satisfiability solver. International Conference on Computer Aided Design (ICCAD). 279--285.]]"},{"key":"e_1_2_1_201_1","volume-title":"International Workshop on Logic Synthesis.]]","author":"Zhong P.","unstructured":"Zhong , P. , Martonosi , M. , Ashar , P. , and Malik , S . 1997. Implementing Boolean satisfiability in configurable hardware . International Workshop on Logic Synthesis.]] Zhong, P., Martonosi, M., Ashar, P., and Malik, S. 1997. Implementing Boolean satisfiability in configurable hardware. International Workshop on Logic Synthesis.]]"},{"key":"e_1_2_1_202_1","doi-asserted-by":"crossref","unstructured":"Zhong P. Martonosi M. Ashar P. and Malik S. 1998. Solving Boolean satisfiability with dynamic hardware configurations. Field-Programmable Logic and Applications. 326--335.]] Zhong P. Martonosi M. Ashar P. and Malik S. 1998. Solving Boolean satisfiability with dynamic hardware configurations. Field-Programmable Logic and Applications. 326--335.]]","DOI":"10.1007\/BFb0055260"}],"container-title":["ACM Computing Surveys"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1177352.1177354","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1177352.1177354","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T14:51:39Z","timestamp":1750258299000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1177352.1177354"}},"subtitle":["A comparative survey"],"short-title":[],"issued":{"date-parts":[[2006,12,25]]},"references-count":200,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2006,12,25]]}},"alternative-id":["10.1145\/1177352.1177354"],"URL":"https:\/\/doi.org\/10.1145\/1177352.1177354","relation":{},"ISSN":["0360-0300","1557-7341"],"issn-type":[{"value":"0360-0300","type":"print"},{"value":"1557-7341","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,12,25]]},"assertion":[{"value":"2006-12-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}