Spring 2021

Theoretical Foundations of SAT/SMT Solving

(Weekly event) Feb 10, 2021 to May 12, 2021 (ended)View all dates

All scheduled dates:

  • Feb 10, 2021 (ended)
  • Feb 17, 2021 (ended)
  • Feb 24, 2021 (ended)
  • Mar 3, 2021 (ended)
  • Mar 10, 2021 (ended)
  • Mar 17, 2021 (ended)
  • Mar 24, 2021 (ended)
  • Mar 31, 2021 (ended)
  • Apr 7, 2021 (ended)
  • Apr 14, 2021 (ended)
  • Apr 21, 2021 (ended)
  • Apr 28, 2021 (ended)
  • May 5, 2021 (ended)
  • May 12, 2021 (ended)

Add to Calendar


Antonina Kolokolova (Memorial University of Newfoundland; co-chair), Moshe Vardi (Rice University; co-chair), María Luisa Bonet Carbonell (Universitat Politecnica de Catalunya), Vijay Ganesh (University of Waterloo), Marijn Heule (Carnegie Mellon University), Kevin Leyton-Brown (University of British Columbia)

This workshop is shared between the programs Satisfiability: Theory, Practice, and Beyond and Theoretical Foundations of Computer Systems.

Boolean satisfiability is a canonical hard problem: not only is it NP-complete, but we do not expect to have any algorithms for it that even slightly outperform exhaustive search in the worst case. Moreover, determining the satisfiability of certain simple formulas is provably hard for Resolution, the underlying proof system of most modern SAT solvers. This stands in stark contrast to the practical success of SAT solvers. Nowadays, they are used to solve industrial problems with millions of variables and tens of millions of clauses; the US Federal Communications Commission used SAT solvers to run its multibillion-dollar broadcast incentive auction. SAT solvers have been used to verify the London train system and schedule exams in large universities, and they are routinely used to verify large hardware subsystems. They have been used in proving combinatorial conjectures — for example, that it is possible to color the numbers 1 to 7,824 in two colors such that no Pythagorean triple of them consists of numbers of the same color, yet there is no such coloring for the numbers 1 to 7,825 — and there are combinatorial statements such as the Williamson conjecture that posits the existence of a certain special class of Hadamard matrices. Further, the architecture of conflict-driven clause-learning (CDCL) SAT solvers forms the basis of modern SMT solvers, a class of solvers for first-order theories critical to the success of many program analysis, testing, and verification methods.

This workshop will focus on the mystery of this drastic gap between the predicted theoretical hardness of SAT and related problems and the unreasonable success of heuristics on their practical instances. We expect the themes to range from the discussion of the special structure in practical instances and their distributions that might make them easier for heuristics, to theoretical characterizations of hard examples and complexity of restricted problems, to the interplay among the success of various solver heuristic types, properties of instances, and encoding strategies.

In response to the COVID-19 pandemic, Simons Institute events are currently taking place online. Please register to receive the Zoom webinar access details.

This workshop will take place every Wednesday from 8:30 a.m. - 10:30 a.m. (PST) starting February 10. 

If you require accommodation for communication, please contact our access coordinator at simonsevents [at] with as much advance notice as possible.

Further details about this workshop will be posted in due course. Enquiries may be sent to the organizers workshop-sat-tfcs [at] (at this address).

Invited Participants: 

