[userundefined]

This is pretty much spot on.

In a bit more detail, the CSP solver does indeed apply forward checking, and a fancier version of that, arc consistency, is available too, but ends up being slower on the whole. There's dynamic variable ordering (i.e., "Which word to try next") and conflict directed backjumping (i.e., "Solver's stuck, how far to go back?"). There's some relatively memory hungry structures for checking word constraints, e.g., when two words overlap and one is assigned we want to remove impossible values for the other word, and a specialized "sparse all different" constraint that disallows using a given word more than once.

And also yes, all this happens on the backend and websockets are used to send the latest state to the client.