SAT evolution

In a recent article on satisfiability problems1 the authors divide their development into three eras: The pre-revolution era with techniques like unit propagation, backtracking; the revolution era with conflict driven clause learning and the trail data structure; the evolution era with more efficient encodings and new techniques like assumptions or incremental processing.

As a quick reminder, a propositional satisfiability problem (SAT) asks wether a propositional formula is satisfiable: Is there an assignment of boolean variables that makes the whole formula true?

The success of SAT solving techniques is not solely due to improvements in the underlying compute hardware as nicely shown in the Time Leap Challenge2, where modern SAT solvers on old hardware were pitched against old SAT solvers on modern hardware.

References

  1. Johannes K. Fichte, Daniel Le Berre, Markus Hecher, and Stefan Szeider. 2023. The Silent (R)evolution of SAT. Commun. ACM 66, 6 (June 2023), 64–72. https://doi.org/10.1145/3560469
  2. Johannes K. Fichte, Markus Hecher, and Stefan Szeider. 2020. A Time Leap Challenge for SAT-Solving. In Principles and Practice of Constraint Programming: 26th International Conference, CP 2020, Louvain-la-Neuve, Belgium, September 7–11, 2020, Proceedings. Springer-Verlag, Berlin, Heidelberg, 267–285. https://doi.org/10.1007/978-3-030-58475-7_16