3
$\begingroup$

The file format for SAT competitions is available online here: Rules of the 2011 SAT Competition but is defacto inaccessible because all browsers redirect to the non-existing address.

Question:
where can I find a description of the SAT file format as use for the competitions that is accessible with modern browsers without having to twiddle their settings?
An informal description of the format would also suffice.

$\endgroup$
2

1 Answer 1

3
$\begingroup$

The Internet Archive Wayback Machine is able to provide a cached copy of that pdf. I'll quote from the pdf here:

4.1 CNF Input Format

The benchmark file format is in a simplified version of the DIMACS format for conjunctive normal form (CNF) propositional formulas. An example is provided in Figure 4.1

c
c start with comments
c
c
p cnf 5 3
1 -5 4 0
-1 5 3 4 0
-3 -4 0

Figure 1: Example of a CNF in the DIMACS format 

Specific Rules For the SAT Competition

  • The file can start with comments, that is lines beginning with the character c.
  • Right after the comments, there is the line p cnf <nbvar> <nbclauses> indicating that the instance is in CNF format; <nbvar> is the exact number of variables appearing in the file; <nbclauses> is the exact number of clauses contained in the file. It is guaranteed that each variable between 1 and nbvar appears at least once in a clause.
  • Then the clauses follow. Each clause is a sequence of distinct non-null numbers between -nbvar and nbvar ending with 0 on the same line. Positive numbers denote the corresponding variables. Negative numbers denote the negations of the corresponding variables. A clause is not allowed to contain the opposite literals i and -i simultaneously.

4.2 Group oriented CNF Input Format

The group oriented CNF file format is an extension of the Dimacs format that adds a group index to each clause. The group index is indicated inside curly braces at the beginning of the clause. An example is provided in Figure 4.2

c
c Example of group oriented CNF
c
c Represents the following formula
c D  = {x1 or x2 or x3}
c G1 = {x1 -> x2, x2 -> x3}
c G2 = {x3}
c G3 = {x3 -> x2, -x2 or -x3}
c G4 = {x2 -> x3}
c
p gcnf 5 7 4
{0} 1 2 3 0
{1} -1 2 0
{1} -2 3 0
{2} -3 0
{3} 2 -3 0
{3} -2 -3 0
{4} -2 3 0

Figure 2: Example of a group oriented CNF

Specific Rules For the SAT Competition

  • The file can start with comments, that is lines beginning with the character c.
  • Right after the comments, there is the line p gcnf <nbvar> <nbclauses> <lastgroupindex> indicating that the instance is in group oriented CNF format; <nbvar> is the exact number of variables appearing in the file. It is guaranteed that each variable between 1 and nbvar appears at least once in a clause. <nbclauses> is the exact number of clauses contained in the file. <lastgroupindex> is the last index of a group in the file number of components contained in the file. It is guaranteed that all groups index between 0 and <lastgroupindex> inclusive appear in the file.
  • Then the clauses follow. Each clause starts with a component number {x} with x between 0 and lastgroupindex. The specific case of 0 means that the clause belong [sic] to the set of don't care clauses (D). The rest of the clause is a sequence of distinct non-null numbers between -nbvar and nbvar ending with 0 on the same line. Positive numbers denote the corresponding variables. Negative numbers denote the negations of the corresponding variables. A clause is not allowed to contain the opposite literals i and -i simultaneously.
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.