Lovely video, and it was enormously personally satisfying to me while he was describing his evolutionary algorithm I just sat thinking "why not just use a SAT solver, this seems like child's play for z3?" and then hearing him go "then I asked Reddit and someone suggested using a SAT solver". Hell yeah, good job, brain! I mean, not as good a job as Brian who actually implemented it and made the video and everything, but still!