International Workshop on Graph Structure and Satisfiability Testing

Overview

A well-established way of describing the structure of SAT instances is to consider different graphs or hypergraphs that encode the interaction of the variables in CNF formulas. These graph structures have seen interest in the last few years both from theory and practice of SAT solving. For example, many tractable classes of SAT and related problems are characterized by restrictions of the underlying graph or hypergraph structure whereas lower bounds in proof complexity and knowledge compilation often use graphs that in a certain well-defined sense lack this structure. On the more practical side, it has been shown that good performance of CDCL solvers on practical SAT instances is related to the community structure of the underlying graphs. Moreover, graphs play a crucial role in some successful variable choice heuristics. Yet another connection between SAT and graph theory is the increasing use of SAT solvers in combinatorial problems, for instance in Ramsey theory.

The goal of the International Workshop on Graph Structure and Satisfiability Testing is to bring together researchers from different areas in which there is an interaction between graph structure and problems related to propositional satisfiability. The aim is to foster exchange between these areas by presenting different perspectives, results and current challenges.

The workshop will feature one 50-minute invited talk and several short contributed talks highlighting different perspectives.

Invited Speaker

Stefan Szeider (TU Wien)

Call

We solicit contributions in the form of 1-2-page extended abstracts concerned with all aspects of current research that relates graphs and SAT, interpreted in a broad sense. Since there will be no proceedings, we explicitly solicit the submission of talk abstracts describing already published work and work in progress which falls into the scope of our workshop.

The topics of interest include (but are not limited to) the following: