Skeptik: subsumption-based proof compression algorithms

by Andreas Fellner for Computational Science and Engineering at TU Wien

Skeptik is a program for converting resolution proofs produced by solvers into shorter, equivalent ones. To this end various compression algorithms have already been implemented. I intend to enrich this collection of algorithms to produce even shorter proofs while remaining in a reasonable computation time window. I would like to implement three new algorithms. Those are Subsumption, RecycleUnits and a variation of the already implemented RecyclePivots algorithm. The first two are described in the literature, but both also leave room for improvement. While I intend to generalize RecycleUnits, Subsumption needs some adaption in order to have the required efficiency.