Efficient Extraction of Skolem Functions from QRAT Proofs


Our tool QRAT-trim can be downloaded here: qrat-trim.c
Our tool cheskol can be downloaded here: cheskol.c

Compile using:
gcc qrat-trim.c -O2 -o qrat-trim
gcc cheskol.c   -O2 -o cheskol

The QRAT-trim tool expects at least to input files:
- INPUT.qdimacs: the original problem in QDIMACS format
- PROOF.qrat: a QRAT proof for the INPUT_FILE

To obtain a QRAT proof for INPUT.qdimacs use bloqqer with QRAT support.
Additionally, one needs specify that the proof is for a true QBF (using -S)
and the output file for Skolem functions in the AAG format (using -a FILE).
For example run:
./qrat-trim INPUT.qdimacs PROOF.qrat -S -a SKOLEM.aag
The cheskol tool check dependencies and generates a SAT formula for INPUT.qdiamcs
using Skolem functions in SKOLEM.aag. For example run:
./cheskol INPUT.qdimacs SKOLEM.aag > TOCHECK.cnf

The log files of our experiments can be found here.