| About ALCom | News | People | Research | Publications | Tools | Student Info | Links |

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

      ResQu

Description

      - 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.