A Promising Preprocessing Proposal for SAT Solvers

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)))

Conjecture: A SAT solver should always be given preprocessed CNFs as input. The conjecture is that the SAT solver will run faster on most preprocessed inputs.

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.