A collection of tools for working with and generating Dimacs CNF files.
Project description
A collection of tools for working with and generating Dimacs CNF files.
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
Release history Release notifications | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
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 |
Filename, size cnftools-0.0.2.tar.gz (10.3 kB) | File type Source | Python version None | Upload date | Hashes View |