Department of Computer Science and Engineering CSE 150
University of California at San Diego Winter 2004


Specification of the input file format for SAT problems

To represent an instance of a SAT problem, we use an ASCII file consisting of a two major sections: the preamble and the clauses.

The Preamble
The preamble contains information about the SAT instance. This information is contained in lines. Each line begins with a single character (followed by a space) that determines the type of line. These types are as follows:

Comments
Comment lines give human-readable information about the file and are ignored by programs. Comment lines appear at the beginning of the preamble. Each comment line begins with a lower-case character c.

Problem line
There is one problem line per input file.  For conjunctive normal form instances (CNF, which is the only format we use), the problem line has pattern
p cnf VARIABLES CLAUSES

The VARIABLES field contains an integer value specifying the number n of variables in the instance. The CLAUSES field contains an integer value specifying the number of clauses in the instance. This line must occur as the last line of the preamble.

The Clauses
The clauses appear immediately after the problem line. The variables are assumed to be numbered from 1 up to n. It is not necessary that every variable actually appear in an instance.  Each clause will be represented by a sequence of numbers, each separated by either a space, a tab, or a newline character. The positive version of a variable i is represented by i; the negated version is represented by -i. Each clause is terminated by the value 0.  This format allows one clause to be on multiple lines.

Example. Using the example

(X1 or X3 or (not X4)) and (X4) and (X2 or (not X3))

a possible input file would be

c Example CNF format file
c with four variables and three clauses
p cnf 4 3
1 3 -4 0
4 0
2 -3 0