Generating difficult CNF instances in unexplored constrainedness regions

Simple item page
dc.contributor.authorEscamocher, Guillaume
dc.contributor.authorO'Sullivan, Barry
dc.contributor.authorPrestwich, Steven D.
dc.contributor.funderScience Foundation Irelanden
dc.contributor.funderEuropean Regional Development Funden
dc.date.accessioned2021-01-22T12:30:05Z
dc.date.available2021-01-22T12:30:05Z
dc.date.issued2020-04-01
dc.date.updated2021-01-22T12:06:59Z
dc.description.abstractWhen 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.en
dc.description.sponsorshipScience Foundation Ireland (Grant No. 12/RC/2289-P2)en
dc.description.statusPeer revieweden
dc.description.versionAccepted Versionen
dc.format.mimetypeapplication/pdfen
dc.identifier.articleid1.6en
dc.identifier.citationEscamocher, 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/3385651en
dc.identifier.doi10.1145/3385651en
dc.identifier.eissn1084-6654
dc.identifier.endpage12en
dc.identifier.journaltitleACM Journal of Experimental Algorithmicsen
dc.identifier.startpage1en
dc.identifier.urihttps://hdl.handle.net/10468/10952
dc.identifier.volume25en
dc.language.isoenen
dc.publisherAssociation for Computing Machinery (ACM)en
dc.rights© 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/3385651en
dc.subjectConstrainedness regionen
dc.subjectConstraint satisfactionen
dc.subjectInstance difficultyen
dc.subjectInstance generatoren
dc.titleGenerating difficult CNF instances in unexplored constrainedness regionsen
dc.typeArticle (peer-reviewed)en
Files
Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
accepted.pdf
Size:
718.51 KB
Format:
Adobe Portable Document Format
Description:
Accepted Version
Download
License bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
license.txt
Size:
2.71 KB
Format:
Item-specific license agreed upon to submission
Description:
Download
Collections
Insight Centre for Data Analytics - Journal Articles
Computer Science - Journal Articles