This is a self-contained description of a fast preprocessing technique for SAT solvers based on manipulating polynomials in one variable. We introduce the concept of a preprocessed CNF and mention that any SAT solver turns a satisfiable CNF into a preprocessed CNF. We show that any CNF F can be translated in polynomial time into an equally satisfiable, preprocessed CNF F'. A CNF F is equally satisfiable to a CNF F' if F' is obtained from F by replacing some of the variables in F by their complements.
Defn. 1: A CNF F is preprocessed if E(Z(F,b)) is maximum for b=0, i.e., E(Z(F,0)) >= E(Z(F,b)) for b in [0,1].
Defn. 2: E(Z(F,b)) is the expected fraction of satisfied clauses in F if each variable is set to true with probablity b.
Fact. 1: E(Z(F,b)) is a polynomial in b by elementary combinatorics.
Fact. 2: A CNF F can be translated in polynomial time into an equally satisfiable, preprocessed CNF F'.
Easiest proof. Use a randomized algorithm using the maximum bias b_max resulting in assignment J after a polynomial number of trials. Turn F into an equally satisfiable formula F' such that J corresponds to assignment "All 0" in F'. Iterate until the maximum bias is 0. The randomized algorithm can be turned into a linear-time preprocessor using the recurrence relation: E(Z(F(x, ...), b)) = (1-b) * E(Z(F(x=0, ...), b)) + b * E(Z((F(x=1,...), b)))
Motivation: A SAT solver will turn any satisfiable CNF into a preprocessed CNF anyway. Why not start with one and let the SAT solver improve it! Clause learning will interact nicely with the maximum bias computation.