Proceedings

A Modularity-Based Random SAT Instances Generator

Jesús Giráldez-Cru, Jordi Levy

Download BibTeX Cite

Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence. Main Track. Pages 1952-1957.

Abstract

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.

Jesús Giráldez-Cru, and Jordi Levy. 2015. A Modularity-Based Random SAT Instances Generator. In Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI-15. IJCAI, 1952–1957. https://ijcai.org/proceedings/2015/277
Welcome Future Conferences AI Journal Division IJCAI Proceedings About IJCAI IJCAI Awards