CNF – Conjunctive Normal Form (Dimacs format) Explained

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

Please like & share:

Leave a Reply