We present CNFgen, a generator of combinatorial benchmarks in DIMACS and OPB format. The proof complexity literature is a rich source not only of hard instances but also of instances that are theoretically easy but “extremal” in different ways, and therefore of potential interest in the context of SAT solving. Since most of these formulas appear not to be very well known in the SAT community, however, we propose CNFgen as a resource to make them readily available for solver development and evaluation. Many formulas studied in proof complexity are based on graphs, and CNFgen is also able to generate, parse and do basic manipulation of such objects. Furthermore, it includes a library cnfformula giving access to the functionality of CNFgen to Python programs.
CITATION STYLE
Lauria, M., Elffers, J., Nordström, J., & Vinyals, M. (2017). CNFgen: A generator of crafted benchmarks. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10491 LNCS, pp. 464–473). Springer Verlag. https://doi.org/10.1007/978-3-319-66263-3_30
Mendeley helps you to discover research relevant for your work.