I've noticed that puzzles that can be solved with CP-SAT's presolver so that the SAT search does not even need to be invoked basically adhere to this (no backtr

I've noticed that puzzles that can be solved with CP-SAT's presolver so that the SAT search does not even need to be invoked basically adhere to this (no backtracking, known rules), e.g.: #Variables: 121 (91 primary variables) - 121 Booleans in [0,1] #kLinear1: 200 (#enforced: 200) #kLinear2: 1 #kLinear3: 2 #kLinearN: 30 (#terms: 355) Presolve summary: - 1 affine relations were detected. - rule 'affine: new relation' was applied 1 time. - rule 'at_most_one: empty or all false' was applied 148 times. - rule 'at_most_one: removed literals' was applied 148 times. - rule 'at_most_one: satisfied' was applied 36 times. - rule 'deductions: 200 stored' was applied 1 time. - rule 'exactly_one: removed literals' was applied 2 times. - rule 'exactly_one: satisfied' was applied 31 times. - rule 'linear: empty' was applied 1 time. - rule 'linear: fixed or dup variables' was applied 12 times. - rule 'linear: positive equal one' was applied 31 times. - rule 'linear: reduced variable domains' was applied 1 time. - rule 'linear: remapped using affine relations' was applied 4 times. - rule 'presolve: 120 unused variables removed.' was applied 1 time. - rule 'presolve: iteration' was applied 2 times. Presolved satisfaction model '': (model_fingerprint: 0xa5b85c5e198ed849) #Variables: 0 (0 primary variables) The solution hint is complete and is feasible. #1 0.00s main a a a a a a a a a a *A* a a a b b b b *B* a a a a a *C* b d d d b b a a a c c d d *E* d d b b a a c d *D* d e d d d b a a f d d d e e e d *G* a a *F* d d d d d d d g a a f f d d d d d *H* g a *I* i f f d d d h h a a i i i f *J* j j j a a a i i i i i k *K* j a a a Together with validating that there is only 1 solution you would probably be able to make the search for good boards a more guided than random creation.