Theory and Practice of SAT and Combinatorial Solving (26w5626)

The Banff International Research Station will host the "Theory and Practice of SAT and Combinatorial Solving" workshop in Banff from January 11 - 16, 2026.

How hard is it to figure out if there is a way to make a set of logical statements true at the same time by choosing appropriate truth values for their variables?
This satisfiability problem is of immense importance both theoretically and practically, and lies right at the heart of mathematics and computer science. On the one hand, today so-called
Boolean satisfiability (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.

This workshop will bring together leading experts from both theory and practice on SAT solving, as well as representatives from neighbouring areas such as, e.g., SAT-based optimization, pseudo-Boolean optimization, constraint programming, satisfiability modulo theories solving, mixed integer linear programming, and automated planning on the applied side, and from other areas of computational complexity theory such as exact exponential-time algorithms and parameterized complexity on the theoretical side, to foster collaboration between these communities. We see great opportunities for fruitful interplay between theoretical and applied research in this area, and believe that a more vigorous interaction 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), and Alberta's Advanced Education and Technology.