Learning, re-starting and other techniques of modern SAT solvers have been shown efficient when solving SAT instances from industr ial application. The ability to exploit the structure of these instances has been proposed as the respon- sible of such success. Here we study the modularity of some of these instances, used in the latest SAT competitions. Using a simple label propagation algorithm we show that the community structure of most of these SAT instances can be identified very efficiently. We also discuss how this structure may be use d to speed up SAT solvers.
['Carlos Ansótegui', 'Jordi Levy']
On the Modularity of Industrial SAT Instances