### Clausal Proof Optimizer ###

Code for CS 357 Course Project

Usage: python3 proof_optimizer.py example/cnf/random_ksat.dimacs example/proof/

Optimized Proof File: temp-work/final.proof

This code optimizes the unsatisfiability proofs generated by a Cube-and-Conquer type parallel
SAT solver into a single proof file. The optimized proof file can be checked
using the DRAT-TRIM proof checker. This optimized proof takes much lesser time
to be checked as compared to sequentially checking the individual
unsatisfiability proofs.