Jesús Giráldez Crú: Graph-based pseudo-industrial random SAT instance generators

PRACTICALITIES

Lunch is served at 12:00 noon (register at  this doodle  at the latest the Saturday before, but preferably earlier). The presentation starts at 12:10 pm and ends at 1 pm. Those of us who wish reconvene after a short break for 1½-2 hours of more technical discussions.

ABSTRACT

The Boolean Satisfiability problem (SAT) is the canonical NP-complete problem. However, Conflict-Driven Clause Learning (CDCL) SAT solvers are nowadays able to efficiently solve many industrial, or real-world, SAT instances -as hardware and software verification, cryptography, planning or scheduling, among others-. On the other hand, relatively small random SAT instances are still too hard. The common intuition to explain the success of CDCL solving industrial instances is the existence of some hidden structure in them (whereas random formulas would not show such structure). In some works, this structure is studied representing SAT instances as graphs and analyzing some graph features, showing that these features are shared by the majority of existing industrial SAT instances. Some examples are the scale-free structure or the community structure.

Unfortunately, the process of development and testing of new SAT solving techniques (specialized in industrial problems) is conditioned to the reduced number of existing industrial benchmarks. Therefore, the generation of random SAT instances that captures realistically some computational properties of such industrial instances is an interesting open problem.

In this talk, we review some models of pseudo-industrial random SAT instances generation. They are the scale-free model and the community attachment model, which are related to some well-known concepts in real-world complex networks: preferential attachment and high modularity, respectively. In the scale-free model, the number of variable occurrences k follows a power-law distribution P(k) \propto k^{-\alpha}. With the community attachment model, it is possible to generate SAT instances with clear community structure (i.e., high modularity). These models will be reviewed from the perspectives of both graphs and SAT instances. Finally, we discuss some models for generating complex networks -not adapted to SAT instances yet- that may reduce the limitations of the previous models.