> When this solver backjumps, it forgets the failure as soon as it lands, so if the same dead end comes up in a different part of the search it gets rediscovered from scratch.
Modern solvers such as CP-SAT combine some SAT features with a CP solver, based of the work of Peter Stuckey I think.