ResQu
News - 2011-07: Version 0.1 released
- 2013-05: Version 1.0 released (now also works with QRP)
- 2014-05: Version 2.0 released (can perform certificate minimization)
- 2015-01: Version LP released (works with LQ resolution proofs)
Download
ResQuDescription
- ResQu is a tool for deriving Herbrand/Skolem functions from Q-resolution and Q-consensus proofs.
- Input formats:
- QBC (proof formats of Squolem, EBDDRES);
- Proof format of Qube-cert;
- QRP (Proof format of cDepQBF);
- RFAO (local input format as a right-firat-and-or formula just for certificate optimization)
- Output formats: BLIF (format of ABC synthesis tool), RFAO (same as above)
Installation and Configuration
- The download folder contains the following materials:
- "README" file explaining current features and usage of ResQu;
- /ResQu/: executables "ResQu_v2" and "ResQu_lp";
- /OtherTools/: some useful tools for complete execution workflow;
- /Examples/: examples of different proofs and certificates;
- "run_ResQu.sh": example of execution ResQu script.
- Source codes are available upon request. Please do not hesitate to contact us!
References
[1] Valeriy Balabanov and Jie-Hong R. Jiang. Resolution Proofs and Skolem Functions in QBF Evaluation and Applications. In Proc. International Conference on Computer Aided Verification (CAV'11), pp. 149-164, July 2011.
[2] Valeriy Balabanov and Jie-Hong R. Jiang. Unified QBF Certification and its Applications. Formal Methods in System Design (FMSD), 41(1): 45-65, August 2012.
[3] Valeriy Balabanov, Jie-Hong R. Jiang, Mikolas Janota and Magdalena Widl. Efficient Extraction of QBF (Counter)models from Long-Distance Resolution Proofs. AAAI conference on Artificial Intelligence, January 2015.