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 (my) blogpost here: https://www.msoos.org/2018/01/predicting-clause-usefulness/ (sorry, self-promotion, but relevant)
Let's not forget the work that could be done on auto-configuring SAT solvers, tuning their configuration to the instance, as per the competition at: http://aclib.net/cssc2014/
Another piece of work in this domain are portifolio solvers, which pick the best-fitting SAT solver from a list of potentials, after having guessed the best one given the instance profile, e.g. priss at http://tools.computational-logic.org/content/riss.php
I think there are some interesting low-hanging fruits in there somewhere, using regular SAT solvers and machine/deep learning, exploiting domain-specific information and know-how.
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 written CNF might take 50x longer than it should (when compared to N-1 and N+1 instances). Minisat (but moreso Picosat) would occasionally hit an edge case or something and slow way down. Fancier solvers produced a nice clean line on the graphs, without anomalous 50x spikes.
Note that winning in the competition, until 2017, meant you solved the most instances, each with a ~5000s timeout. So if you solved every single one within 4999s you won, you were the best... This obviously encouraged incredibly long startup times that are gained back over the overall 5000s timeout. It clearly does not mimic normal use-cases.
We use SAT solvers extensively in the Phil 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.
I think we ought to collect a lot more data, which would allow for better heuristics. But collecting data incurs running overhead, so it must be configurable -- collect when not in a "competition mode" and analyse, then during in the competition, only collect the data really needed for the computed prediction algorithm to correctly function.