This post is just to explain the CNF DIMACS file format to people new to SAT
Boolean Operators
V – OR
^ – AND
¬ – NOT/Negation
Variable – can assume only values either 1 (true/ON) or 0 (false/OFF)
Clause – is the disjunction of a number of variables (negations may also be present)
A CNF expression is made up of conjunction of one or more clauses.
Every Satisfiability problem can be expressed in CNF (conjunctive normal form).
File Format
At the begining of the file there can exist one or more comment line.
comment lines start with a ‘c’
Example:
c This is a comment
c This is another comment
The following lines are information about the expression itself so an example expression is used to help understanding.
(A v ¬B v C) ^ (B v D v E) ^ (D V F)
After comments if any comes the Problem line starts with a ‘p’
p FORMAT VARIABLES CLAUSES
FORMAT is for programs to detect which format is to be expected. Which should always be ‘cnf’
VARIABLES is the count of number of unique variables in the expression
A,B,C,D,E,F
VARIABLES = 6
CLAUSES is the number of clauses in the expression
(A v ¬B v C) ^ (B v D v E) ^ (D V F)
1 1 1 = 3
results to
p cnf 6 3
This line is followed by the information in each clause
unique variables are enumerated from 1 to n
A,B,C,D,E,F
1,2,3,4,5,6
such that
1 represents A
2 represents B
3 represents C
etc…
a negation is represented as ‘-‘
e.g.
-1 represents ¬A
Each variable information is seprated by a blank space
so
(A v ¬B v C) is represented by 1 -2 3
Add a 0 behind to indicate the end of the clause
so
(A v ¬B v C) is represented by 1 -2 3 0
(B v D v E) is represented by 2 4 5 0
(D V F) is represented by 4 6 0
The final File will be
c This is a comment
c This is another comment
p cnf 6 3
1 -2 3 0
2 4 5 0
4 6 0
Some Considerations
If you are building a parser
-the final 0 is sometimes ommited.
If you are building a SAT solver
-CNF is used just to have a common way of expressing the file format your SAT solver could transform the expression in another format for a different strategy.
Further Readings
http://en.wikipedia.org/wiki/Conjunctive_normal_form
http://www.domagoj-babic.com/uploads/ResearchProjects/Spear/dimacs-cnf.pdf
http://classes.soe.ucsc.edu/cmps132/Winter05/hw/hw8sols.pdf