dobrichev wrote:Thank you for these numbers.

Are you sending only the direct contradiction clauses to SAT? If so, you may try to bombard it additionally with clauses that simulate some of the basic techniques.

I do not really understand your question concerning the contradiction. The variables of the SAT clauses are the candidates/pencilmarks of not yet filled cells and the givens. The variables corresponding to the givens are set to true while with the variables belonging to the candidates we construct clauses for each cell, each row, each column and each block which describe that

1.in each unfilled cell at least one candidate is true and at most one candidate is true

2 in each row/column block for each number at least one candidate ist true and at most one candidate ist true.

If for example in cell C there are 3 candidates 2, 4, 7 left corresponding to the variables a, b, c we have the 4 clauses (a or b or c), (not a or not b), (not a or not c), (not b or not c).

If for example in row R the candidates for 7 are exactly in column 5 and column 6 corresponding to variables d and e we add the clauses (d or e), (not d or not e).

In DIMACS CNF format (which is the input format for a SAT solver) the variables are coded with numbers and for a given puzzle size I code a candidate/given in row r and column c and value n (r, c internally zero based) by r * S^2 + c * S + n where S is the number of cells in a row/column/block. So the "variable names" range from 1..S^3, but only fewer variables really are used, depending on the number of candidates left.

This all is quite straighforward and I do not think it is useful to simulate basic techniques within SAT. I apply the basic techniques

before I do the SAT part and try to eliminate as many candidates as possible there.