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.

• Type: Conference
• Year: 2010
• Where: SAT
• Authors: Scott Cotton
• Keywords: Hardware, Proof Rewriting Technique, Resolution Proof, Resolution Proof Minimization, SAT 2010