Compression of Propositional Resolution Proofs via Partial Regularization

Pascal Fontaine, Stephan Merz, and Bruno Woltzenlogel Paleo

Abstract

This paper describes two algorithms for the compression of propositional resolution proofs. The first algorithm, RPI, performs partial regularization, removing an inference when it is redundant in the sense that its pivot literal already occurs as the pivot of another inference located below in the path to the root of the proof. The second algorithm, LU, delays the resolution of (both input and derived) unit clauses, thus removing (some) inferences having the same pivot but possibly occurring also in different branches of the proof.

© Springer-Verlag 2011

Available as: PDF

Reference

@InProceedings{fontaine:compression,
  author =       {Pascal Fontaine and Stephan Merz and Bruno {Woltzenlogel Paleo}},
  title =        {Compression of Propositional Resolution Proofs via Partial Regularization},
  booktitle = {23rd Intl. Conf. Automated Deduction (CADE 2011)},
  pages =     {237-251},
  year =      2011,
  editor =    {Nikolaj Bj{\o}rner and Viorica Sofronie-Stokkermans},
  volume =    6803,
  series =    {LNCS},
  address =   {Wroclaw, Poland},
  publisher = {Springer},
}