Theory and Practice of Satisfiability Solving (18w5208)

The Casa Matemática Oaxaca (CMO) will host the "Theory and Practice of Satisfiability Solving" workshop from August 26th to August 31st, 2018.

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 formulas in a wide range of application areas (such as hardware and software verification, electronic design automation, artificial intelligence research, cryptography, bioinformatics, operations research, and sometimes even pure mathematics). On the other hand, this problem is believed to be intractable in general---though proving that this is so is so is one of the famous million dollar Clay Millennium Problems (the P vs. NP problem)---and there are tiny formulas for which even the very best SAT solvers today fail miserably.

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 Casa Matemática Oaxaca (CMO) in Mexico, and the Banff International Research Station for Mathematical Innovation and Discovery (BIRS) in Banff, are collaborative Canada-US-Mexico ventures that provide 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 in Banff 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). The research station in Oaxaca is funded by CONACYT.