CNFgen: A generator of crafted benchmarks

Massimo Lauria, Jan Elffers, Jakob Nordström, Marc Vinyals

Forskningsoutput: Kapitel i bok/rapport/Conference proceedingKonferenspaper i proceedingPeer review

Sammanfattning

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.

Originalspråkengelska
Titel på värdpublikationTheory and Applications of Satisfiability Testing – SAT 2017
Undertitel på värdpublikation20th International Conference, Proceedings
RedaktörerSerge Gaspers, Toby Walsh
FörlagSpringer
Sidor464-473
Antal sidor10
ISBN (tryckt)9783319662626
DOI
StatusPublished - 2017
Externt publiceradJa
Evenemang20th International Conference on Theory and Applications of Satisfiability Testing, SAT 2017 - Melbourne, Australien
Varaktighet: 2017 aug. 282017 sep. 1

Publikationsserier

NamnLecture Notes in Computer Science
FörlagSpringer
Volym10491
ISSN (tryckt)0302-9743
ISSN (elektroniskt)1611-3349

Konferens

Konferens20th International Conference on Theory and Applications of Satisfiability Testing, SAT 2017
Land/TerritoriumAustralien
OrtMelbourne
Period2017/08/282017/09/01

Ämnesklassifikation (UKÄ)

  • Datavetenskap (datalogi)

Fingeravtryck

Utforska forskningsämnen för ”CNFgen: A generator of crafted benchmarks”. Tillsammans bildar de ett unikt fingeravtryck.

Citera det här