Generating difficult CNF instances in unexplored constrainedness regions
Loading...
Files
Accepted Version
Date
2020-04-01
Authors
Escamocher, Guillaume
O'Sullivan, Barry
Prestwich, Steven D.
Journal Title
Journal ISSN
Volume Title
Publisher
Association for Computing Machinery (ACM)
Published Version
Abstract
When creating benchmarks for satisfiability (SAT) solvers, we need Conjunctive Normal Form (CNF) instances that are easy to build but hard to solve. A recent development in the search for such methods has led to the Balanced SAT algorithm, which can create k-CNF instances with m clauses of high difficulty, for arbitrary k and m. In this article, we introduce the No-Triangle CNF algorithm, a CNF instance generator based on the cluster coefficient graph statistic. We empirically compare the two algorithms by fixing the arity and the number of variables, but varying the number of clauses. We find that the hardest instances produced by each method belong to different constrainedness regions. In the 3-CNF case, for example, hard No-Triangle CNF instances reside in the highly-constrained region (many clauses), while Balanced SAT instances obtained from the same parameters are easy to solve. This allows us to generate difficult instances where existing algorithms fail to do so.
Description
Keywords
Constrainedness region , Constraint satisfaction , Instance difficulty , Instance generator
Citation
Escamocher, G., O'Sullivan, B. and Prestwich, S. D. (2020) 'Generating difficult CNF instances in unexplored constrainedness regions', ACM Journal of Experimental Algorithmics, 25, 1.6 (12pp). doi: 10.1145/3385651
Link to publisher’s version
Copyright
© 2020, Association for Computing Machinery. This is the author's version of the work. It is posted here for your personal use. Not for redistribution. The definitive Version of Record was published in ACM Journal of Experimental Algorithmics, https://doi.org/10.1145/3385651