Guillaume Baud-Berthier, Jesus Giráldez-Cru, Laurent Simon

On the community structure of Bounded Model Checking SAT problems

SAT 2017

Following the impressive progress made in the quest for efficient SAT solving in the last years, a number of researches has focused on explaining performances observed on typical applications. However, until now, tentative explanations were only partial, essentially because the semantic of the original problem was lost in the translation to SAT.

In this work, we study the behavior of so called "modern" SAT solvers under the prism of the first successful application of CDCL solvers, i.e., Bounded Model Checking. We trace the origin of each variable w.r.t. its unrolling depth, and show a surprising relationship between these timesteps and the communities found in the CNF encoding. We also show how the VSIDS heuristic, the resolution engine, and the learning mechanism interact with the unrolling steps. Additionally, we show that the Literal Block Distance (LBD), used to identify good learnt clauses, is related to this measure.

Our work shows that communities identify strong dependencies among the variables of different timesteps, revealing a structure that arises when unrolling the problem, and which is probably caught by the LBD measure.