A picture of me

Florian Lonsing

e-mail: "fml" followed by the at-sign and "florianlonsing.com"
WWW: http://www.florianlonsing.com/

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):


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 https://github.com/lonsing/nenofex.