Understanding VSIDS Branching Heuristics in Conflict-Driven Clause-Learning SAT Solvers

TL;DR

This paper provides a detailed analysis of the VSIDS branching heuristic in SAT solvers, revealing its preference for high-centrality bridge variables and the role of decay, leading to an improved adaptive heuristic.

Contribution

It uncovers the structural properties of variables selected by VSIDS and introduces a new adaptive heuristic that outperforms existing variants.

Findings

VSIDS predominantly selects bridge variables connecting communities.

Multiplicative decay acts like an exponential moving average favoring persistent variables.

The new adaptive heuristic solves more instances than previous variants.

Abstract

Conflict-Driven Clause-Learning SAT solvers crucially depend on the Variable State Independent Decaying Sum (VSIDS) branching heuristic for their performance. Although VSIDS was proposed nearly fifteen years ago, and many other branching heuristics for SAT solving have since been proposed, VSIDS remains one of the most effective branching heuristics. In this paper, we advance our understanding of VSIDS by answering the following key questions. The first question we pose is "what is special about the class of variables that VSIDS chooses to additively bump?" In answering this question we showed that VSIDS overwhelmingly picks, bumps, and learns bridge variables, defined as the variables that connect distinct communities in the community structure of SAT instances. This is surprising since VSIDS was invented more than a decade before the link between community structure and SAT solver performance was discovered. Additionally, we show that VSIDS viewed as a ranking function correlates strongly with temporal graph centrality measures. Putting these two findings together, we conclude that VSIDS picks high-centrality bridge variables. The second question we pose is "what role does multiplicative decay play in making VSIDS so effective?" We show that the multiplicative decay behaves like an exponential moving average (EMA) that favors variables that persistently occur in conflicts (the signal) over variables that occur intermittently (the noise). The third question we pose is "whether VSIDS is temporally and spatially focused." We show that VSIDS disproportionately picks variables from a few communities unlike, say, the random branching heuristic. We put these findings together to invent a new adaptive VSIDS branching heuristic that solves more instances than one of the best-known VSIDS variants over the SAT Competition 2013 benchmarks.