Cnfgen

#+LANGUAGE: en #+OPTIONS: H:2 num:nil toc:nil \n:nil @:t ::t |:t ^:t f:t TeX:t

• CNFgen formula generator

#+begin_html <a href='https://travis-ci.com/github/MassimoLauria/cnfgen'> <img src='https://app.travis-ci.com/github/MassimoLauria/cnfgen.svg?branch=master' alt='Build Status' /> </a> <a href='http://cnfgen.readthedocs.org/en/latest/?badge=latest'> <img src='http://readthedocs.org/projects/cnfgen/badge/?version=latest' alt='Documentation Status' /> </a> <a href="https://zenodo.org/badge/latestdoi/6294497"> <img src="https://zenodo.org/badge/6294497.svg" alt="DOI" /> </a> #+end_html

/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 [[http://pypi.python.org][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.

** Resources

• 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

** Contribution

Please contribute to the code by sending pull requests.

Copyright 2012-2025 © Massimo Lauria ([[mailto:massimo.lauria@uniroma1.it][massimo.lauria@uniroma1.it]])