Page personnelle d'Olivier Fourdrinoy    cril
 

Eliminating redundant clauses in SAT instances

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.


Handmade Instances

Random Instances

Industrial Instances

 

Home  l  Recherche l  Enseignement  l  Liens l  Contact

Copyrights 2006 Olivier Fourdrinoy. All rights reserved