Armin Biere, Florian Lonsing,
"Nenofex: Expanding NNF for QBF Solving"
: Lecture notes in computer science, Serie Lecture Notes in Computer Science (LNCS), Vol. 4996, Springer, Seite(n) 196-210, 5-2008, ISBN: 978-3-540-79718-0, ISSN: 0302-9743
Original Titel:
Nenofex: Expanding NNF for QBF Solving
Sprache des Titels:
Englisch
Original Buchtitel:
Lecture notes in computer science
Original Kurzfassung:
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.
Forschungs-