A collection of tools for working with and generating Dimacs CNF files.
pip install cnftools
cnftools is listed in PyPI and
can be installed with pip.
cnftools exposes the cnf command-line interface for quickly generating
Dimacs CNF files typically for use with a SAT solver.
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]
Simply the input CNF file.
cnf simplify -i [input.cnf] -o [output.cnf]
Randomly reorder clauses, literals within clauses, and variable names.
cnf shuffle -i [input.cnf] -o [output.cnf] [-l/--literals] [-c/--clauses] [-v/--variables]
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]
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
| [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. |
| [ZUCK1996] | Zuckerman, David. "On unapproximable versions of NP-complete problems." SIAM Journal on Computing 25.6 (1996): 1293-1304. |