Generating Difficult SAT Instances by Preventing Triangles
  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.
