Jesús Giráldez Crú: The notion of structure in real-world SAT solving

Practicalities

Lunch is served at 12:00 noon (register at this doodle at the latest on Tuesday May 5). The presentation starts at 12:10 pm and ends at 1 pm. Those of us who wish reconvene after a short break for ca two hours of more technical discussions.

Abstract:

Modern SAT solvers have experienced a remarkable progress on solving industrial (or real-world) SAT instances. Most of the techniques have been developed after an intensive experimental testing process. The common wisdom in the SAT community is that the success of these techniques is because they exploit some kind of hidden structure that industrial formulas actually have. Recently, there have been some attempts to analyze this structure in terms of complex networks, with the long-term aim of explaining the success of these
SAT solving techniques, and possibly improving them.

In this talk, we analyze some structural properties of SAT instances, viewed as graphs. Namely, the scale-free structure, the community structure and the self-similar structure. In addition, we explore how these features are affected during the SAT solving search by effects of variable instantiation or clause learning. Finally, we present some applications in SAT based on these notions of structure.