I found some fascinating paper by Marijn Heule and Oliver Kullmann on advances in SAT solvers and automated reasoning. In particular, the authors where able to show (a year earlier) a breakthrough result on a decade old problem through automated reasoning, showing that state of the art tools on solving boolean satifyability problem are very powerful these days.
I am curious how Mathematica's SAT solver compares to these developments. Does Mathematica's function SatisfiableQ or SatisfiabilityInstances use clever techniques such as Conflict-Driven Clause Learning, look-ahead or Cube-And-Conquere?
The background of my question is the following: I am able to map certain hard problems to boolean formulars, and wonder whether it is immediatly worth learning these other techniques, or is Mathematica sufficently clever solving these systems (or is it basically trying with pure brute-force to find solutions?)
One useful previous answer by a Wolfram developer can be found here, which sets the stage for my question (which methods have been used 3 years ago, but not what explicit techniques and how they compare to state-of-the-art)