Resolution-Based Simplification Techniques of CNF Formulas

I will present some new resolution based simplification techniques for CNF. The techniques can be applied either as a pre-processor of a SAT solver, or during the SAT solving itself. The intended area of application are CNFs produced from circuit netlists, typically in bounded model checking (BMC) or
induction-based hardware verification problems.
Extensive benchmarking shows that such simplification gives a speedup between 5-10 times on this type of problem. The simplification can be viewed as a partial solution to the problem of generating good CNFs.

Niklas Een received his M.S. degree in computer science from Uppsala University in 1999, and is currently working towards his Ph.D. degree at
Chalmers University of Technology under the direction of Mary Sheeran. His research interests include SAT solving and SAT-based model checking of hardware systems.