Software
I have been involved as (co-)advisor and/or (co-)author in the following projects:DepQBF
DepQBF is a search-based QBF solver with conflict-driven clause and solution-driven cube learning. Please click here for further information.QBF Certificate Extraction and Checking
- QBFcert (developed by Aina Niemetz and Mathias Preiner) is a framework for resolution-based extraction and checking of certificates for QBFs. E.g., it can be used to check proofs produced by DepQBF and extract Skolem/Herbrand functions.
Parallel QBF Solving
-
HordeQBF is a modular and massively parallel QBF solver. It consists of an MPI-based flexible parallelization framework and integrates DepQBF as a core solver. HordeQBF is a joint project of Tomas Balyo and Florian Lonsing. See also the related SAT 2016 tool paper (PDF preprint).
-
MPIDepQBF is an MPI-based parallel QBF solver without knowledge sharing. It implements a master/worker architecture . A worker consists of an instance of the solver DepQBF. The master balances the workload by generating subproblems defined by variable assignments (assumptions), which are solved by the workers. MPIDepQBF is a joint project of Charles Jordan, Lukasz Kaiser, Florian Lonsing, and Martina Seidl. See also the related SAT 2014 tool paper. Source code of MPIDepQBF is available as part of the Toss project.
QBF Preprocessing
QRATPre+ is a preprocessor to simplify quantified Boolean formulas (QBFs) given in prenex conjunctive normal form (PCNF). For simplification, QRATPre+ tries to eliminate redundant clauses from the PCNF, or universal literals from clauses. It implements redundancy checking based on the QRAT+ proof system.
Source code is available on GitHub.
The theory behind QRATPre+ is described in our IJCAR 2018 paper (preprint on arXiv).
QxBF is a preprocessor for QBFs in prenex CNF based on failed literal detection (FL). The basic idea is to assign some variable as assumption. If boolean constraint propagation (QBCP) yields an empty clause then the negated assumption can be added as a new unit clause to the CNF.
Further information and source code can be found here.
Failed literal detection for QBF as implemented in QxBF was extended by Allen Van Gelder and Samuel Wood. See also the paper A. Van Gelder, S. B. Wood, F. Lonsing: Extended Failed-Literal Preprocessing for Quantified Boolean Formulas. in Proc. SAT 2012.
- Bloqqer is a preprocessor for QBFs in prenex CNF which implements techniques such as quantified blocked clause elimination, equivalence reasoning etc. See also the paper A. Biere, F. Lonsing, and M. Seidl. Blocked Clause Elimination for QBF. Source code and further information can be found here.
QBF Generator and Fuzzer
- BlocksQBF is a generator for random QBFs. Source code and further information can be found here.
- QBFuzz (implemented by Mathias Preiner) is a fuzzer which generates random QBFs. Source code and further information can be found here.
QBF Delta-Debugger
- QBFDD (implemented by Aina Niemetz) is a delta-debugger for QBFs in QDIMACS format. Source code and further information can be found here.
Nenofex
Nenofex ("NEgation NOrmal Form EXpansion") is an expansion-based QBF solver which operates on negation normal form (NNF). A formula in NNF is represented as a structurally restricted tree. Expansions of variables from the two rightmost quantifier blocks are scheduled based on estimated expansion costs. Further information can be found in our SAT'08 paper.
Nenofex is no longer actively developed. Source code is available from GitHub at https://github.com/lonsing/nenofex.