qrp2rup
This page provides a link to download an alpha implementation of our algorithm for polynomial-time validation of QCDCL certificates, as described in [1]. The source code will be published at a later time. This binary was used to carry out the experiments described in Section 7 of the paper. In order to use the program, run
$ ./qrp2rup <qrp_file> <qdimacs_file>
This will extract the certificate into <qrp_file>.cert, the RUP proof into <qrp_file>.rup, and will combine the certificate and the original formula into <qrp_file>.cnf (the validation formula). qrp2rup automatically detects whether the input formula is true or false, and whether the given proof is long-distance or not (in fact it always runs the long-distance version of the algorithm, but the results on ordinary Q-resolution proofs are identical). Afterwards, the certificate can be validated by DRAT-trim [2]
$ drat-trim <qrp_file>.cnf <qrp_file>.rup
or by calling a SAT solver on <qrp_file>.cnf. In order to generate deletion information for the RUP proof, pass the command line parameter -d n to qrp2rup, where n is a non-negative integer, 0 meaning to produce no deletion information (default), and a positive value meaning to produce deletion information for all clauses of size greater than n. Since DRAT-trim ignores deletions of unit clauses anyway, deletion information for unit clauses is never generated.
[1] Peitl, T., Slivovsky F., and Szeider S.,: Polynomial-Time Validation of QCDCL Certificates, to appear at SAT 2018 [2] Wetzler, N., Heule, M.J.H., and Hunt, Jr., W.A.: DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs. In: Theory and Applications of Satisfiability Testing (SAT) Volume 8561 of LNCS, Springer (2014) 422-429
