&gt; Solvers don&#x27;t do brute force at all<p>&gt; solver will efficiently backtrack all the possible solutions of input variables to come up to your desired endstate, by filtering out impossible paths and values<p>That seems to be a contradiction, because Back-Tracking uses Brute-Force. The <i>efficiency</i> comes from heuristics that can fail, which is kind of important to note. SAT problems are in principle np-complete with all the uncertainty that implies.