SAT solvers are really fast now. Some sort of "neural SAT problem definition" followed by solving it seems to be an interesting direction, but I'm relatively naive on it all. Not sure how training would work since there's no backprop through Boolean logic.