Yehia Abd Alrahman (Gothenburg University), Parosh Abdulla (Uppsala University), Albert Atserias (Universitat Politècnica de Catalunya), Shaun Azzopardi (Gothenburg University), Paul Beame (University of Washington), Christoph Berkholz (Humboldt-Universität zu Berlin), Olaf Beyersdorff (Friedrich-Schiller University of Jena), Nikolaj Bjorner (Microsoft Research), Rastislav Bodik (University of Washington), Mikołaj Bojańczyk (University of Warsaw), Maria Paola Bonacina (Università degli Studi di Verona), María Luisa Bonet Carbonell (Universitat Politècnica de Catalunya), Ahmed Bouajjani (U. Paris 7), Samuel Buss (UC San Diego), Antonio Casares (Université de Bordeaux), Supratik Chakraborty (IIT Bombay), Norine Coenen (CISPA Helmholtz Center), Thomas Colcombet (Université Paris Diderot - Paris 7), Anuj Dawar (University of Cambridge), Rayna Vasileva Dimitrova (University of Sheffield), Javier Esparza (Technische Universität München), Kousha Etessami (University of Edinburgh), Azadeh Farzan (University of Toronto), Nathanaël Fijalkow (CNRS), Bernd Finkbeiner (Saarland University), Vijay Ganesh (University of Waterloo), Orna Grumberg (Technion), Jana Hoffmann (CISPA Helmholtz Center), Neil Immerman (University of Massachusetts Amherst), Russell Impagliazzo (UC San Diego), Arthur Jaquard (IRIF), Samuel Judson (Yale University), Marcin Jurdzinski (University of Warwick), Valentine Kabanets (Simon Fraser University), Bartosz Klin (University of Warsaw), Phokion Kolaitis (UC Santa Cruz), Antonina Kolokolova (Memorial University of Newfoundland), Alexander Kozachinskiy (University of Warwick), Jędrzej Kołodziejski (University of Warsaw), Oliver Kullmann (Swansea University), Viktor Kuncak (EPFL), Antonín Kučera (Masaryk University), Ratan Lal (Kansas State University), Ranko Lazic (University of Warwick, Department of Computer Science), Karoliina Lehtinen (University of Liverpool), Jorge Levy Diaz (Artificial Intelligence Research Institute, Spanish National Research Council), Anthony Lin (TU Kaiserslautern), Anna Lukina (Institute of Science and Technology Austria), Rupak Majumdar (Max Planck Institute for Software Systems; International Computer Science Institute), Susan Margulies (United States Naval Academy), Joao Marques-Silva (University of Toulouse), Mauricio Martel (Gothenburg University), Alexandra Martins da Silva (University College London), Umang Mathur (University of Illinois at Urbana-Champaign), Stanislav Mazurenko (Masaryk University), Ciaran McCreesh (University of Glasgow), Kuldeep Singh Meel (National University of Singapore), Niklas Metzger (CISPA Helmholtz Center), Yifei Min (Yale University), David Mitchell (Simon Fraser University), sayan mitra (University of Illinois at Urbana Champaign), Annielo Murano (University of Naples Federico II), Anca Muscholl (University of Bordeaux), Karl Jakob Nordström (University of Copenhagen & Lund University), Gethin Norman (University of Glasgow), Pierre Ohlmann (IRIF), Noemi Estrid Passing (CISPA Helmholtz Center), Ramamohan Paturi (UC San Diego), Vaidyanathan Peruvemba Ramaswamy (TU Wien), Ruzica Piskac (Yale University), Toniann Pitassi (University of Toronto), Nir Piterman (Gothenburg University), Pavithra Prabhakar (Kansas State University), Pavel Pudlák (Czech Academy of Sciences), Thejaswini Raghavan (University of Warwick), Barna Saha (UC San Diego), Karem Sakallah (University of Michigan), Rahul Santhanam (University of Oxford), Maximilian Schwenger (CISPA Helmholtz Center), Dana Scott (UC Berkeley & Carnegie Mellon University), Laurent Simon (Bordeaux INP), Rafał Stefański (University of Warsaw), Stefan Szeider (TU Wien), Ufuk Topcu (University of Texas at Austin), Szymon Toruńczyk (University of Warsaw), Marc Vinyals (Technion - Israel Institute of Technology), Igor Walukiewicz (University of Bordeaux), Thomas Wies (NYU), Ryan Williams (MIT), Richard Williams (Massachusetts Institute of Technology), Pavol Černý (TU Wien)