#
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.