Constraint CNF: SAT and CSP Language Under One Roof

A new language, called constraint CNF, is proposed. It integrates propositional logic with constraints stemming from constraint programming. A family of algorithms is designed to solve problems expressed in constraint CNF. These algorithms build on techniques from both propositional satisfiability and constraint programming. The result is a uniform language and an algorithmic framework, which allow us to gain a deeper understanding of the relation between the solving techniques used in propositional satisfiability and in constraint programming and apply them together