Generating Difficult SAT Instances by Preventing Triangles

TL;DR

This paper introduces the No-Triangle SAT algorithm, a new method for generating challenging SAT instances based on graph cluster coefficients, which outperforms the existing Balanced SAT algorithm in producing difficult benchmarks.

Contribution

The paper presents the No-Triangle SAT algorithm, a novel approach leveraging graph cluster coefficients to generate harder SAT instances, expanding the toolkit for benchmarking SAT solvers.

Findings

No-Triangle SAT produces more difficult SAT instances than Balanced SAT.

Difficult instances from No-Triangle SAT have different clause counts, enabling diverse benchmark creation.

The combination of both algorithms can generate a wider range of hard SAT instances.

Abstract

When creating benchmarks for SAT solvers, we need SAT 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-SAT instances with m clauses of high difficulty, for arbitrary k and m. In this paper we introduce the No-Triangle SAT algorithm, a SAT 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. The hardest instances that we find are produced by No-Triangle SAT. Furthermore, difficult instances from No-Triangle SAT have a different number of clauses than difficult instances from Balanced SAT, potentially allowing a combination of the two methods to find hard SAT instances for a larger array of parameters.