> Solvers don't do brute force at all > solver will efficiently backtrack all the possible solutions of input variables to come up to your desired endstate, by

> Solvers don't do brute force at all > 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 That seems to be a contradiction, because Back-Tracking uses Brute-Force. The efficiency 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.