CNFgen formula generator

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.

Homepage of the project at http://massimolauria.net/cnfgen/

Basic usage

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

Lifting/transformations/post-processing

It is possible to apply one or more transformations to the formula by appending one or more -T <transformation> <params> 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. To list the available transformations you can use

cnfgen --help

Installation

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

pip3 install [--user] cnfgen

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.