On-the-fly resolve trace minimization

Abstract

The ability of modern SAT solvers to produce proofs of unsatisfiability for Boolean formulas has become a powerful tool for EDA applications. Proofs are generated from a resolve trace that captures information about the creation of all conflict clauses. Due to their sizes, resolve traces are kept in files. The sizes of these files makes the use of proofs of unsatisfiability impractical for industrial tools. Although only a small part of the resolve trace is eventually used, until now it was not known how to filter out unnecessary information. We propose a simple algorithm for on-the-fly resolve trace minimization in which we identify clauses that are guaranteed not to take part in the proof of unsatisfiability, and delete all of their associated information. This algorithm dramatically decreases the size of the resolve trace, to the point where it can be stored in the main memory. Our experiments reveal that the minimized trace is typically 3 to 6 times smaller. This makes the use of proofs of unsatisfiability and the computation of unsat cores more practical and will enable future applications to take advantage of it. Copyright 2007 ACM.