Evolving difficult SAT instances thanks to local search

TL;DR

This paper introduces a method using local search algorithms to generate challenging SAT instances, aiming to test solver robustness and understand solver behavior better.

Contribution

It presents a novel approach to create difficult SAT instances through local search, providing a new tool for evaluating and analyzing SAT solver performance.

Findings

Initial results show the approach can produce harder SAT instances than random ones.

The method offers potential for testing solver robustness and analyzing solver strategies.

Further research is needed to refine the technique and explore its full capabilities.

Abstract

We propose to use local search algorithms to produce SAT instances which are harder to solve than randomly generated k-CNF formulae. The first results, obtained with rudimentary search algorithms, show that the approach deserves further study. It could be used as a test of robustness for SAT solvers, and could help to investigate how branching heuristics, learning strategies, and other aspects of solvers impact there robustness.