Propositional Satisfiability and Constraint Programming: A comparative Survey

Propositional Satisfiability and Constraint Programming: A comparative Survey. Lucas Bordeaux; Youssef Hamadi; L. Zhang.

Propositional Satisfiability (SAT) and Constraint Programming (CP) have developped as two relatively independent threads of research, cross-fertilising occasionally. These two approaches to problem solving have a lot in common, as evidenced by similar ideas underlying the branch and prune algorithms which 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 report 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.

This is a long and detailed survey, that may serve as an introduction to the two fields.

How useful these searching strategies are as programming language constructs is open to debate, of course.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Greatly appreciate links like

Greatly appreciate links like this as well as the Logic/Declaritive archive! Thanks.

Nice, but,

Bit lacking on BDD research. Are there any complexity theorists on LtU? I always find that the current preoccupation of SAT-solving with the CNF encoding bothers me a bit, are CNF based solvers actually the fastest or just fast on different propositional problems?