CNFgen : A generator of crafted benchmarks
(2017) 20th International Conference on Theory and Applications of Satisfiability Testing, SAT 2017 In Lecture Notes in Computer Science 10491. p.464-473- 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... (More)
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.
(Less)
- author
- Lauria, Massimo ; Elffers, Jan LU ; Nordström, Jakob LU and Vinyals, Marc
- publishing date
- 2017
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- host publication
- Theory and Applications of Satisfiability Testing – SAT 2017 : 20th International Conference, Proceedings - 20th International Conference, Proceedings
- series title
- Lecture Notes in Computer Science
- editor
- Gaspers, Serge and Walsh, Toby
- volume
- 10491
- pages
- 10 pages
- publisher
- Springer
- conference name
- 20th International Conference on Theory and Applications of Satisfiability Testing, SAT 2017
- conference location
- Melbourne, Australia
- conference dates
- 2017-08-28 - 2017-09-01
- external identifiers
-
- scopus:85028695687
- ISSN
- 0302-9743
- 1611-3349
- ISBN
- 9783319662626
- DOI
- 10.1007/978-3-319-66263-3_30
- language
- English
- LU publication?
- no
- id
- 077a280a-1a31-4680-8f2f-a77e2e8cecda
- date added to LUP
- 2020-12-18 22:20:23
- date last changed
- 2024-05-30 03:02:48
@inproceedings{077a280a-1a31-4680-8f2f-a77e2e8cecda,
abstract = {{<p>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.</p>}},
author = {{Lauria, Massimo and Elffers, Jan and Nordström, Jakob and Vinyals, Marc}},
booktitle = {{Theory and Applications of Satisfiability Testing – SAT 2017 : 20th International Conference, Proceedings}},
editor = {{Gaspers, Serge and Walsh, Toby}},
isbn = {{9783319662626}},
issn = {{0302-9743}},
language = {{eng}},
pages = {{464--473}},
publisher = {{Springer}},
series = {{Lecture Notes in Computer Science}},
title = {{CNFgen : A generator of crafted benchmarks}},
url = {{http://dx.doi.org/10.1007/978-3-319-66263-3_30}},
doi = {{10.1007/978-3-319-66263-3_30}},
volume = {{10491}},
year = {{2017}},
}