The purpose of this workshop is to explore one of the most important problems in all of mathematics and computer science, namely, the Boolean satisfiability problem. While Boolean satisfiability is the quintessential NP-complete problem, believed to be intractable in general, the last two decades have seen dramatic developments in algorithmic techniques in solving it. These techniques, often referred to as conflict-driven clause-learning (CDCL) SAT solving, routinely solve large real-world instances obtained from wide-ranging applications such as hardware and software verification, electronic design automation, artificial intelligence, bioinformatics, and operations research, just to name a few examples.

A surprising aspect of this development is that the state-of-the-art CDCL SAT solvers can often handle real-world formulas with millions of variables and clauses, but may also get hopelessly stuck on formulas with just a few hundred variables. A fundamental question then is "why do CDCL SAT solvers perform as well as they do, and which underlying properties of Boolean formulas influence their performance the most?" Compounding the mystery is the curious phenomena that CDCL-based techniques are effective in solving large real-world instances from many other hard problem classes, such as the satisfiability problem for quantified Boolean logic which is PSPACE-complete. These questions remain poorly understood, and worst-case complexity analysis is not sufficient to answer it. We need a deeper mathematical understanding of the inner workings of CDCL SAT solvers, and ideas from parameterized and proof complexity theory to better characterize the classes of instances on which they scale well.

This workshop will gather leading researchers in applied and theoretical areas of SAT solving, logic, and computational complexity, to stimulate an exchange of ideas between these communities that may finally lead to a solution to this problem of "understanding the CDCL paradigm". We see great opportunities for fruitful interplay between theoretical and applied research at the proposed workshop. Such an organized event on a problem as fundamental as Boolean satisfiability, and heuristics to solve it, has the potential for major long-term impact in mathematics, theoretical computer science, and industry.

A tabular schedule for the workshop can be downloaded here.