Nenofex, an expansion-based QBF solver for negation normal form
Fetching latest commit…
Cannot retrieve the latest commit at this time.
|Type||Name||Latest commit message||Commit time|
|Failed to load latest commit information.|
March 2017 ------------------- GENERAL INFORMATION ------------------- This is Nenofex ("NEgation NOrmal Form EXpansion"), 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: Florian Lonsing, Armin Biere: Nenofex: Expanding NNF for QBF Solving. Proceedings of SAT 2008, volume 4996 of LNCS, Springer, 2008. Version 1.1 is a maintenance release: - added simple API to enable library use - added support for most recent versions of PicoSAT solver Apart from code maintenance, Nenofex is no longer actively developed. For bug reports, please contact Florian Lonsing (see below). ------------ INSTALLATION ------------ Create a new directory DIR. Download the latest source package of PicoSAT from http://fmv.jku.at/picosat/ copy it to DIR and unpack it. Installation should work with version 965 or any later version. In the directory of PicoSAT, call './configure -O -static' and then 'make'. Make sure that the directory of PicoSAT is named 'picosat'. Rename it if necessary. Copy the source package of Nenofex to directory DIR and unpack it. The directory tree should now look like 'DIR/picosat' and 'DIR/nenofex'. Call 'make' in the directory of Nenofex which produces optimized code without assertions. The compilation process of Nenofex requires to have PicoSAT compiled before in directory 'DIR/picosat/'. ----------------------- CONFIGURATION AND USAGE ----------------------- Call './nenofex -h' to display usage information. Calling Nenofex without command line parameters results in default behaviour. The solver returns exit code 10 if the given instance was found satisfiable and exit code 20 if the instance was found unsatisfiable. Any other exit code indicates that the instance was not solved. The subdirectory 'test' contains example programs that demonstrate the use of the library of Nenofex. ------- License ------- DepQBF is free software released under GPLv3: https://www.gnu.org/copyleft/gpl.html See also the file COPYING. Nenofex uses the SAT solver PicoSAT as an external library. http://fmv.jku.at/picosat/ Please see the license of PicoSAT for further information. ------- CONTACT ------- For comments, questions, bug reports etc. related to Nenofex please contact Florian Lonsing. See also http://www.kr.tuwien.ac.at/staff/lonsing/