Generating difficult CNF instances in unexplored constrainedness regions

Thumbnail Image
accepted.pdf(718.51 KB)
Accepted Version
Escamocher, Guillaume
O'Sullivan, Barry
Prestwich, Steven D.
Journal Title
Journal ISSN
Volume Title
Association for Computing Machinery (ACM)
Published Version
Research Projects
Organizational Units
Journal Issue
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.
Constrainedness region , Constraint satisfaction , Instance difficulty , Instance generator
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
© 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,