cnftools 0.0.2

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

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.