• Participants :
  • Johannes K. Fichte
  • Daniel Le Berre
  • Markus Hecher
  • Stefan Szeider

This is a video promoting an article of the same name by Johannes K. Fichte, Daniel Le Berre, Markus Hecher, and Stefan Szeider published in Communications of the ACM, June 2023, Vol. 66 No. 6, Pages 64-72 10.1145/3560469.

The propositional satisfiability problem (SAT) was the first to be shown NP-complete by Cook and Levin. SAT remained the embodiment of theoretical worst-case hardness. However, in stark contrast to its theoretical hardness, SAT has emerged as a central target problem for efficiently solving a wide variety of computational problems. SAT solving technology has continuously advanced since a breakthrough around the millennium, which catapulted practical SAT solving ahead by orders of magnitudes. Today, the many flavors of SAT technology can be found in all areas of technological innovation.