Theoretical Foundations of Applied SAT Solving

The Banff International Research Station will host the "Theoretical Foundations of Applied SAT Solving" workshop from January 19th to January 24th, 2014.

How hard is it to prove a logic formula? This is a problem of immense importance both theoretically and practically, which lies right at the heart of mathematics and computer science. On the one hand, today so-called SAT solvers are routinely and successfully used to solve large-scale real-world instances in a wide range of application areas (such as hardware and software verification, electronic design automation, artificial intelligence research, cryptography, bioinformatics, operations research, and railway signalling systems, just to name a few examples). On the other hand, this problem is believed to be intractable in general, and deciding whether this is so is one of the famous million dollar Clay Millennium Problems (the P vs. NP problem). Indeed, even for the very best SAT solvers today there are known tiny formulas that cause the solvers to stumble.

In this workshop, we aim to gather leading theoreticians and practitioners to stimulate an increased exchange of ideas between these two communities. We see great opportunities for fruitful interplay between theoretical and applied research in this area, and believe that a more vigorous interaction between the two has potential for major long-term impact in computer science and mathematics, as well for applications in industry.

The Banff International Research Station for Mathematical Innovation and Discovery (BIRS) is a collaborative Canada-US-Mexico venture that provides an environment for creative interaction as well as the exchange of ideas, knowledge, and methods within the Mathematical Sciences, with related disciplines and with industry. The research station is located at The Banff Centre in Alberta and is supported by Canada's Natural Science and Engineering Research Council (NSERC), the U.S. National Science Foundation (NSF), Alberta's Advanced Education and Technology, and Mexico's Consejo Nacional de Ciencia y Tecnología (CONACYT).

BIRS Scientific Director, Nassif Ghoussoub
E-mail: birs-director[@]birs.ca
http://www.birs.ca/~nassif