RATZ and ZTAR

This site provides access to our RATZ and ZTAR proof compression and decompression tools. See the following paper for more details about this approach.

Marijn Heule, Armin Biere. Clausal Proof Compression. In Proc. 11th Intl. Workshop on the Implementation of Logics (IWIL'15), EPiC Series in Computing vol. 40, pages 21-26, EasyChair, 2016.
[ paper | bibtex | ratz | sbp ]

The software is available under an MIT License:

[ ratz2.tar.bz2 ]