[joshuata]

Yes, competitive SAT solvers are very complicated. However, they are not outside of most developers' abilities. During a verification course at my University we had to build a simple SAT solver. Most students were able to complete the project in ~20-30 hours. Mine wasn't fast, but it worked well enough to be a proof of concept.

Also, saying that NN are easy with a library like tensorflow is akin to saying that Sudoku solvers are easy with Prolog. Of course they are! The library/language does the vast majority of the heavy lifting.