Probing-based preprocessing techniques for propositional satisfiability

Preprocessing is an often used approach for solving hard instances of propositional satisfiability (SAT). Preprocessing can be used for reducing the number of variables and for drastically modifying the set of clauses, either by eliminating irrelevant clauses or by inferring new clauses. Over the years, a large number of formula manipulation techniques has been proposed, that in some situations have allowed solving instances not otherwise solvable with state-of-the-art SAT solvers. This paper proposes probing-based preprocessing, an integrated approach for preprocessing propositional formulas, that for the first time integrates in a single algorithm most of the existing formula manipulation techniques. Moreover, the new unified framework can be used to develop new techniques. Preliminary experimental results illustrate that probing-based preprocessing can be effectively used as a preprocessing tool in state-of-the-art SAT solvers.