Abstract
Topics:
Jordi Levy: On the Formal Characterization of Industrial SAT Instances
Abstract: Over the last 20 years, SAT solvers have experienced a great improvement in their efficiency when solving practical or industrial SAT problems. This success is surprising, considering that SAT is an NP-complete problem. Over the years, the particular structure of industrial instances has been proposed, informally, as a reason. This has led, for instance, the organizers of the SAT competition to distinguish two tracks, random and industrial, and solvers wining in one track have a poor performance on the other, and vice versa. We think that a better characterization of this structure may be decisive in future improvements of practical SAT solving.
During my talk, I'll start revisiting the notions that try to characterize how difficult is to be solved a SAT instance in practice, especially, the notion of "hardness" or tree-like space resolution. I'll discuss some properties that are shared by most industrial SAT instances used in the SAT competition, such as scale-free structure, high modularity, and low fractal dimension, and how these features may influence the performance of practical SAT solvers. I'll finish introducing some models of random SAT instances that try to reproduce these characteristics.
Stefan Szeidar: Algorithmic utilization of structure in SAT instances
Abstract: In this talk, I will survey various concepts that have been proposed to capture the hidden structure in SAT instances. I will focus on concepts that provide worst-case runtime guarantees for SAT algorithms and discuss a suitable theoretical framework. I will also discuss how these concepts relate to each other and propose questions for further research.
Some of the talk's content is covered by the extended and updated Chapter 17, Fixed-Parameter Tractability, of the Handbook of Satisfiability, 2nd edition, 2021.
Ralf Rothenberger: Structural Parameters - Heterogeneity and Geometry
Abstract: Two characteristic properties seem to be prevalent in the majority of real-world SAT instances, heterogeneous degree distribution and locality. In this talk I present our most recent results trying to understand the impact of these two properties on SAT by studying the resolution proof size of random k-SAT models that allow to control heterogeneity and locality.