Sciweavers

34
Voted
SAT
2010
Springer

Two Techniques for Minimizing Resolution Proofs

14 years 2 months ago
Two Techniques for Minimizing Resolution Proofs
Some SAT-solvers are equipped with the ability to produce resolution proofs for problems which are unsatisfiable. Such proofs are used in a variety of contexts, including finding minimal unsatisfiable sets of clauses, interpolant generation, configuration management, and proof replay in interactive theorem provers. In all of these settings, the size of the proof may be prohibitively large for subsequent processing. We suggest some new methods for resolution proof minimization. First, we identify a simple and effective method of extracting shared structure from a proof using structural hashing. Second, we suggest a heuristically-guided proof rewriting technique based on variable valuations. Our findings indicate structural sharing reduces proof length significantly and efficiently, and that our valuation-based rewriting method can give substantial further reductions but is currently limited to smaller proofs.
Scott Cotton
Added 16 Aug 2010
Updated 16 Aug 2010
Type Conference
Year 2010
Where SAT
Authors Scott Cotton
Comments (0)