# CNFgen - background

# CNFgen

## Combinatorial benchmarks for SAT solvers

### What is a CNF?

A propositional formula is a representation of a function over
\(\{\mathrm{True},\mathrm{False}\}\) variables. Consider such
a variable \(x\), the formula \(\overline{x}\) is called the *negation*
of \(x\), and has the opposite value of \(x\). Expressions of the form
\(x\) and \(\overline{x}\) are called *literals*, and a *clause* is
a disjunction

\[ \ell_1 \lor \ell_2 \ldots \]

where each \(\ell_i\) is a literal. A clause evaluates to
\(\mathrm{True}\) when **at least** one of the literals evaluates to
\(\mathrm{True}\), and evaluates to \(\mathrm{False}\) otherwise. A CNF
is a conjunction of clauses \[ C_1 \land C_2 \ldots \]

and the CNF evaluates to \(\mathrm{True}\) if **all** clauses evaluates
to \(\mathrm{True}\).

To **falsify** a formula we need an input for which the formula
evaluates to \(\mathrm{False}\); to **satisfy** a formula we need an
input for which it evaluates to \(\mathrm{True}\). 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
\(\mathrm{False}\). 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_1, x_2,
x_3, \ldots\), then the line `3 -1 5 6 -4 0`

encodes the clause \(x_3
\lor \overline{x_1} \lor x_5 \lor x_6 \lor \overline{x_4}\).