A theoretical analysis of the k-satisfiability search space

Abstract

Local search algorithms perform surprisingly well on the k-satisfiability (k-SAT) problem. However, few theoretical analyses of the k-SAT search space exist. In this paper we study the search space of the k-SAT problem and show that it can be analyzed by a decomposition. In particular, we prove that the objective function can be represented as a superposition of exactly k elementary landscapes. We show that this decomposition allows us to immediately compute the expectation of the objective function evaluated across neighboring points. We use this result to prove previously unknown bounds for local maxima and plateau width in the 3-SAT search space. We compute these bounds numerically for a number of instances and show that they are non-trivial across a large set of benchmarks.