cnfgen
cnfgen copied to clipboard
MassimoLauria
CNF generator in DIMACS format. It produces common families of CNFs.
Since `cnfgen` has the ability to take graphs as input, I think it would be possible for it to generate CNFs for Hamiltonian Paths and Hamiltonian Cycles. Here is a...
During a workshop in Toronto: Theoretical Foundation of SAT Solving 2016, Moshe Vardi suggested to implement some scalable benchmarks from See http://www.cs.rice.edu/~vardi/papers/sat04rj.pdf
Should we allow multigraphs as input for Tseitin formulas? Currently we do not, but the only (technical) reason is that we do not know how to label multiedges. I do...
Implements the changes suggested in #113. OPB instances have another member `_objective` which is just a list of pairs (coefficient, literal).
Metadata
Owner
Metadata
CNF generator in DIMACS format. It produces common families of CNFs.