CNFgen: A generator of crafted benchmarks

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

*Corresponding author af dette arbejde

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningpeer review

30 Citationer (Scopus)

Abstract

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.

OriginalsprogEngelsk
TitelTheory and Applications of Satisfiability Testing – SAT 2017 - 20th International Conference, Proceedings
RedaktørerSerge Gaspers, Toby Walsh
Antal sider10
ForlagSpringer Verlag,
Publikationsdato2017
Sider464-473
ISBN (Trykt)9783319662626
DOI
StatusUdgivet - 2017
Udgivet eksterntJa
Begivenhed20th International Conference on Theory and Applications of Satisfiability Testing, SAT 2017 - Melbourne, Australien
Varighed: 28 aug. 20171 sep. 2017

Konference

Konference20th International Conference on Theory and Applications of Satisfiability Testing, SAT 2017
Land/OmrådeAustralien
ByMelbourne
Periode28/08/201701/09/2017
SponsorAssociation for Constraint Programming, Association for Logic Programming, CSIRO Data61, et al., Monash University, University of Melbourne
NavnLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Vol/bind10491 LNCS
ISSN0302-9743

Citationsformater