| Summary: | The propositional satisfiability problem (SAT) was the first problem 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, the SAT problem has emerged as an essential tool 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 by orders of magnitudes ahead. Today, the many flavors of SAT technology can be found in all areas of technological innovation.
|
|---|