Wow, that's kinda interesting. I somehow cannot get rid of the feeling of having a really nice hammer and then treating everything as a nail. There are other uses of deep/machine learning that could help SAT solvers. For example, one could try to better guess the learnt clauses to keep/throw away or to restart when the search space is deemed non-interesting through prediction models built using machine learning. See…
I have not been too impressed with fancier SAT solvers. I'm currently drafting a blog post where I compare Minisat, Picosat, Cryptominisat, Lingeling and Glucose. (Those were all that I could easily get running on Linux. Open to more suggestions.) The venerable Minisat was (for the most part) the fastest in my simple use case. What I did notice though was that the "smarter" solvers were more consistent. A poorly writ…
We use SAT solvers extensively in the Phil[0] crossword construction tool, to figure out when the grid is overconstrained, and which letters have only a single value in all possible solutions. We ended up running Glucose (compiled to wasm and running in the browser) because the simpler solvers couldn't solve many instances quickly, and with preprocessing off but most other parameters at their defaults. I didn't do a careful evaluation of all solvers, but it might be interesting.
I really need to write this stuff up.