Using Boolean Constraint Propagation for Sub-clause Deduction

International audienceBoolean Constraint Propagation (BCP) is recognized as one of the most use- ful technique for efficient satisfiability checking. In this paper a new extension of the scope of boolean constraint propagation is proposed. It makes an original use of BCP to achieve further reduction of boolean formulas. Considering the impli- cation graph generated by the constraint propagation process as a resolution tree, sub-clauses from the original formula can be deduced. Then, we show how such extension can be grafted to modern SAT solvers where BCP is maintained at each step of the search tree. Preliminary results of “Zchaff” - the state of the art SAT solver - augmented with extended BCP, show the great potential of our approach with respect to certain classes of SAT instance