Florian Lonsing 




Home  Publications  Software  Talks 
This page mainly describes projects developed between 2008 and 2018. See also my GitHub profile and, for more recent software, the GitHub profile of the Upscale project carried out at Stanford.
I have been involved as (co)advisor and/or (co)author in the following projects (among others):HordeQBF is a modular and massively parallel QBF solver. It consists of an MPIbased 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 MPIbased 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.
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). We also published a related tool paper at SAT 2019.
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 FailedLiteral Preprocessing for Quantified Boolean Formulas. in Proc. SAT 2012.
Nenofex ("NEgation NOrmal Form EXpansion") is an expansionbased 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.