Recovering and Exploiting Structural Knowledge from CNF Formulas.

In this paper, a new pre-processing step is proposed in the resolution of SAT instances, that recovers and exploits structural knowledge that is hidden in the CNF. It delivers an hybrid formula made of clauses together with a set of equations of the form y = f(x₁,..., x_n) where f is a standard connective operator among (⌄, 〉, ⤔) and where y and x_i are boolean variables of the initial SAT instance. This set of equations is then exploited to eliminate clauses and variables, while preserving satisfiability. These extraction and simplification techniques allowed us to implement a new SAT solver that proves to be the most efficient current one w.r.t. several important classes of instances. [ABSTRACT FROM AUTHOR]