6.5440 Algorithmic Lower Bounds: Fun with Hardness Proofs (Fall 2023)

Satisfiability, particularly 3SAT and its many variations, is the prototype NP-complete problem, forming the starting point for almost all NP-complete problems. This class gives an overview of all the important variations, particularly the NP-complete ones, but also some close cousins which are polynomially solvable (so no good for NP-completeness!).

Then we'll cover some examples of NP-hardness proofs based on 3SAT. First we'll look at pushing block puzzles popular in many video games (and with practical applications to warehouse motion planning). After introducing a variety of different such puzzles, such as Sokoban, we'll prove NP-hard Push-∗ and Push-1 and PushPush-1 (first in 3D, then in 2D). Finally, we'll cover Conway's Phutball (Philosopher's Football), where mate-in-1 is NP-hard, unlike Checkers where mate-in-1 is polynomial.