A Comparison between SAT and CSP Techniques

The aim of this paper is to establish a connection between the propositional logic and the constraint based reasoning frameworks. This work is based on a translation of the satisfiability problem (SAT) into the binary constraint-satisfaction problem (CSP). The structure of the SAT problem and its associated CSP are then exploited together for characterizing tractable SAT problems, increasing the effectiveness of the classical reduction rules: unit clause and monotone literal rules, and expressing the arc and path consistency concepts with logical inference rules. This study leads to compare the behaviors of the DP and MAC procedures for solving respectively a SAT instance and its binary CSP expression.