July 2012 ------------------------------------------------------------------------------- GENERAL ------------------------------------------------------------------------------- This is the first release of QRPcert, a tool for extracting Skolem/Herbrand function-based QBF certificates from Q-resolution proofs. QRPcert is part of a framework for extracting and validating QBF certificates. For more information see 'http://fmv.jku.at/qbfcert/' and our tool paper at SAT'12: @inproceedings{DBLP:conf/sat/NiemetzPLSB12, author = {Aina Niemetz and Mathias Preiner and Florian Lonsing and Martina Seidl and Armin Biere}, title = {Resolution-Based Certificate Extraction for QBF - (Tool Presentation)}, booktitle = {SAT}, year = {2012}, pages = {430-435}, ee = {http://dx.doi.org/10.1007/978-3-642-31612-8_33}, crossref = {DBLP:conf/sat/2012}, bibsource = {DBLP, http://dblp.uni-trier.de} } The algorithm for extracting Skolem/Herbrand functions is based on the approach presented in: @inproceedings{DBLP:conf/cav/BalabanovJ11, author = {Valeriy Balabanov and Jie-Hong R. Jiang}, title = {Resolution Proofs and Skolem Functions in QBF Evaluation and Applications}, booktitle = {CAV}, year = {2011}, pages = {149-164}, ee = {http://dx.doi.org/10.1007/978-3-642-22110-1_12}, crossref = {DBLP:conf/cav/2011}, bibsource = {DBLP, http://dblp.uni-trier.de} } QRPcert is released under GPL version 3. A copy of the license can be found in the file COPYING. If no file COPYING has been delivered with this release it can also be found at 'http://www.gnu.org/licenses/gpl.txt'. ------------------------------------------------------------------------------- CHANGELOG ------------------------------------------------------------------------------- Version 1.0.1 - Fixed parser bug for files > 4GB - Fixed re-encoding of AIG for reading binary aiger - Added abort() in case of incorrect universal/existential reduction - Sorting literals is now done after parsing Version 1.0 - First public release ------------------------------------------------------------------------------- BUILD ------------------------------------------------------------------------------- Unpack the sources and call 'make'. By default, it produces optimized code without any assertions enabled. If you want to compile QRPcert with assertions enabled call 'make debug'. Note that QRPcert may run considerably slower if assertions are enabled. ------------------------------------------------------------------------------- USAGE ------------------------------------------------------------------------------- Basic usage: './qrpcert ' For more usage information call './qrpcert -h'. QRPcert supports Q-resolution proofs in QRP format (ascii and binary version). A detailed description can be found at 'http;//fmv.jku.at/qbfcert/qrp.format'. Skolem/Herbrand functions are represented as AIGs in AIGER format (ascii and binary version supported; for more information see 'http://fmv.jku.at/aiger/'). By default, QRPcert produces QBF certificates in binary AIGER format. A certificate generated by QRPcert consists of a set of AIGs, which represent Skolem/Herbrand functions of the corresponding existential/universal variables. Each primary output of the certificate AIG corresponds to a Skolem/Herbrand function denoted by the respective variable index (in ascii AIGER format). In case the certificate is generated in binary AIGER format, the input/output indices do not correspond to the variable indices used in the input formula. Therefore, QRPcert additionally produces a symbol table for each input/output of the AIG, which maps the reencoded indices to the original variable indices of the input formula. As an example, consider following QBF formula in QDIMACS format: p cnf 9 6 a 1 2 0 e 3 0 a 4 0 e 5 6 0 a 7 0 e 8 9 0 4 5 -7 -8 0 6 -7 -8 0 -5 -6 7 0 -2 3 8 0 1 -3 -9 0 8 9 0 DepQBF produces the following Q-resolution trace of unsatisfiability: p qrp 9 6 a 1 2 0 e 3 0 a 4 0 e 5 6 0 a 7 0 e 8 9 0 1 4 5 -7 -8 0 0 2 6 -7 -8 0 0 3 -5 -6 7 0 0 4 -2 3 8 0 0 5 1 -3 -9 0 0 6 8 9 0 0 7 1 -3 8 0 5 6 0 8 1 -2 8 0 7 4 0 9 -5 -7 -8 0 3 2 0 10 4 -7 -8 0 9 1 0 11 0 10 8 0 r UNSAT QRPcert extracts a corresponding Herbrand function-based QBF certificate (# comments not included): aag 10 5 0 4 5 # ascii AIGER header 6 # i0 ex. var 3 10 # i1 ex. var 5 12 # i2 ex. var 6 16 # i3 ex. var 8 18 # i4 ex. var 9 2 # o0 un. var 1 4 # o1 un. var 2 8 # o2 un. var 4 14 # o3 un. var 7 2 1 0 # f_1 = false 4 1 1 # f_2 = true 8 1 0 # f_4 = false 20 10 12 14 1 21 # f_7 = true /\ not (5 /\ 6) The binary AIGER version of the certificate is as follows: aig 10 5 0 4 5 # binary AIGER header # i0 - i4 implicitely defined 12 # o0 reencoded index 6 14 # o1 reencoded index 7 16 # o2 reencoded index 8 20 # o3 reencoded index 10 [...] # binary AND gate encoding (omitted) i0 3 # i0 (2) mapped to ex. var 3 i1 5 # i1 (4) mapped to ex. var 5 i2 6 # i2 (6) mapped to ex. var 6 i3 8 # i3 (8) mapped to ex. var 8 i4 9 # i4 (10) mapped to ex. var 9 o0 1 # o0 (12) mapped to un. var 1 o1 2 # o1 (14) mapped to un. var 2 o2 4 # o2 (16) mapped to un. var 4 o3 7 # o3 (20) mapped to un. var 7 The binary AIGER version defines only the primary output indices. After the definition of the AND gates, QRPcert also produces a symbol table, which maps each input/output to its original variable index. For example, o0 (output 0, re-encoded to index 12) is mapped to variable index 1 of the input formula. A more detailed description of QRPcert (with ascii AIGER support) can be found in: 'http://fmv.jku.at/preiner/papers/preiner-master_thesis-2012.pdf' ------------------------------------------------------------------------------- CONTACT ------------------------------------------------------------------------------- For comments, questions, bug reports etc. please contact Mathias Preiner. See also 'http://fmv.jku.at/preiner/' and 'http://fmv.jku.at/qbfcert/'.