TY - GEN
T1 - Nenofex: Expanding NNF for QBF Solving
AU - Biere, Armin
AU - Lonsing, Florian
PY - 2008/5
Y1 - 2008/5
N2 - The topic of this paper is Nenofex, a solver for quantified boolean
formulae (QBF) in negation normal form (NNF), which relies on
expansion as the core technique for eliminating variables. In contrast
to eliminating existentially quantified variables by resolution on
CNF, which causes the formula size to increase quadratically in the
worst case, expansion on NNF is involved with only a linear increase
of the formula size. This property motivates the use of NNF instead of
CNF combined with expansion. In Nenofex, a formula in NNF is
represented as a tree with structural restrictions in order to keep
its size small and distances from nodes to the root short. Expansions
of variables are scheduled based on estimated expansion cost. The
variable with the smallest estimated cost is expanded first. In order
to remove redundancy from the formula, limited versions of two
approaches from the domain of circuit optimization have been
integrated. Experimental results on latest benchmarks show that
Nenofex indeed exceeds a given memory limit less frequently than a
resolution-based QBF solver for CNF, but also that there is the need
for runtime-related improvements.
AB - The topic of this paper is Nenofex, a solver for quantified boolean
formulae (QBF) in negation normal form (NNF), which relies on
expansion as the core technique for eliminating variables. In contrast
to eliminating existentially quantified variables by resolution on
CNF, which causes the formula size to increase quadratically in the
worst case, expansion on NNF is involved with only a linear increase
of the formula size. This property motivates the use of NNF instead of
CNF combined with expansion. In Nenofex, a formula in NNF is
represented as a tree with structural restrictions in order to keep
its size small and distances from nodes to the root short. Expansions
of variables are scheduled based on estimated expansion cost. The
variable with the smallest estimated cost is expanded first. In order
to remove redundancy from the formula, limited versions of two
approaches from the domain of circuit optimization have been
integrated. Experimental results on latest benchmarks show that
Nenofex indeed exceeds a given memory limit less frequently than a
resolution-based QBF solver for CNF, but also that there is the need
for runtime-related improvements.
UR - https://www.scopus.com/pages/publications/44649145387
U2 - 10.1007/978-3-540-79719-7_19
DO - 10.1007/978-3-540-79719-7_19
M3 - Conference proceedings
SN - 3540797181
SN - 9783540797180
VL - 4996
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 196
EP - 210
BT - Theory and Applications of Satisfiability Testing - SAT 2008 - 11th International Conference, SAT 2008, Proceedings
PB - Springer
ER -