Duaffle version 1.0NL Cornell University, 2007 April 10, 2007 This package contains the QBF solver Duaffle version 1.0NL (without learning), which uses a dual-format "cnfdnf" file as input. This file contains a set of traditional CNF clauses as well as a set of DNF terms. See example.qdimacs for an example of such a file. The syntax is essentially the same as the standard QDIMACS format for QBF, except that the header line looks like p cnfdnf and the constraints are divided into two parts separated by a line containing only a zero. The first part has CNF constraints as a set of clauses while the second part has DNF constraints as a set of terms. Semantically they are joined together using the logical operator specified in the header, which is either "or" or "and". Lines beginning with a 'c' are treated as comments as usual. NOTICE: THIS CODE IS STILL UNDER PROGRESS AND DOES NOT HAVE CLAUSE- AND SOLUTION-LEARNING ENABLED!! Nonetheless, it often performs quite well compared to other state-of-the-art QBF solvers. See, e.g., results published in the above paper. COMPILATION: Type "make" to compile using g++; this will create an executable called duaffle. USAGE: The usage is same as that of its parent QBF solver, Quaffle: duaffle cnfdnf_file [optional time_limit in seconds] USAGE EXAMPLE: duaffle example.qdimacs This will evaluate the input dual-format QBF formula and output QSAT or QUNSAT depending on the result. In addition, when QSAT, it will also output the values of the variables in the first existential layer that were found to lead to a consistent solution. This solution printing may be turned off by commenting out the corresponding line in the file config.h and recompiling. For further details, please see the paper "QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency" in the proceedings of SAT-06 (also available from http://www.cs.cornell.edu/~sabhar). --- Please report bugs and send comments/questions to Ashish Sabharwal, sabhar at cs dot cornell dot edu.