Nenofex

Nenofex: Expanding NNF for QBF Solving. 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.


References in zbMATH (referenced in 14 articles , 1 standard article )

Showing results 1 to 14 of 14.
Sorted by year (citations)

  1. Egly, Uwe; Kronegger, Martin; Lonsing, Florian; Pfandler, Andreas: Conformant planning as a case study of incremental QBF solving (2017)
  2. Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund: Solving QBF with counterexample guided refinement (2016)
  3. Rabe, Markus N.; Seshia, Sanjit A.: Incremental determinization (2016)
  4. Tentrup, Leander: Non-prenex QBF solving using abstraction (2016)
  5. Janota, Mikoláš; Marques-Silva, Joao: Expansion-based QBF solving versus Q-resolution (2015)
  6. Janota, Mikoláš; Grigore, Radu; Marques-Silva, Joao: On QBF proofs and preprocessing (2013)
  7. Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund: Solving QBF with counterexample guided refinement (2012)
  8. Biere, Armin; Lonsing, Florian; Seidl, Martina: Blocked clause elimination for QBF (2011)
  9. Lonsing, Florian; Biere, Armin: Failed literal detection for QBF (2011)
  10. Giunchiglia, Enrico; Marin, Paolo; Narizzano, Massimo: sQueezeBF: an effective preprocessor for QBFs based on equivalence reasoning (2010)
  11. Goultiaeva, Alexandra; Bacchus, Fahiem: Exploiting circuit representations in QBF solving (2010)
  12. Klieber, William; Sapra, Samir; Gao, Sicun; Clarke, Edmund: A non-prenex, non-clausal QBF solver with game-state learning (2010)
  13. Peschiera, Claudia; Pulina, Luca; Tacchella, Armando; Bubeck, Uwe; Kullmann, Oliver; Lynce, In^es: The seventh QBF solvers evaluation (QBFEVAL’10) (2010)
  14. Lonsing, Florian; Biere, Armin: Nenofex: Expanding NNF for QBF solving (2008)