Benchmarking SAT Solvers for Bounded Model Checking

Benchmarking SAT Solvers for Bounded
Model Checking
Emmanuel Zarpas
IBM Haifa Research Laboratory,
zarpas@il.ibm.com
Abstract. Modern SAT solvers are highly dependent on heuristics.
Therefore, benchmarking is of prime importance in evaluating the per-
formances of different solvers. However, relevant benchmarking is not
necessarily straightforward. We present our experiments using the IBM
CNF Benchmark on several SAT solvers. Using the results, we attempt
to define guidelines for a relevant benchmarking methodology, using SAT
solvers for real life BMC applications.
1 Introduction
Over the past decade, formal verification via model checking has evolved from a
theoretical concept to a production-level technique. It is being actively used in
chip design projects across the industry, where formal verification engineers can
now tackle the verification of large industrial hardware designs. Bounded Model
Checking (BMC) [1] has recently enabled the verification of problems that used
to be beyond the reach of formal verification. However, BMC performance relies
heavily on the performance of the underlying SAT solver.
We conducted several experiments using the IBM CNF benchmark [12, 11]
to evaluate SAT tools. Often, we found discrepancies between our results and
the experimental results found in the literature. For example, our results are not
necessarily in line with the results of the SAT03 contest [4]. The main goal of this
paper is to outline a methodology for benchmarking SAT ...