View on GitHub


Combinatorial benchmarks for SAT solvers

Download this project as a .zip file Download this project as a tar.gz file

What is a CNF?

A propositional formula a representation of a function oven {0,1} variables. Consider such a variable x, then ¬x is a formula which has value 1-x. This is called the negation of x. Expressions of the form x and ¬x are called \literals/, and a clause is a disjunction

l₁ v l₂ v …

where each lᵢ is a literal. A clause evaluates to one if and only if at least one of the literals evaluates to one. Otherwise the clause evaluates to zero. A CNF is a conjunction of clauses

C₁ ∧ C₂ ∧ …

and the CNF evaluates to one if all clauses evaluates to one.

To falsify a formula we need an input for which the formula evaluates to 0; to satisfy a formula we need an input for which it evaluates to 1. Observe that to falsify a CNF it is sufficient to pick a clause and set the variables in such a way that all literals in the clause evaluate to zero. There is no efficient algorithm that decides whether a CNF is satisfiable or not.

DIMACS encoding of CNFs

The program outputs CNF formulas encoded in dimacs format, which has the following structure:

at the beginning of the file there may be an arbitrary number of comment lines, which must start with character c. The first non comment line specifies how many variables and how many clauses are in the CNF formulas. The next lines are sequence of non zero integers followed by zero.

p cnf <N> <M>
<i> <i> <i> <i> 0
<i> <i> <i> 0

Each line after the specification represents a clause in the following way: a positive number t is the positive literal on the variable indexed by t. A negative number t is the negated literal on the variable indexed by -t.

For example if the formula is defined on n variables x₁, x₂, x₃, …, then the line 3 -1 5 6 -4 0 encodes the clause x3 v ¬x₁ v x₅ v x₆ v ¬x₄.