Skip to Content

TU Wien Fakultät für Informatik Knowledge-Based Systems Group
Top-level Navigation: Current-level Navigation:

Path: KBS > staff > Florian Lonsing>

Tools: Drucken


I have been involved as (co-)advisor and/or (co-)author in the following projects:


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

Parallel QBF Solving

QBF Preprocessing

QBF Generator and Fuzzer

QBF Delta-Debugger


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

Home / Kontakt / Webmaster / Offenlegung gemäß § 25 Mediengesetz: Inhaber der Website ist die Fakultät für Informatik an der Technischen Universität Wien, 1040 Wien. Die TU Wien distanziert sich von den Inhalten aller extern gelinkten Seiten und übernimmt diesbezüglich keine Haftung. / Disclaimer. Datenschutzerklärung.