Using Algorithm Configuration Tools to Generate Hard SAT Benchmarks

Abstract

Algorithm configuration tools have been successfully used to speed up local search satisfiability (SAT) solvers and other search algorithms by orders of magnitude. In this paper, we show that such tools are also very useful for generating hard SAT formulas with a planted solution, which is useful for benchmarking SAT solving algorithms and also has cryptographic applications. Our experiments with state-of-the-art local search SAT solvers show that by using this approach we can randomly generate satisfiable formulas that are considerably harder than uniform random formulas of the same size from the phase-transition region or formulas generated by state-of-the-art approaches. Additionally, we show how to generate small satisfiable formulas that are hard to solve by CDCL solvers.