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/

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 

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

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.

• Webpage of the project at http://massimolauria.net/cnfgen/
• Technical documentation https://cnfgen.readthedocs.io/en/latest/
• Python Package at https://pypi.org/project/CNFgen/
• Github repository https://github.com/MassimoLauria/cnfgen
• Zenodo link (DOI) https://zenodo.org/record/3548843

Please contribute to the code by sending pull requests.

Copyright 2012-2021 © Massimo Lauria ([email protected])