# 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