On-The-Fly Resolve Trace Minimization

14 years 29 days ago
On-The-Fly Resolve Trace Minimization
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 ...
Ohad Shacham, Karen Yorav
Added 12 Nov 2009
Updated 12 Nov 2009
Type Conference
Year 2007
Where DAC
Authors Ohad Shacham, Karen Yorav
Comments (0)