Using Boolean Constraint Propagation for sub-clauses deduction

Abstract

The Boolean Constraint Propagation (BCP) is a well-known helpful technique implemented in most state-of-the-art efficient satisfiability solvers. We propose in this paper a new use of the BCP to deduce sub-clauses from the associated implication graph. Our aim is to reduce the length of clauses thanks to the subsumption rule. We show how such extension can be grafted to modern SAT solvers and we provide some experimental results of the sub-clauses deduction as a pretreatment process. © Springer-Verlag Berlin Heidelberg 2005.