# CNFgen - background

# CNFgen

## Combinatorial benchmarks for SAT solvers

### 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₄.