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.
The software is available under an MIT License:
[ ratz2.tar.bz2 ]