Skip to Content

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

Path: KBS > staff > Florian Lonsing>

Tools: Drucken


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.

Parallel QBF Solving

QBF Preprocessing

QBF Generator and Fuzzer

QBF Delta-Debugger

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.


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.