A picture of me

Florian Lonsing

Computer Science Department
Gates Computer Science Building
353 Serra Mall
Stanford University
Stanford, CA 94305-9025
e-mail: "lonsing" followed by the at-sign and "cs.stanford.edu"
WWW: http://www.florianlonsing.com/

Home Publications Software Talks


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.