QDIMACS standard

Version 1.1

Released on December 21, 2005

[Introduction] - [Input format] - [Output format]

Introduction

This page defines a suggested standard for the input and output formats of quantified Boolean formulas (QBFs) solvers. The proposed standard is a stricter version of the original QDIMACS draft which, in turn, is built on top of the DIMACS standard for SAT solvers. The standard is comprised of two specifications:

Input format How to format the input QBF instance; the format is geared towards getting simple parsers and maintaining backward compatibility with the DIMACS format (any DIMACS/SAT instance is also a QDIMACS/QSAT instance).
Output format How to format the output of a QBF solver; this includes the answer to the question "Is the input QBF true?", a partial certificate of the input QBF truth/falsity, and optional further information on the solver execution.

For questions, comments and any other issue regarding the QDIMACS suggested standard please get in touch with qbfeval AT qbflib DOT org.

[Introduction] - [Input format] - [Output format]

Input format

The input format is described by the following BNF grammar:

<input> ::= <preamble> <prefix> <matrix> EOF

<preamble>      ::= [<comment_lines>] <problem_line>
<comment_lines> ::= <comment_line> <comment_lines> | <comment_line> 
<comment_line>  ::= c <text> EOL
<problem_line>  ::= p cnf <pnum> <pnum> EOL

<prefix>     ::= [<quant_sets>]
<quant_sets> ::= <quant_set> <quant_sets> | <quant_set>
<quant_set>  ::= <quantifier> <atom_set> 0 EOL
<quantifier> ::= e | a
<atom_set>   ::= <pnum> <atom_set> | <pnum>

<matrix>      ::= <clause_list>
<clause_list> ::= <clause> <clause_list> | <clause> 
<clause>      ::= <literal> <clause> | <literal> 0 EOL
<literal>     ::= <num>

<text>  ::= {A sequence of non-special ASCII characters}
<num>   ::= {A 32-bit signed integer different from 0}
<pnum>  ::= {A 32-bit signed integer greater than 0}

where the terminal symbols EOL and EOF stand for the end-of-line and end-of-file markers respectively, [<expr>] denotes that <expr> is an optional expression, and concatenation of expressions has precedence over choice between expressions.

The syntax above is subject to the following additional constraints:

Let v be the the first positive non-zero integer specified in the problem line: v corresponds to the number of distinct atoms appearing in the prefix and in the matrix, i.e., all the members of the quantified sets are less than or equal to v, and the absolute value of each literal in all the clauses is less than or equal to v.
Let c be the second positive non-zero integer specified in the problem line: c corresponds to the number of clauses appearing in the matrix, i.e., the number of <clause> expressions which <matrix> is comprised of.
Each atom appearing in the prefix, must also appear in the matrix. The converse may not be true, i.e., we allow atoms to appear in the matrix that are not bound by any quantifier in the prefix. Unbound atoms are to be considered as being existentially quantified in the first (i.e., the outermost) quantified set. This is to retain backward compatibility with the DIMACS format: any DIMACS instance is also a QDIMACS instance.

Contiguous quantified sets bound by the same type of quantifier are disallowed. The following example should clarify this point:

Wrong! Contiguous 'e' sets

  p cnf 4 2
  e 1 2 3 4 0
  -1  2 0
   2 -3 -4 0

Ok! Single 'e' set

  p cnf 4 2
  -1  2 0
   2 -3 -4 0

Ok! DIMACS compatibility

The same atom cannot appear bound in the prefix more than once.
The innermost quantified set is always of type 'e'.

[Introduction] - [Input format] - [Output format]

Output format

The output format is described by the following BNF grammar:

<output> ::= <preamble> [<certificate>] EOF

<preamble>      ::= [<comment_lines>] <solution_line>
<comment_lines> ::= <comment_line> <comment_lines> | <comment_line> 
<comment_line>  ::= c <text> EOL
<solution_line> ::= s cnf <answer> <pnum> <pnum> EOL
<answer>        ::= 1 | 0 | -1 

<certificate> ::= <cert_lines>
<cert_lines>  ::= <cert_line> <cert_lines> | <cert_line> 
<cert_line>   ::= V <literal> EOL
<literal>     ::= <num>

<text>  ::= {A sequence of non-special ASCII characters}
<num>   ::= {A 32-bit signed integer different from 0}
<pnum>  ::= {A 32-bit signed integer greater than 0}

and it is subject to the following additional constraints:

The first positive non-zero integer specified in the solution line after the answer coincides with the first such number in the problem line of the input file, i.e., it is the number of distinct atoms appearing in the prefix and in the matrix of the input file.
The second positive non-zero integer specified in the solution line after the answer coincides with the second such number in the problem line of the input file, i.e., the number of clauses appearing in the matrix of the input file.
The answer to the problem is either 1, 0, or -1 indicating that the input QBF was found true, false, or remained unsolved, respectively.
The certificate lines report the values assigned to the literals in the outermost quantified set of the input file in the following cases:
- the outermost quantified set is bound by 'a' and the answer is 0, or
- the outermost quantified set is bound by 'e' and the answer is 1.
Notice that in the case of a satisfiable DIMACS input file, the certificate lines report the complete witness found by the solver.