Theoretical Foundations of Applied SAT Solving (14w5101)

Arriving in Banff, Alberta Sunday, January 19 and departing Friday January 24, 2014

Organizers

(Universitat Politecnica de Catalunya)

(Johannes Kepler University)

(University of California, San Diego)

(Memorial University of Newfoundland)

(KTH Royal Institute of Technology)

(University of Michigan)

Description

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).