Propositional Satisfiability

For each cell with a given value, we assert p(i, j, n) when the cell in row i and column j has the given value n.

We assert that every row contains every number:

 We assert that every column contains every number:

We assert that each of the nine 3 × 3 blocks contains every number:

To assert that no cell contains more than one number, we take the conjunction over all values of n, n', i, and j where each variable ranges from 1 to 9 and n ≠ n
 of p(i, j, n) → ¬p(i, j, n').