> For instance, your Alldifferent(X11, X12, X13, X14, X15, X16, X17, X18, X19) constraint would be written as "x11 + x12 + x13 + x14 + x15 + x16 + x17 + x18 + x19 = 1". Same expressive power, on this problem.
I'm more comfortable with constraint-programming than 3SAT / SMT / etc. etc. So I'm probably getting something wrong here.
I don't think you're correct on this issue? "x11 + x12 = 1" means that "x11 or x12 are 1, and the other is zero".
EDIT: That is, the 9-set of solutions you described is:
{1, 0, 0, 0, 0, 0, 0, 0, 0}
{0, 1, 0, 0, 0, 0, 0, 0, 0}
{0, 0, 1, 0, 0, 0, 0, 0, 0}
{0, 0, 0, 1, 0, 0, 0, 0, 0}
{0, 0, 0, 0, 1, 0, 0, 0, 0}
{0, 0, 0, 0, 0, 1, 0, 0, 0}
{0, 0, 0, 0, 0, 0, 1, 0, 0}
{0, 0, 0, 0, 0, 0, 0, 1, 0}
{0, 0, 0, 0, 0, 0, 0, 0, 1}
Meanwhile, Alldifferent(X11, X12, X13, X14, X15, X16, X17, X18, X19) represents the following 9-factorial set of solutions:
{1, 2, 3, 4, 5, 6, 7, 8, 9}
{1, 2, 3, 4, 5, 6, 7, 9, 8}
{1, 2, 3, 4, 5, 6, 9, 8, 7}
{1, 2, 3, 4, 5, 6, 9, 7, 8}
{1, 2, 3, 4, 5, 9, 6, 7, 8}
{1, 2, 3, 4, 5, 9, 6, 8, 7}
{1, 2, 3, 4, 5, 9, 7, 6, 8}
{1, 2, 3, 4, 5, 9, 7, 8, 6}
{1, 2, 3, 4, 5, 9, 8, 6, 7}
{1, 2, 3, 4, 5, 9, 8, 7, 6}
....
{9, 8, 7, 6, 5, 4, 3, 2, 1}
That is, the entire set of permutations of the domain of all 9 variables participating in the constraint. What I've listed above is a *complete* Sudoku solver within the constraint-programming mindset.
--------
In most of the 3SAT / SMT solvers for Sudoku I've seen, you set up the variables as: "X111, X112, X113, X114...", which means "X11 == 1", and "X11 == 2", etc. etc. So you then do "X111 + X112 + X113... X119 == 1", meaning "X11 is either 1, 2, 3, 4, 5... 9".
Meanwhile, this entire process is simply "Domain of X11 = {1, 2, 3, 4, 5, 6, 7, 8, 9}" in the constraint-processing world, because variables can have arbitrarily sized (though finite) domains in constraint programming.
That is to say, I'm pretty sure you need 999 == 729 variables to brute-force represent the problem in 3SAT / SMT? Meanwhile, Constraint Solver trivially represents it with 81-variables (but each of these 81 variables, X11 through X99, have a domain of size 9: {1, 2, 3, 4, 5, 6, 7, 8, 9}).
There might be an easier way to represent Sudoku in 3SAT/SMT world, but again, I'm not very good with that world. I "just" know that 3SAT / SMT is a "similar but different" kind of solver and barely have used them.
--------
One can argue that "constraint programming" is simply 3SAT / SMT-solving except with arbitrarily sized domains. Rather than solely using 0 and 1 or boolean functions.
I've been told that "because everything is {0, 1}, more optimizations / inferences can be discovered" in 3SAT/SMT solvers compared to constraint programmers. Meanwhile, constraint programmers benefit from generic constraints that have a polynomial class subsolution (ie: using maximum flow, or other simpler algorithms to solve the subproblem).
It'd take a rather well-studied expert to know whether 3SAT/SMT is better for a particular problem vs constraint-programming.