Generating solutions to large sudokus

Given a 9x9 grid, divided into (nine non-overlapping) 3x3 subgrids, the objective is to fill each cell with digits $D = \{1, ..., 9\}$ such that

1. Each row contains every digit
2. Each column contains every digit
3. Each 3x3 subgrid contains every digit

The problem of solving a sudoku can be modelled as a satisfiability problem and solved as such by a SAT-solver. Let’s introduce a boolean variable for each digit in each cell, $x_{1,1,1}$ $x_{1,1,2}$ $x_{1,1,3}$ …

Or, more generally $$x_{d,i,j} \quad \forall d,i,j \in D \times D \times D$$ That is, for a 9x9 sudoku there are $9^3$ variables. A cell $i,j$ contains digit $d$ when $x_{d,i,j}$ is true.

Now, to enforce the rules, we have to ensure that a cell contains exactly one digit. That means of all the variables in a cell, only one can be true and for each cell there has to be at least one variable which is true. If, say, the cell 2,3 contains digit 1, then this implies that cell 2,3 does not contain any other digit $$x_{1,2,3} \implies \overline{ x_{2,2,3} } \land \overline{x_{3,2,3} } \land ... \land \overline{ x_{9,2,3} }$$ Similarly, if the cell contains any other digit. Generally, $$x_{d,i,j} \implies \bigwedge_{c \in D \setminus d} \overline{ x_{c,i,j} } \quad \forall d \in D \quad \forall i, j \in D \times D$$ To ensure the second point, that at least one variable in cell 2,3 is true; $$x_{1,2,3} \lor x_{2,2,3} \lor x_{3,2,3} \lor ... \lor x_{9,2,3}$$ Generally, $$\bigvee_{d \in D} x_{d,i,j} \quad \forall i,j \in D \times D$$

To implement the first rule, an approach similar to the above is followed where each row has only one variable true for each digit. For instance, $$x_{1,2,3} \implies \overline{ x_{1,2,1} } \land \overline{ x_{1,2,2} } \land \overline{ x_{1,2,4 } } \land .. \land \overline{ x_{1,2,9} }$$ Generally, $$x_{d,i,j} \implies \bigwedge_{c \in D \setminus j} \overline{ x_{d,i,c} } \quad \forall d \in D \quad \forall i,j \in D \times D$$ Very similarly this is done for the columns and subgrids. (omitted)

To make this digestible for a SAT-solver the problem has to be brought to conjunctive normal form, which consists of clauses anded together, where each clause is variables ored together. $$c_1 \land c_2 \land c_3 \land ...$$ Where each $c$ is of the form $$x_1 \lor x_2 \lor \overline{ x_3} \lor ...$$

An implication of the type $$x_1 \implies \overline{x_2} \land \overline{x_3} \land ...$$ Can equivalenty be expressed as $$x_1 \implies \overline{x2} \land x_1 \implies \overline{x_3} ...$$ To get rid of the implications altogether, the following logical equivalency is used: $p \implies q \iff \overline p \lor q$. Thus $$( \overline{x_1} \lor \overline{x_2} ) \land ( \overline{x_1} \lor \overline{x_3} ) \land ...$$

The sudoku problem can be generalized to, not just 9, but any square number.

The following script generates a description of the $dxd$ sudoku problem given a square number $d$ for a SAT-solver.

#!/usr/bin/env python3
import sys

def gen_clauses( n, d ):
    # ingen ens cifre vandret
    row_clause( n, range( d**2 ), range( 0, d**4, d**2 ) )
    
    # ingen ens cifre lodret
    row_clause( n, range( 0, d**4, d**2 ), range( d**2 ) )

    #ingen ens cifre i kasser
    r = [ j * d + i * d**3 for i in range( d ) for j in range( d ) ]
    a = [ i * d**2 + j for i in range( d ) for j in range( d ) ]
    row_clause( n, a, r )

def digit_clause( d ):
    # kun ét ciffer i hvert felt
    for i in range( d**4 ):
        impl( [ j*d**4+i for j in range(d**2) ] )

def fill_clause( d ):
    # der skal være et ciffer i hvert felt
    for i in range( d**4 ):
        for k in [ j*d**4+i for j in range(d**2) ]:
            print( k+1, end=" " )
        print( 0 )

def row_clause( n, a, r ):
    for i in r:
        impl( [ n+i+j for j in a ] )

def impl( r ):
    for i in r:
        for j in r:
            if i != j:
                print( "-{} -{} 0".format( i+1, j+1) )

def all_clauses( d ):
    for i in range( d**2 ):
        gen_clauses( d**4*i, d )
    digit_clause( d )
    fill_clause( d )

if __name__ == "__main__":
    all_clauses( int( sys.argv[1] ) )

Below are presented solutions to instances of the sudoku problem.

Time taken for computing sudokus up to and including 25x25 is in the order of seconds. 36x36 is in the order of minutes. 49x49 is in the order of hours and I was never able to finish computing a 64x64 sudoku having run out of memory after running for 5 days. How a 64x64 sudoku looks like is left as an exercise for the reader.

---

• 16x16 sudoku
• 25x25 sudoku
• 36x36 sudoku
• 49x49 sudoku

---

16x16

---

25x25

---

36x36

---

49x49