crup a Checker for RUP proofs in Lean 4
The only RUP proof checker that I was able to find was this one: https://www.cs.utexas.edu/~marijn/drup/. While it does still compile it segfaults and/or produces wrong results on trivial examples for some reason so I decided to build my own instead.
I dont't believe that this is a particularly good implementation of the algorithm and it does only support plain RUP, not DRUP right now (although that could be added without too much hassle if necessary).
Compiling
To compile this you need an installation of the elan Lean version manager,
set up to use Lean 4. Once you have that simply run:
$ lake build
Running
Given a DIMACS file input.cnf and a RUP file proof.rup you can verify it like so:
$ lake exe crup input.cnf proof.rup
Additionally you can change the log level (higher is less verbose) with:
$ lake exe crup input.cnf proof.rup 2
If you wish to run the binary directly you can find it in .lake/build/bin.
Note that I didn't put a particular amount of effort into supporting DIMACS or RUP files
in general. The tool expects DIMACS files to only contain the p cnf header line
and a list of clauses. The RUP file parser is designed to be able to consume
RUP files generated by picosat.
In addition to verifying UNSAT proofs by having an empty clause at the end of a RUP file this tool can also simply verify a chain of reasoning based on RUP.
If for whatever reason you wish to use this in some sort of automated fashion you do not have to parse the output, instead the tool returns the following exit codes:
0on success1on wrong usage2if it gets stuck while verifying3If it fails to demonstrate the final empty clause step in an UNSAT proof