SAT is hard, but there are algorithms that tend to do okay empirically. I recently learned about the Davis-Putnam-Logemann-Loveland (DPLL) procedure and rolled up a short Python implementation. (I can’t get no) satisfaction A boolean formula is called “satisfiable” if you can assign truth values to the underlying atoms in such a way that the […]
