# CNFgen

# CNFgen

## Combinatorial benchmarks for SAT solvers

*CNFgen* produces benchmark propositional formulas in DIMACS format,
ready to be fed to SAT solvers. These benchmarks come mostly from
research in Proof Complexity (e.g. pigeonhole principle, ordering
principle, k-clique, …). Many of these formulas encode structured
combinatorial problems well known to be challenging for certain
SAT solvers.

### Features

`cnfgen`

generator for CNF formula benchmarks,- several formula families (a list here)
- several formula transformations (a list here)
- output in DIMACS and LaTeX formats,
- behind-the-scene integration with many SAT solvers,
- the
`cnfgen`

python library (read the docs) for more flexible CNF generation and manipulation, - CNF based on graph structures (see the supported graph formats).

### Installation

You can install CNFgen from Python Package Index, together with all its dependencies, typing either

pip3 install [--user] cnfgen

or

python3 -m pip install [--user] cnfgen

if `pip3`

is not a program on your path. Otherwise it is possible
to install from source, assuming the requirements are already
installed, using

python3 setup.py install [--user]

The `--user`

option allows to install the package in the user home
directory. If you do that please check that the target location for
the command line utilities are in your $PATH.

### Quickstart

In most cases it is sufficient to invoke `cnfgen`

giving the name
of the formula family and the corresponding parameters.

cnfgen <formula> <param1> <param2> ...

For example

cnfgen php 10 7

gives the Pigeonhole Principle from 10 pigeons and 7 holes. To get more help you can type

cnfgen --help # available formulas / help for the tool cnfgen <formula> --help # help about a specific formula cnfgen --tutorial # a quick tutorial

Here's how to generate a formula encoding the Graph ordering principle on a random regular graph with 10 vertices and degree 3.

cnfgen op 10 3

or a formula claiming the 3-colorability formula of a 15 by 15 grid graph.

cnfgen kcolor 3 grid 15 15

In the next example we generate the formula that claims the graph isomorphism between (1) the bidimensional torus of 3x1 and (2) the complete graph over three vertices. This formula is clearly satisfiable.

cnfgen iso torus 3 1 -e complete 3

Some formulas require input graph(s), and the `cnfgen`

tool
supports several graph file formats. For example

cnfgen kclique 5 largegraph.gml

encodes in DIMACS the problem of searching a clique of size 5 in
the graph encoded in file `largegraph.gml`

. In general there are
various formulas generator that need either a simple graph,
a directed acyclic graph, or a bipartite graph specified on the
command line. See

cnfgen --help-graph cnfgen --help-dag cnfgen --help-bipartite

### Lifting/transformations/post-processing

CNFgen can apply one or more transformations to the formula by appending one or more transformation descriptions to the command line. For example

cnfgen op 15 -T shuffle

produces the ordering principle formula on 15 elements, with a random shuffle of variables, polarities and clauses. Or for example

cnfgen php 5 4 -T xor 2

substitute all variables in the pigeohole principle formula with the XOR of 2 fresh variable.

cnfgen --help

For more information check out transformations.

### Acknowledgments

The CNFgen project is by Massimo Lauria (massimo.lauria@uniroma1.it), with helps and contributions by Marc Vinyals, Jan Elffers, Mladen Mikša and Jakob Nordström. Special thanks to Adam Lugowski who helped updateing the codebase to work on Python 3 and NetworkX 2.

A large part of the initial work has been funded by

- [2016-2017] The European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme (grant agreement ERC-2014-CoG 648276 AUTAR)
- [2012-2015] The European Research Council under the European Union's Seventh Framework Programme (FP7/2007–2013) ERC grant agreement no. 279611.