You are here

Generating Difficult CNF Instances in Unexplored Constrainedness Regions

Publication Type: 
Refereed Original Article
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.
Digital Object Identifer (DOI): 
10.1145/3385651
Publication Status: 
Published
Date Accepted for Publication: 
Monday, 24 February, 2020
Publication Date: 
01/11/2020
Journal: 
ACM Journal of Experimental Algorithmics
Volume: 
25
Institution: 
National University of Ireland, Cork (UCC)
Open access repository: 
Yes
Publication document: