On the community structure of SAT-BMC problems

A common belief says that modern SAT solvers are efficient because of their ability to exploit structural properties of industrial problems. However, we only have a limited understanding of what is covered by this ‘structure’. A recent hypothesis suggests the community structure as a candidate definition for that notion. Our paper proposes a tool helping to understand community structure of SAT instances generated by BMC