Recovering and exploiting structural knowledge from CNF formulas

Abstract

In this paper, a new pre-processing step is proposed in there solution 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(x1,…, xn)where f is a standard connective operator among (∨, ∧, ⇔) and where y and xi 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.