Bonjour,

> And what about a sudoko generator with a pertinent notion of level for a
> human ? Would be nice if you could choose the cases that are filled from
> start ...

Actually that is what Helmut Simonis was trying to do with his paper.
He considers :
- difficulty (= level of "complexity" of the filtering algorithm needed to
solve the problem without backtracking)
- minimality (= number of non-redundant information for each deduction)

> These are not formal definition ... yet, but using a representation of
> the problem as a set of close, I think we can do something with the
> complexity of the proof search ...

Constraint programming is has a higher-level representation but I guess
the same could be achieved in SAT.

        Diego Olivier