Reducing the size of resolution proofs in linear time
Venue
International Journal on Software Tools for Technology Transfer, vol. 13 (2011)
Publication Year
2011
Authors
Omer Bar Ilan, Oded Fuhrmann, Ofer Strichman, Ohad Shacham, Shlomo Hoory
BibTeX
Abstract
DPLL-based SAT solvers progress by implicitly applying bi- nary resolution. The
resolution proofs that they generate are used, afterthe SAT solver’s run has
terminated, for various purposes. Most notable uses in formal verification are:
extracting an unsatisfiable core, extracting an interpolant, and detecting clauses
that can be reused in an incremental satisfiability setting (the latter uses the
proof only implicitly, during the run of the SAT solver). Making the resolution
proof smaller can benefit all of these goals: it can lead to smaller cores, smaller
interpolants, and smaller clauses that are propagated to the next SAT instance in
an incremental setting. We suggest two methods that are linear in the size of the
proof for doing so. Our first technique, called Recycle-Units , uses each learned
constant (unit clause) (x) for simplifying resolution steps in which x was the
pivot, prior to when it was learned. Our second technique, called Recycle-Pivots,
simplifies proofs in which there are several nodes in the resolution graph, one of
which dominates the others, that correspond to the same pivot. Our experiments with
industrial in- stances show that these simplifications reduce the core by ≈ 5% and
the proof by ≈ 13%. It reduces the core less than competing methods such as
run-till-fix, but whereas our algorithms are linear in the size of the proof, the
latter and other competing techniques are all exponential as they are based on SAT
runs. If we consider the size of the proof (the resolution graph) as being
polynomial in the number of variables (it is not necessarily the case in general),
this gives our method an exponen- tial time reduction comparing to existing tools
for small core extraction. Our experiments show that this result is evident in
practice more so for the second method: rarely it takes more than a few seconds,
even when competing tools time out, and hence it can be used as a cheap proof
post-processing procedure.
