Take a look at the new version of this page: [ beta version ]. Tell us what you think.

ABSTRACT

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.

REFERENCES

• 1: Miron Abramovici , Jose T. de Sousa , Daniel Saab, A massively-parallel easily-scalable satisfiability solver using reconfigurable hardware, Proceedings of the 36th ACM/IEEE conference on Design automation, p.684-690, June 21-25, 1999, New Orleans, Louisiana, United States [doi>10.1145/309847.310028]
• 2: 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.
• 3: Fadi A. Aloul , Igor L. Markov , Karem A. Sakallah, Shatter: efficient symmetry-breaking for boolean satisfiability, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA [doi>10.1145/775832.776042]
• 4: Krzysztof R. Apt, The essence of constraint propagation, Theoretical Computer Science, v.221 n.1-2, p.179-210, June 28, 1999 [doi>10.1016/S0304-3975(99)00032-8]
• 5: Bacchus, F. and Walsh, T. 2005. Propagating logical combinations of constraints. International Joint. Conference on Artificial Intelligence (IJCAI). 35--40.
• 6: 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.
• 7: Barrett, C., de Moura, L., and Stump, A. 2005. SMT-COMP: Satisfiability modulo theories competition. In International Conference on Computer-Aided Verification (CAV). Springer, 20--23.
• 8: Clark W. Barrett , David L. Dill , Aaron Stump, Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT, Proceedings of the 14th International Conference on Computer Aided Verification, p.236-249, July 27-31, 2002
• 9: Bart, P. 1995. A Davis-Putnam based enumeration algorithm for linear pseudo-Boolean optimization. Tech. rep. 95-2-003, Max Planck Institute.
• 10: 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.
• 11: Beldiceanu, N., Carlsson, M., and Rampon, J.-X. 2005. Global constraint catalog. Tech. rep. T2005-08, Swedish Institute of Computer Science.
• 12: Beldiceanu, N. and Contejean, E. 1994. Introducing global constraints in CHIP. Mathem. Comput. model. 20, 12, 87--123.
• 13: Richard Ernest Bellman, Dynamic Programming, Dover Publications, Incorporated, 2003
• 14: Benhamou, F. and Older, W. J. 1997. Applying interval arithmetic to real, integer, and Boolean constraints. J. Logic Program. 32, 1, 1--24.
• 15: Christian Bessière, Arc-consistency and arc-consistency again, Artificial Intelligence, v.65 n.1, p.179-190, Jan. 1994 [doi>10.1016/0004-3702(94)90041-8]
• 16: Bessière, C., Freuder, E. C., and Régin, J.-C. 1995. Using inference to reduce arc consistency computation. International Joint Conference on Artificial Intelligence (IJCAI). 592--599.
• 17: Bessière, C., Hébrard, E., and Walsh, T. 2003. Local consistencies in SAT. International Conference on Theory and Applications of Satisfiability Testing (SAT). 299--314.
• 18: Bessière, C. and Régin, J.-C. 1996. MAC and combined heuristics: Two reasons to forsake FC (and CBJ?) on hard problems. In International Conference on Principles and Practice of Constraint Programming (CP). 61--75.
• 19: Christian Bessière , Jean-Charles Régin , Roland H. C. Yap , Yuanlin Zhang, An optimal coarse-grained arc consistency algorithm, Artificial Intelligence, v.165 n.2, p.165-185, July 2005 [doi>10.1016/j.artint.2005.02.004]
• 20: Armin Biere , Alessandro Cimatti , Edmund M. Clarke , Yunshan Zhu, Symbolic Model Checking without BDDs, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.193-207, March 22-28, 1999
• 21: S. Bistarelli , U. Montanari , F. Rossi , T. Schiex , G. Verfaillie , H. Fargier, Semiring-Based CSPs and Valued CSPs: Frameworks, Properties,and Comparison, Constraints, v.4 n.3, p.199-240, September 1999 [doi>10.1023/A:1026441215081]
• 22: W. Blochinger , W. Westje , W. Kuchlin , S. Wedeniwski, ZetaSAT - Boolean SATisfiability solving on Desktop Grids, Proceedings of the Fifth IEEE International Symposium on Cluster Computing and the Grid (CCGrid'05) - Volume 2, p.1079-1086, May 09-12, 2005
• 23: Daniel Brélaz, New methods to color the vertices of a graph, Communications of the ACM, v.22 n.4, p.251-256, April 1979 [doi>10.1145/359094.359101]
• 24: Bruynooghe, M. 1981. Solving combinatorial search problems by intelligent backtracking. Inform. Proces. Lett. 12, 1, 36--39.
• 25: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 26: Randal E. Bryant , Shuvendu K. Lahiri , Sanjit A. Seshia, Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions, Proceedings of the 14th International Conference on Computer Aided Verification, p.78-92, July 27-31, 2002
• 27: Jerry R. Burch , David L. Dill, Automatic verification of Pipelined Microprocessor Control, Proceedings of the 6th International Conference on Computer Aided Verification, p.68-80, June 21-23, 1994
• 28: Buro, M. and Büning, H. K. 1993. Report on a SAT competition. Bull. Europ. Assoc. Theoret. Comput. Science 49, 143--151.
• 29: Marco Cadoli , Toni Mancini, Automated reformulation of specifications by safe delay of constraints, Artificial Intelligence, v.170 n.8, p.779-801, June 2006 [doi>10.1016/j.artint.2006.01.008]
• 30: Srimat T. Chakradhar , Vishwani D. Agrawal, A transitive closure based algorithm for test generation, Proceedings of the 28th conference on ACM/IEEE design automation, p.353-358, June 17-22, 1991, San Francisco, California, United States [doi>10.1145/127601.127693]
• 31: Chatalic, P. and Simon, L. 2001. Multiresolution for SAT checking. Int. J. Artific. Intell. Tools 10, 4, 451--481.
• 32: Wahid Chrabakh , Rich Wolski, GridSAT: A Chaff-based Distributed SAT Solver for the Grid, Proceedings of the 2003 ACM/IEEE conference on Supercomputing, p.37, November 15-21, 2003
• 33: Chvatal, V. 1983. Linear Programming. W. H. Freeman Co.
• 34: Edmund Clarke , Armin Biere , Richard Raimi , Yunshan Zhu, Bounded Model Checking Using Satisfiability Solving, Formal Methods in System Design, v.19 n.1, p.7-34, July 2001 [doi>10.1023/A:1011276507260]
• 35: Cleary, J. G. 1987. Logical arithmetic. Future Comput. Syst. 2, 2, 125--149.
• 36: Codognet, P. and Diaz, D. 1996. Compiling constraints in CLP(FD). J. Logic Program. 27, 3, 185--226.
• 37: Collavizza, H. and Rueher, M. 2006. Exploration of the capabilities of constraint programming for software verification. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 182--196.
• 38: Colmerauer, A. 1984. Equations and inequations on finite and infinite tress. International Conference on Fifth Generation Computing. 85--99.
• 39: Alain Colmerauer, An introduction to Prolog III, Communications of the ACM, v.33 n.7, p.69-90, July 1990 [doi>10.1145/79204.79210]
• 40: Patrick Cousot , Radhia Cousot, Automatic synthesis of optimal invariant assertions: Mathematical foundations, Proceedings of the 1977 symposium on Artificial intelligence and programming languages, p.1-12, August 15-17, 1977
• 41: Andreas Dandalis , Viktor K. Prasanna, Run-time performance optimization of an FPGA-based deduction engine for SAT solvers, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.7 n.4, p.547-562, October 2002 [doi>10.1145/605440.605444]
• 42: Evgeny Dantsin , Alexander Wolpert, Solving Constraint Satisfaction Problems with DNA Computing, Proceedings of the 8th Annual International Conference on Computing and Combinatorics, p.171-180, August 15-17, 2002
• 43: Andrew Davenport , Edward Tsang , Chang J. Wang , Kangmin Zhu, GENET: a connectionist architecture for solving constraint satisfaction problems by iterative improvement, Proceedings of the twelfth national conference on Artificial intelligence (vol. 1), p.325-330, October 1994, Seattle, Washington, United States
• 44: Ernest Davis, Constraint propagation with interval labels, Artificial Intelligence, v.32 n.3, p.281-331, July 1987 [doi>10.1016/0004-3702(87)90091-9]
• 45: Martin Davis , George Logemann , Donald Loveland, A machine program for theorem-proving, Communications of the ACM, v.5 n.7, p.394-397, July 1962 [doi>10.1145/368273.368557]
• 46: Martin Davis , Hilary Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM (JACM), v.7 n.3, p.201-215, July 1960 [doi>10.1145/321033.321034]
• 47: Debruyne, R. and Bessière, C. 2001. Domain filtering consistencies. J. Artific. Intell. Resear. 14, 205--230.
• 48: Rina Dechter, Enhancement schemes for constraint processing: backjumping, learning, and cutset decomposition, Artificial Intelligence, v.41 n.3, p.273-312, Jan. 1990 [doi>10.1016/0004-3702(90)90046-3]
• 49: Rina Dechter, Constraint Processing, Morgan Kaufmann Publishers Inc., San Francisco, CA, 2003
• 50: Delzanno, G. and Podelski, A. 2001. Constraint-based deductive model checking. Int. J. Softw. Tools Technol. Transfer 3, 3, 250--270.
• 51: Dershowitz, N., Hanna, Z., and Nadel, A. 2005. A clause-based heuristic for SAT solvers. International Conference on Theory and Applications of Satisfiability Testing (SAT). 46--60.
• 52: Dixon, H. E., Ginsberg, M. L., Luks, E. M., and Parkes, A. J. 2004. Generalizing Boolean satisfiability II: Theory. J. Artific. Intell. Resear. 22, 481--534.
• 53: Marco Dorigo , Thomas Stützle, Ant Colony Optimization, Bradford Book, 2004
• 54: Èen, N. and Biere, A. 2005. Effective preprocessing in SAT through variable and clause elimination. International Conference on Theory and Applications of Satisfiability Testing (SAT). 61--75.
• 55: Fang, H. and Ruml, W. 2004. Complete local search for propositional satisfiability. North American National Conference on Artificial Intelligence (AAAI). 161--166.
• 56: Feldman, Y., Dershowitz, N., and Hanna, Z. 2005. Parallel multithreaded satisfiability solver: Design and implementation. Elec. Notes Theor. Comput. Science 128, 3, 75--90.
• 57: Fikes, R. 1970. REF-ARF: A system for solving problems stated as procedures. Artific. Intell. 1, 1/2, 27--120.
• 58: 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.
• 59: Fourer, R., Gay, D., and Kernighan, B. 1993. AMPL: A Modeling Language for Mathematical Programming. Duxbury Press.
• 60: Jon William Freeman, Improvements to propositional satisfiability search algorithms, University of Pennsylvania, Philadelphia, PA, 1995
• 61: Eugene C. Freuder, Synthesizing constraint expressions, Communications of the ACM, v.21 n.11, p.958-966, Nov. 1978 [doi>10.1145/359642.359654]
• 62: Eugene C. Freuder , Richard J. Wallace, Partial constraint satisfaction, Artificial Intelligence, v.58 n.1-3, p.21-70, Dec. 1992 [doi>10.1016/0004-3702(92)90004-H]
• 63: 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.
• 64: Malay K. Ganai , Pranav Ashar , Aarti Gupta , Lintao Zhang , Sharad Malik, Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT solver, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA [doi>10.1145/513918.514105]
• 65: 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.
• 66: Gaschnig, J. 1979. Performance measurement and analysis of certain search algorithms. Tech. rep. CMU-CS-79-124, Carnegie-Mellon University.
• 67: Richard Génisson , Philippe Jégou, On the relations between SAT and CSP enumerative algorithms, Discrete Applied Mathematics, v.107 n.1-3, p.27-40, Dec. 2000 [doi>10.1016/S0166-218X(99)00205-X]
• 68: Gent, I. P. and Smith, B. M. 2000. Symmetry breaking in constraint programming. In European Conference on Artificial Intelligence (ECAI). 599--603.
• 69: Ginsberg, M. L. 1993. Dynamic backtracking. J. Artific. Intell. Resear. 1, 25--46.
• 70: Matthew L. Ginsberg , Andrew J. Parkes , Amitabha Roy, Supermodels and robustness, Proceedings of the fifteenth national/tenth conference on Artificial intelligence/Innovative applications of artificial intelligence, p.334-339, July 1998, Madison, Wisconsin, United States
• 71: Enrico Giunchiglia , Marco Maratea , Armando Tacchella, Dependent and Independent Variables in Propositional Satisfiability, Proceedings of the European Conference on Logics in Artificial Intelligence, p.296-307, September 23-26, 2002
• 72: Fred Glover , Manuel Laguna, Tabu search, Modern heuristic techniques for combinatorial problems, John Wiley & Sons, Inc., New York, NY, 1993
• 73: E. Goldberg , Y. Novikov, BerkMin: A Fast and Robust Sat-Solver, Proceedings of the conference on Design, automation and test in Europe, p.142, March 04-08, 2002
• 74: Solomon W. Golomb , Leonard D. Baumert, Backtrack Programming, Journal of the ACM (JACM), v.12 n.4, p.516-524, Oct. 1965 [doi>10.1145/321296.321300]
• 75: Carla P. Gomes , Bart Selman , Henry Kautz, Boosting combinatorial search through randomization, Proceedings of the fifteenth national/tenth conference on Artificial intelligence/Innovative applications of artificial intelligence, p.431-437, July 1998, Madison, Wisconsin, United States
• 76: 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.
• 77: Gu, J. 1995. Parallel algorithms for satisfiability (SAT) problem. Parallel Processing of Discrete Optimization Problems. DIMACS, vol. 22. 105--161.
• 78: 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.
• 79: Youssef Hamadi, Optimal Distributed Arc-Consistency, Proceedings of the 5th International Conference on Principles and Practice of Constraint Programming, p.219-233, October 11-14, 1999
• 80: Hamadi, Y. 1999b. Traitement des problèmes de satisfaction de contraintes distribués. Ph.D. thesis, Université Montpellier.
• 81: Hamadi, Y. 2003. Disolver: A distributed constraint solver. Tech. rep. MSR-TR-2003-91, Microsoft Research.
• 82: Hamadi, Y. 2005. Conflicting agents in distributed search. Int. J. Artific. Intell. Tools 14, 3, 459--476.
• 83: Hamadi, Y., Bessière, C., and Quinqueton, J. 1998. Backtracking in distributed constraint networks. European Conference on Artificial Intelligence (ECAI). 219--223.
• 84: 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.
• 85: Harvey, W. D. and Ginsberg, M. L. 1995. Limited discrepancy search. J. Artific. Intell. Resear. (JAIR). 607--615.
• 86: Hebrard, E., Hnich, B., and Walsh, T. 2004. Robust solutions for constraint satisfaction and optimization. European Conference on Artificial Intelligence (ECAI). 186--190.
• 87: Martin Henz , Edgar Tan , Roland H. C. Yap, One Flip per Clock Cycle, Proceedings of the 7th International Conference on Principles and Practice of Constraint Programming, p.509-523, November 26-December 01, 2001
• 88: 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.
• 89: Hooker, J. 2000. Logic-Based Methods for Optimization: Combining Optimization and Constraint Satisfaction. John Wiley & Sons.
• 90: Holger H. Hoos, On the run-time behaviour of stochastic local search algorithms for SAT, Proceedings of the sixteenth national conference on Artificial intelligence and the eleventh Innovative applications of artificial intelligence conference innovative applications of artificial intelligence, p.661-666, July 18-22, 1999, Orlando, Florida, United States
• 91: Holger Hoos , Thomas Sttzle, Stochastic Local Search: Foundations & Applications, Morgan Kaufmann Publishers Inc., San Francisco, CA, 2004
• 92: Hopcroft, J. E. and Karp, R. M. 1973. An n&frac52; algorithm for maximum matchings in bipartite graphs. SIAM J. Comput. 2, 4, 225--231.
• 93: 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.
• 94: Hutter, F., Hamadi, Y., Hoos, H., and Leyton-Brown, K. 2006. Performance prediction and automated tuning of randomized and parametric algorithms. International Conference on Principles and Practice of Constraint Programming (CP). To appear.
• 95: Frank Hutter , Dave A. D. Tompkins , Holger H. Hoos, Scaling and Probabilistic Smoothing: Efficient Dynamic Local Search for SAT, Proceedings of the 8th International Conference on Principles and Practice of Constraint Programming, p.233-248, September 09-13, 2002
• 96: Hyvönen, E. 1989. Constraint reasoning based on interval arithmetic. International Joint Conference on Artificial Intelligence (IJCAI). 1193--1198.
• 97: J. Jaffar , J.-L. Lassez, Constraint logic programming, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.111-119, January 21-23, 1987, Munich, West Germany [doi>10.1145/41625.41635]
• 98: Jeroslow, R. J. and Wang, J. 1990. Solving propositional satisfiability problems. Ann. Mathemat. Artific. Intell. 1, 167--188.
• 99: Simon Kasif, On the parallel complexity of discrete relaxation in constraint satisfaction networks, Artificial Intelligence, v.45 n.3, p.275-286, Oct. 1990 [doi>10.1016/0004-3702(90)90009-O]
• 100: Katsirelos, G. and Bacchus, F. 2005. Generalized nogood in CSPs. North American National Conference on Artificial Intelligence (AAAI). 390--396.
• 101: Henry Kautz , Eric Horvitz , Yongshao Ruan , Carla Gomes , Bart Selman, Dynamic restart policies, Eighteenth national conference on Artificial intelligence, p.674-681, July 28-August 01, 2002, Edmonton, Alberta, Canada
• 102: Henry Kautz , Bart Selman, Planning as satisfiability, Proceedings of the 10th European conference on Artificial intelligence, p.359-363, August 1992, Vienna, Austria
• 103: Kirkpatrick, S., Gelatt, C., and Vecchi, M. 1983. Optimization by simulated annealing. Science 220, 671--680.
• 104: Kunz, W. and Pradhan, D. 1994. Recrusive Learning: A new implication technique for efficient solutions to CAD problems: Test, verification and optimization. IEEE Trans. Comput.-Aided Design 13, 9, 1143--1158.
• 105: Larrabee, T. 1992. Test pattern generation using Boolean satisfiability. IEEE Trans. Comput.-Aided Design 11, 1, 6--22.
• 106: Laurière, J.-L. 1978. A language and a program for stating and solving combinatorial problems. Artific. Intell. 10, 1, 29--127.
• 107: Kevin Leyton-Brown , Eugene Nudelman , Yoav Shoham, Learning the Empirical Hardness of Optimization Problems: The Case of Combinatorial Auctions, Proceedings of the 8th International Conference on Principles and Practice of Constraint Programming, p.556-572, September 09-13, 2002
• 108: Lhomme, O. 1993. Consistency techniques for numeric CSPs. International Joint Conference on Artificial Intelligence (IJCAI). 232--238.
• 109: Chu Min Li, Integrating Equivalency Reasoning into Davis-Putnam Procedure, Proceedings of the Seventeenth National Conference on Artificial Intelligence and Twelfth Conference on Innovative Applications of Artificial Intelligence, p.291-296, July 30-August 03, 2000
• 110: López-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.
• 111: Feng Lu , Li-C. Wang , Kwang-Ting Cheng , Ric C-Y Huang, A Circuit SAT Solver With Signal Correlation Guided Learning, Proceedings of the conference on Design, Automation and Test in Europe, p.10892, March 03-07, 2003
• 112: 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.
• 113: Lynce, I. and Marques-Silva, J. 2004. On computing minimum unsatisfiable cores. International Conference on Theory and Applications of Satisfiability Testing (SAT). 305--310.
• 114: Mac Allester, D. A. 1990. Truth maintenance. North American National Conference on Artificial Intelligence (AAAI). 1109--1116.
• 115: Mackworth, A. 1977. Consistency in networks of relations. Artific. Intell. 8, 99--118.
• 116: Alan K. Mackworth , Eugene C. Freuder, The complexity of some polynomial network consistency algorithms for constraint satisfaction problems, Artificial Intelligence, v.25 n.1, p.65-74, Jan. 1985 [doi>10.1016/0004-3702(85)90041-4]
• 117: 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.
• 118: Marinov, D., Khurshid, S., Bugrara, S., Zhang, L., and Rinard, M. 2005. Optimizations for compiling declarative models into Boolean formulas. International Conference on Theory and Applications of Satisfiability Testing (SAT). 187--202.
• 119: João P. Marques Silva, The Impact of Branching Heuristics in Propositional Satisfiability Algorithms, Proceedings of the 9th Portuguese Conference on Artificial Intelligence: Progress in Artificial Intelligence, p.62-74, September 21-24, 1999
• 120: João P. Marques Silva, Algebraic Simplification Techniques for Propositional Satisfiability, Proceedings of the 6th International Conference on Principles and Practice of Constraint Programming, p.537-542, September 18-21, 2000
• 121: João Marques-Silva , Thomas Glass, Combinational equivalence checking using satisfiability and recursive learning, Proceedings of the conference on Design, automation and test in Europe, p.33-es, January 1999, Munich, Germany [doi>10.1145/307418.307477]
• 122: João P. Marques Silva , Karem A. Sakallah, GRASP—a new search algorithm for satisfiability, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.220-227, November 10-14, 1996, San Jose, California, United States
• 123: Marriott, K. and Stuckey, P. J. 1998. Programming with Constraints: An Introduction. MIT Press.
• 124: McMillan, K. L. 2003. Interpolation and SAT-based model checking. International Conference on Computer-Aided Verification (CAV). 1--13.
• 125: 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.
• 126: Meseguer, P. 1997. Interleaved depth-first search. International Joint Conference on Artificial Intelligence (IJCAI). 1382--1387.
• 127: Meseguer, P. and Walsh, T. 1998. Interleaved and discrepancy based search. European Conference on Artificial Intelligence (ECAI). 239--243.
• 128: Mézard, M. and Zecchina, R. 2002. Random k-satisfiability: from an analytic solution to a new efficient algorithm. Physical Rev. E, 66, 056126.
• 129: Michalewicz, Z. 1995. A survey constraint handling techniques in evolutionary computation methods. International Conference on Evolutionary Programming (EP). 135--155.
• 130: Michela Milano, Constraint and Integer Programming: Toward a Unified Methodology (Operations Research/Computer Science Interfaces", 27), Kluwer Academic Publishers, Norwell, MA, 2003
• 131: Patrick Mills , Edward Tsang, Guided Local Search for Solving SAT and Weighted MAX-SAT Problems, Journal of Automated Reasoning, v.24 n.1-2, p.205-223, February 2000 [doi>10.1023/A:1006343127545]
• 132: David G. Mitchell, Hard problems for CSP Algorithms, Proceedings of the fifteenth national/tenth conference on Artificial intelligence/Innovative applications of artificial intelligence, p.398-405, July 1998, Madison, Wisconsin, United States
• 133: Mitchell, D. G. 2005. A SAT solver primer. Bull. Euro. Ass. Theoret. Comput. Science 85, 112--133.
• 134: Roger Mohr , Thomas C. Henderson, Arc and path consistence revisited, Artificial Intelligence, v.28 n.2, p.225-233, March 1986 [doi>10.1016/0004-3702(86)90083-4]
• 135: Eric Monfroy , Carlos Castro, Basic components for constraint solver cooperations, Proceedings of the 2003 ACM symposium on Applied computing, March 09-12, 2003, Melbourne, Florida [doi>10.1145/952532.952606]
• 136: Montanari, U. 1974. Networks of constraints: Fundamental properties and applications to picture processing. Inform. Science 7, 2, 85--132.
• 137: Moore, R. E. 1966. Interval Analysis. Prentice-Hall.
• 138: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 139: Gi-Joon Nam , Fadi Aloul , Karem A. Sakallah , Rob A. Rutenbar, A Comparative Study of Two Boolean Formulations of FPGA Detailed Routing Constraints, IEEE Transactions on Computers, v.53 n.6, p.688-696, June 2004 [doi>10.1109/TC.2004.1]
• 140: Greg Nelson , Derek C. Oppen, Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.2, p.245-257, Oct. 1979 [doi>10.1145/357073.357079]
• 141: Nieuwenhuis, R. and Oliveras, A. 2005. DPLL(T) with exhaustive theory propagation and its application to difference logic. International Conference on Computer-Aided Verification (CAV). 321--334.
• 142: Yoonna Oh , Maher N. Mneimneh , Zaher S. Andraus , Karem A. Sakallah , Igor L. Markov, AMUSE: a minimally-unsatisfiable subformula extractor, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA [doi>10.1145/996566.996710]
• 143: Yoonna Oh , Maher N. Mneimneh , Zaher S. Andraus , Karem A. Sakallah , Igor L. Markov, AMUSE: a minimally-unsatisfiable subformula extractor, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA [doi>10.1145/996566.996710]
• 144: Gilles Pesant , Michel Gendreau, A Constraint Programming Framework for Local Search Methods, Journal of Heuristics, v.5 n.3, p.255-279, October 1999 [doi>10.1023/A:1009694016861]
• 145: Prasad, M. R., Biere, A., and Gupta, A. 2005. A survey of recent advances in sat-based formal verification. International J. Softw. Tools Technol. Transfer 7, 2, 156--173.
• 146: Prosser, P. 1993. Hybrid algorithms for the constraint satisfaction problem. Computat. Intell. 9, 268--299.
• 147: Pruul, E. A. and Nemhauser, G. L. 1988. Branch-and-bound and parallel computation: A historical note. Operat. Resear. Lett. 7, 2, 65--69.
• 148: Puget, J.-F. 1994. A C++ implementation of CLP. Tech. rep., ILOG, inc. ILOG Solver Collected Papers.
• 149: Jean-Francois Puget, Applications of Constraint Programming, Proceedings of the First International Conference on Principles and Practice of Constraint Programming, p.647-650, September 19-22, 1995
• 150: Ranise, S. and Tinelli, C. 2003. The SMT-LIB format: An initial proposal. International Workshop on Pragmatics of Decision Procedures in Automated Reasoning.
• 151: V. N. Rao , V. Kumar, On the Efficiency of Parallel Backtracking, IEEE Transactions on Parallel and Distributed Systems, v.4 n.4, p.427-437, April 1993 [doi>10.1109/71.219757]
• 152: Jean-Charles Régin, A filtering algorithm for constraints of difference in CSPs, Proceedings of the twelfth national conference on Artificial intelligence (vol. 1), p.362-367, October 1994, Seattle, Washington, United States
• 153: Régin, J.-C. 1996. Generalized arc consistency for global cardinality constraint. North American National Conference on Artificial Intelligence (AAAI). 209--215.
• 154: Ringwelski, G. and Hamadi, Y. 2005. Boosting distributed constraint satisfaction. International Conference on Principles and Practice of Constraint Programming (CP). 549--562.
• 155: J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
• 156: Ryan, L. 2004. Efficient algorithms for clause learning SAT solvers. Tech. rep., Simon Fraser University.
• 157: Sabharwal, A. 2005. Symchaff: A structure-aware satisfiability solver. North American National Conference on Artificial Intelligence (AAAI). 467--474.
• 158: Sabin, D. and Freuder, E. 1994. Contradicting conventional wisdom in constraint satisfaction. European Conference on Artificial Intelligence (ECAI). 125--129.
• 159: Bart Selman , Henry A. Kautz , Bram Cohen, Noise strategies for improving local search, Proceedings of the twelfth national conference on Artificial intelligence (vol. 1), p.337-343, October 1994, Seattle, Washington, United States
• 160: 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.
• 161: Sanjit A. Seshia , Randal E. Bryant, Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04), p.100-109, July 13-17, 2004
• 162: Sanjit A. Seshia , Shuvendu K. Lahiri , Randal E. Bryant, A hybrid SAT-based decision procedure for separation logic with uninterpreted functions, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA [doi>10.1145/775832.775945]
• 163: Mary Sheeran , Gunnar Stålmarck, A Tutorial on Stålmarck‘s Proof Procedure for PropositionalLogic, Formal Methods in System Design, v.16 n.1, p.23-58, Jan 1,2000 [doi>10.1023/A:1008725524946]
• 164: Sheini, H. M. and Sakallah, K. A. 2005. A sat-based decision procedure for mixed logical/integer linear problems. International Conference on Integration of AI and OR Techniques in CP for Combinatorial Optimization Problems (CP-AI-OR). 320--335.
• 165: 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.
• 166: Robert E. Shostak, Deciding Combinations of Theories, Journal of the ACM (JACM), v.31 n.1, p.1-12, Jan. 1984 [doi>10.1145/2422.322411]
• 167: Helmut Simonis , Mehmet Dincbas, Using Logic Programming for Fault Diagnosis in Digital Circuits, Proceedings of the 11th German Workshop on Artificial Intelligence, p.139-148, September 28-October 02, 1987
• 168: Sinz, C., Blochinger, W., and Küchlin, W. 2001. PaSAT---parallel SAT-checking with lemma exchange: Implementation and applications. Elec. Notes in Discrete Math. 9.
• 169: Iouliia Skliarova , Antonio de Brito Ferrari, Reconfigurable Hardware SAT Solvers: A Survey of Systems, IEEE Transactions on Computers, v.53 n.11, p.1449-1461, November 2004 [doi>10.1109/TC.2004.102]
• 170: Smith, B. 2002. Solve your problem faster---by changing the model. International Workshop on Constraint Solving and Constraint Logic Programming (CSCLP). invited talk.
• 171: 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.
• 172: Ofer Shtrichman, Tuning SAT Checkers for Bounded Model Checking, Proceedings of the 12th International Conference on Computer Aided Verification, p.480-494, July 15-19, 2000
• 173: Ofer Strichman , Sanjit A. Seshia , Randal E. Bryant, Deciding Separation Formulas with SAT, Proceedings of the 14th International Conference on Computer Aided Verification, p.209-222, July 27-31, 2002
• 174: 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.
• 175: Swain, M. J. and Cooper, P. R. 1988. Parallel hardware for constraint satisfaction. National Conference on Artificial Intelligence. Los Altos, CA, 682--686.
• 176: 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.
• 177: Tseitin, G. 1968. On the complexity of derivation in propositional calculus. Studies in Constructive Mathematics and Mathematical Logic, part 2, 115--125.
• 178: 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.
• 179: Pascal Van Hentenryck, Constraint satisfaction in logic programming, MIT Press, Cambridge, MA, 1989
• 180: 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.
• 181: Pascal Van Hentenryck , Yves Deville , Choh-Man Teng, A generic arc-consistency algorithm and its specializations, Artificial Intelligence, v.57 n.2-3, p.291-321, Oct. 1992 [doi>10.1016/0004-3702(92)90020-X]
• 182: Laurent Michel , Pascal Van Hentenryck, A constraint-based architecture for local search, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
• 183: Pascal Van Hentenryck , Laurent Michel, Constraint-Based Local Search, The MIT Press, 2005
• 184: Van Hentenryck, P., Michel, L., and Deville, Y. 1997. Numerica: A Modeling Language for Global Optimization. MIT Press.
• 185: Pascal Van Hentenryck , Laurent Perron , Jean-François Puget, Search and strategies in OPL, ACM Transactions on Computational Logic (TOCL), v.1 n.2, p.285-320, Oct. 2000 [doi>10.1145/359496.359529]
• 186: Van Hentenryck, P., Saraswat, V. A., and Deville, Y. 1998. Design, implementation, and evaluation of the constraint language CC(FD). J. Logic Program. 37, 1-3, 139--164.
• 187: Miroslav N. Velev, Exploiting Signal Unobservability for Efficient Translation to CNF in Formal Verification of Microprocessors, Proceedings of the conference on Design, automation and test in Europe, p.10266, February 16-20, 2004
• 188: Verfaillie, G., Lemaître, M., and Schiex, T. 1996. Russian Doll Search for solving constraint optimization problems. North American National Conference on Artificial Intelligence (AAAI). 181--187.
• 189: Walsh, T. 1997. Depth-bounded discrepancy search. In International Joint Conference on Artificial Intelligence (IJCAI). 1388--1395.
• 190: Toby Walsh, SAT v CSP, Proceedings of the 6th International Conference on Principles and Practice of Constraint Programming, p.441-456, September 18-21, 2000
• 191: David L. Waltz, Generating Semantic Descriptions From Drawings of Scenes With Shadows, Massachusetts Institute of Technology, Cambridge, MA, 1972
• 192: Wolsey, L. 1998. Integer Programming. Wiley Interscience.
• 193: Xilinx-Inc. 1991. The Programmable Gate Array Data Book. Product Briefs.
• 194: Yokoo, M., Ishida, T., and Kubawara, K. 1990. Distributed constraint satisfaction for DAI problems. International Workshop on Distributed Artificial Intelligence.
• 195: 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.
• 196: Hantao Zhang , Maria Paola Bonacina , Jieh Hsiang, PSATO: a distributed propositional prover and its application to quasigroup problems, Journal of Symbolic Computation, v.21 n.4-6, p.543-560, April/May/June 1996 [doi>10.1006/jsco.1996.0030]
• 197: Hantao Zhang , Mark Stickel, Implementing the Davis–Putnam Method, Journal of Automated Reasoning, v.24 n.1-2, p.277-296, February 2000 [doi>10.1023/A:1006351428454]
• 198: 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.
• 199: Lintao Zhang , Sharad Malik, Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications, Proceedings of the conference on Design, Automation and Test in Europe, p.10880, March 03-07, 2003
• 200: Lintao Zhang , Conor F. Madigan , Matthew H. Moskewicz , Sharad Malik, Efficient conflict driven learning in a boolean satisfiability solver, Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, November 04-08, 2001, San Jose, California
• 201: Zhong, P., Martonosi, M., Ashar, P., and Malik, S. 1997. Implementing Boolean satisfiability in configurable hardware. International Workshop on Logic Synthesis.
• 202: Peixin Zhong , Margaret Martonosi , Pranav Ashar , Sharad Malik, Solving Boolean Satisfiability with Dynamic Hardware Configurations, Proceedings of the 8th International Workshop on Field-Programmable Logic and Applications, From FPGAs to Computing Paradigm, p.326-335, August 31-September 03, 1998

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Logic and constraint programming

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Constraints

  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS
      G.2.1 Combinatorics
          Subjects: Combinatorial algorithms

Keywords:
SAT, Search, constraint satisfaction