Corelab Seminar

Fotis Iliopoulos (NTUA)
Local Search Algorithms inspired by the Lovasz Local Lemma

For a CNF formula $F$ with $n$ variables, let $E: \{0,1\}^n \to \mathbf{N}$ be the (energy) function counting the number of violated clauses at each value assignment. A number of practically useful satisfiability algorithms start at a random $\sigma \in \{0,1\}^n$ and, while violated clauses exist, employ a randomized process to select a violated clause $c$ and new values for its variables, leading to a new state $\tau$. For both the choice of $c$ and the choice of values for its variables there exists a cornucopia of heuristics, but not much to distinguish between them besides experiments, the systematic conduct of which forms an entire subarea of satisfiability research. One property that is shared by the vast majority of these heuristics is that they are primarily guided by the new number of violated clauses, $E(\tau)$, i.e., they largely focus on the energetic potential near the current truth assignment $\sigma$.

Inspired by Moser's~\cite{moser} groundbreaking algorithmic argument for the Lov\'{a}sz Local Lemma we show that there is an alternative \emph{entropic} potential to consider that lends itself to rigorous mathematical analysis. Focusing on this potential suggests a systematic methodology for designing algorithms for any discrete-valued CSP, while also elucidating why certain existing heuristics perform as well as they do. For example, our work suggests an explanation for the following, rather surprising, experimental finding of Balint and Sch\"{o}ning~\cite{balint}: in choosing new values for $c$ one should focus on minimizing the number of clauses that will become unsatisfied, ignoring the clauses that will become satisfied. We also derive new positive algorithmic results, in the style of the Lov\'{a}sz Local Lemma, for formulas in which clauses share multiple variables or have local neighborhoods that are not locally tree-like.