This code is a collection of tools for the manipulation of CNF formulas in dimacs format. So far we only provide the command line tool
cnf2kcnf
which transforms a CNF formula F into a k-CNF formula Fₖ which is satisfiable if and only if F was. The transformation goes along the following lines (the example is for k = 4): consider a clause of F,
x₁ v x₂ v x₃ v x₄ v x₅.
This becomes
y₀ ∧ (¬y₀ v x₁ v x₂ v y₁) ∧ (¬y₁ v x₃ v x₄ v y₂) ∧ (¬y₂ v x₅ v y₂) ∧ ¬y₃
where {yᵢ} are new extension variables.
Anyone can use this software of course! But the main target is the community of SAT solver programmers, who may want to test they solvers on canonical families of formulas. Proof complexity researcher may be interested to, since they study the computational complexity of proving that a CNF formula is unsatisfiable.
cnf2kcnf reads a dimacs file from standard input and outputs the
translated formula to the standard output. For example
cnf2kcnf < formula.cnf > translation3cnf.cnf
converts the CNF in the file formula.cnf into a 3-CNF which is
saved to translation3cnf.cnf.
To convert the formula to k-CNF for k≠3, use the option [-k]
where k is an (single digit, sorry) number. For example
cnf2kcnf -5 < formula.cnf > translation5cnf.cnf
gives you a 5-CNF. For more information type
cnf2kcnf -h
To compile the code you need a C++ compiler which supports C++11
standard. With GNU C++ compiler and make utility installed, it
is sufficient to type
make
to build the software. If you have C++ Unit installed then typing
make test
will build and run a test suite.
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 … v lₖ
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₂ ∧ … ∧ 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.
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₄.