Skip to main content

A collection of tools for working with and generating Dimacs CNF files.

Project description

https://circleci.com/gh/easyas314159/cnftools/tree/master.svg?style=svg

A collection of tools for working with and generating Dimacs CNF files.

Installation

pip install cnftools

cnftools is listed in PyPI and can be installed with pip.

Usage

cnftools exposes the cnf command-line interface for quickly generating Dimacs CNF files typically for use with a SAT solver.

3cnf

Apply the Tseytin transformation [TSEY1970] to a CNF file producing an output where all clauses contain 3 or fewer literals.

cnf 3cnf -i [input.cnf]

simplify

Simply the input CNF file.

cnf simplify -i [input.cnf] -o [output.cnf]

stats

Provide details about contents of a CNF file. This includes the number of literals, the total number of clauses, as well as a histogram of clause lengths.

cnf stats -i [input.cnf]

karps21

This sub-command exposes utilities for generating CNF files based on Karp’s 21 NP-Complete problems [KARP1972]. For more details on this utility use the -h/--help option.

cnf karps21 --help

References

[TSEY1970]Tseitin, Grigori. “On the complexity of derivation in propositional calculus.” Studies in constructive mathematics and mathematical logic (1968): 115-125.
[COOK1971]Cook, Stephen A. “The complexity of theorem-proving procedures.” Proceedings of the third annual ACM symposium on Theory of computing. ACM, 1971.
[KARP1972]Karp, Richard M. “Reducibility among combinatorial problems.” Complexity of computer computations. Springer, Boston, MA, 1972. 85-103.

Project details


Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Files for cnftools, version 0.0.2
Filename, size File type Python version Upload date Hashes
Filename, size cnftools-0.0.2-py3-none-any.whl (14.4 kB) File type Wheel Python version py3 Upload date Hashes View hashes
Filename, size cnftools-0.0.2.tar.gz (10.3 kB) File type Source Python version None Upload date Hashes View hashes

Supported by

Elastic Elastic Search Pingdom Pingdom Monitoring Google Google BigQuery Sentry Sentry Error logging AWS AWS Cloud computing DataDog DataDog Monitoring Fastly Fastly CDN SignalFx SignalFx Supporter DigiCert DigiCert EV certificate StatusPage StatusPage Status page