Two years ago I had to create a quarterly schedule for a team of four, and about 20 tasks with dependencies. I had just read a piece about using SAT solvers fo

Two years ago I had to create a quarterly schedule for a team of four, and about 20 tasks with dependencies. I had just read a piece about using SAT solvers for designing keys and locks that was on HN, and decided to model my problem as a SAT problem. An hour later (about 59:30 coding, 00:30 minicrypto3 running), I had the perfect schedule! It was optimal since it was also proven to be the shortest time to do all tasks. No one caring about this schedule and it didn't matter - one hours work. The joy I got from the exercise - priceless.