We have experimented a UP-based pre-treatment to eliminate redundant clauses in
SAT instances extensively on the last SAT competitions benchmarks (
http://www.satcompetition.org). We
have tested more than 700 SAT instances which are from various domains
(industrial, random,handmade, graph-coloring, ...). Three of the winners of the
last three competitions, namely ZChaff, Minisat and SatElite have been selected
as SAT solvers. All experiments have been conducted on Pentium IV, 3Ghz under
linux Fedora Core 4.