Using Boolean Constraint Propagation for Sub-clauses Deduction

Boolean Constraint Propagation (BCP) is recognized as one of the most useful 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 implication 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 instances.

• Type: Conference
• Year: 2005
• Where: CP
• Authors: Sylvain Darras, Gilles Dequen, Laure Devendeville, Bertrand Mazure, Richard Ostrowski, Lakhdar Sais
• Keywords: Artificial Intelligence, Boolean Constraint Propagation, Constraint Propagation, CP 2005, Sat Solver