A Modularity-Based Random SAT Instances Generator / 1952
Jesús Giráldez-Cru, Jordi Levy
PDF

Nowadays, many industrial SAT instances can be solved efficiently by modern SAT solvers. However, the number of real-world instances is finite. Therefore, the process of development and test of SAT solving techniques can benefit of new models of random formulas that capture more realistically the features of real-world problems. In many works, the structure of industrial instances has been analyzed representing them as graphs and studying some of their properties, like modularity. In this paper, we use modularity, or community structure, to define a new model of pseudo-industrial random SAT instances, called Community Attachment. We prove that the phase transition point, if exists, is independent on the modularity. We evaluate the adequacy of this model to real industrial problems in terms of SAT solvers performance, and show that modern solvers do actually exploit this community structure.