# Sudoku as a SAT problem

## Background

An interesting way to solve a Sudoku puzzle is to represent it as a Boolean satisfiability problem, and then feed it to a SAT solver.

A Boolean Satisfiability Problem (abbreviated as SAT problem) is a problem in which you are given a set of Boolean expressions, and you need to find a set of values for the variables such that all the expressions evaluate to true.

SAT solvers usually take a CNF (conjunctive normal form) as input, and output a satisfying assignment if one exists. A CNF is a conjunction (AND) of clauses. A clause is a disjunction (OR) of literals. A literal is a variable or a negated variable. For example, $$\x_1 \vee \neg x_2\$$ is a clause, and $$\x_1\$$ and $$\\neg x_2\$$ are literals.

Let's take the CNF $$\((x_1 \vee x_2) \wedge (\neg x_1 \vee \neg x_2))\$$ as an example. This CNF has two variables, $$\x_1\$$ and $$\x_2\$$. The first clause is $$\x_1 \vee x_2\$$, which means that either $$\x_1\$$ or $$\x_2\$$ must be true. The second clause is $$\\neg x_1 \vee \neg x_2\$$, which means that either $$\x_1\$$ or $$\x_2\$$ must be false. Therefore, the CNF is satisfiable if and only if $$\x_1\$$ and $$\x_2\$$ have opposite values. One possible satisfying assignment is $$\x_1 = 1\$$ and $$\x_2 = 0\$$.

Your task is to write a program or function that takes a Sudoku puzzle as input, and outputs a CNF that represents the puzzle. This means that the output CNF should be satisfiable if and only if the input puzzle has at least one solution.

You don't need to actually find the solution.

A Sudoku puzzle is still considered solvable, even if it has multiple solutions.

Your program or function should pass the following test cases in reasonable time. This is to prevent answers that brute force the sudoku and return a trivial CNF.

## Input

You can take the input in any reasonable format. For example, you can take the input as a list of 81 numbers, where 0 represents an empty cell. The list can be flattened, or as a 9x9 matrix, or even as a 3x3x3x3 array.

## Output

The output is a CNF. The CNF should be represented as a list of lists of integers. Each inner list represents a clause, and each integer represents a literal. Positive integers represent variables, and negative integers represent negated variables. For example, the CNF $$\((x_1 \vee x_2) \wedge (\neg x_1 \vee \neg x_2))\$$ is represented as [[1, 2], [-1, -2]].

The format is based on the DIMACS CNF format used by many SAT solvers.

This is , so the shortest code in bytes wins.

## Test cases

You can check your output CNF using an online SAT solver, such as this one. Your code should generate the CNF in reasonable time, but it's okay if the SAT solver can't solve it in reasonable time.

### Satisfiable

[[8,0,0,0,0,0,0,0,0],[0,0,3,6,0,0,0,0,0],[0,7,0,0,9,0,2,0,0],[0,5,0,0,0,7,0,0,0],[0,0,0,0,4,5,7,0,0],[0,0,0,1,0,0,0,3,0],[0,0,1,0,0,0,0,6,8],[0,0,8,5,0,0,0,1,0],[0,9,0,0,0,0,4,0,0]]
[[0,0,0,7,0,0,0,0,0],[1,0,0,0,0,0,0,0,0],[0,0,0,4,3,0,2,0,0],[0,0,0,0,0,0,0,0,6],[0,0,0,5,0,9,0,0,0],[0,0,0,0,0,0,4,1,8],[0,0,0,0,8,1,0,0,0],[0,0,2,0,0,0,0,5,0],[0,4,0,0,0,0,3,0,0]]
[[0,0,0,0,0,0,0,1,0],[4,0,0,0,0,0,0,0,0],[0,2,0,0,0,0,0,0,0],[0,0,0,0,5,0,4,0,7],[0,0,8,0,0,0,3,0,0],[0,0,1,0,9,0,0,0,0],[3,0,0,4,0,0,2,0,0],[0,5,0,1,0,0,0,0,0],[0,0,0,8,0,6,0,0,0]]
[[0,0,0,0,0,0,0,3,4],[0,8,0,1,0,0,0,0,0],[0,0,0,0,0,0,0,6,0],[0,0,0,0,3,9,0,0,0],[0,0,0,0,4,0,8,0,0],[0,0,1,0,0,0,0,0,0],[0,6,0,2,0,0,0,0,0],[4,0,0,0,0,0,7,0,0],[0,0,0,0,0,0,5,0,0]]
[[7,2,5,8,9,3,4,6,1],[8,4,1,6,5,7,3,9,2],[3,9,6,1,4,2,7,5,8],[4,7,3,5,1,6,8,2,9],[1,6,8,4,2,9,5,3,7],[9,5,2,3,7,8,1,4,6],[2,3,4,7,6,1,9,8,5],[6,8,7,9,3,5,2,1,4],[5,1,9,2,8,4,6,7,3]]
[[0,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,0,0]]


### Unsatisfiable

[[0,0,0,3,0,0,0,1,6],[5,0,0,0,2,0,0,0,0],[0,0,0,0,0,0,0,3,0],[0,1,0,0,5,9,0,0,0],[0,3,6,0,0,0,0,0,0],[0,0,0,0,0,8,2,0,0],[7,0,0,0,0,0,9,0,0],[0,0,0,1,0,0,0,0,0],[9,0,0,0,0,0,0,0,0]]
[[3,0,0,0,0,0,2,0,8],[9,0,0,0,1,0,0,0,0],[0,0,0,0,0,0,0,0,0],[0,1,4,0,0,0,0,9,0],[0,6,0,7,0,3,0,0,0],[0,0,0,0,8,0,0,0,0],[7,5,0,8,0,0,0,0,0],[0,0,0,0,0,0,4,1,0],[0,0,0,3,0,0,0,0,0]]
[[0,0,2,0,6,0,0,0,0],[8,0,0,0,0,0,0,4,0],[0,0,0,0,0,0,0,0,1],[4,0,0,5,0,1,0,0,0],[0,0,0,0,0,0,2,0,0],[0,0,0,9,0,0,0,0,0],[0,0,0,0,3,0,6,2,0],[0,6,0,0,0,0,8,0,0],[1,0,0,7,0,0,0,0,0]]
[[5,0,0,0,0,9,3,0,0],[0,2,0,0,8,0,0,0,0],[0,0,0,0,0,0,1,0,0],[0,0,0,1,0,0,5,7,0],[0,0,4,0,0,0,0,0,0],[0,8,0,0,0,0,0,0,0],[0,0,6,0,0,0,0,8,4],[1,0,0,3,0,0,0,0,0],[0,0,0,0,0,0,0,2,0]]
[[1,0,0,0,0,0,0,0,0],[1,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,0,0]]
[[1,2,3,4,5,6,7,8,9],[1,2,3,4,5,6,7,8,9],[1,2,3,4,5,6,7,8,9],[1,2,3,4,5,6,7,8,9],[1,2,3,4,5,6,7,8,9],[1,2,3,4,5,6,7,8,9],[1,2,3,4,5,6,7,8,9],[1,2,3,4,5,6,7,8,9],[1,2,3,4,5,6,7,8,9]]

• Can't 9x9 sudokus be solved in reasonable time? It might be better to request something along the line of "if the algorithm was extended to general size sudokus it would run in polynomial time", or just have the question be about sudokus of any size in the first place Commented Jun 10, 2023 at 14:43
• You could definately create a SAT file which solved a given 9x9 sudoku, but would take an unreasonable amount of time to solve -- I can't think of how to do that, while also golfing, as the simplest translation to SAT is a fairly good choice! Commented Jun 12, 2023 at 3:38

# Python3, 427 bytes

J=range(1,10)
u=lambda d,*t:d.setdefault(t,max(d.values()or[0])+1)
Y=[(r,c)for r in J for c in J]
def f(b):d={};return[[u(d,r,c,n)for n in J]for r,c in Y]+[[-1*u(d,r,c,v),-1*u(d,r,c,V)]for r,c in Y for v in J for V in J if v<V]+[[u(d,r,n,v)for n in J]for r,v in Y]+[[u(d,n,c,v)for n in J]for c,v in Y]+[[u(d,R*3+i,C*3+j,v)for i,j in Y[:3]]for R,C in Y[:3]for v in J]+[[u(d,r,c,b[r-1][c-1])]for r in J for c in J if b[r-1][c-1]]


Try it online!

• You can save 3 bytes by putting def f(b):d={};return ... all on one line. Commented Jun 10, 2023 at 14:10
• @TheThonnu Thanks, updated Commented Jun 10, 2023 at 14:24
• u=lambda d,t:d.setdefault(t,max(d.values()or[0])+1) saves 16. Then 72 more by making Y(9) a fixed list and Y(3)->Y[3:] and adjusting all ranges to range(1,10) - TIO Commented Jun 10, 2023 at 16:43
• (oh and using u=lambda d,*t:... avoiding many paretheses) Commented Jun 10, 2023 at 16:52
• Starting with d={0:0} saves 2 more by removing or[0] too. Commented Jun 10, 2023 at 17:29

# Charcoal, 97 94 bytes

≔ΦＥθ∧ι⟦⁺×⁸¹ικ⟧ιυＦ⁹Ｆ⁹Ｆ⟦Ｅ⁹↨⟦⊕ικλ⟧⁹Ｅ⁹↨⟦⊕ιλκ⟧⁹Ｅ⁹↨⟦⊕ι÷κ³÷λ³﹪κ³﹪λ³⟧³⟧⊞υλＦ⁸¹Ｆ⁹Ｆκ⊞υ±⁺ι×⁸¹⊕⟦κλ⟧Ｅυ⪫⊞Ｏι⁰


Try it online! Link is to verbose version of code. Explanation:

≔ΦＥθ∧ι⟦⁺×⁸¹ικ⟧ιυ


For each provided digit, mark that digit as being in that cell.

Ｆ⁹


For each digit...

Ｆ⁹


... for each square, row and column...

Ｆ⟦Ｅ⁹↨⟦⊕ικλ⟧⁹Ｅ⁹↨⟦⊕ιλκ⟧⁹Ｅ⁹↨⟦⊕ι÷κ³÷λ³﹪κ³﹪λ³⟧³⟧⊞υλ


... require the digit to appear in that square, row and column.

Ｆ⁸¹


For each cell...

Ｆ⁹Ｆκ


... for each pair of digits...

⊞υ±⁺ι×⁸¹⊕⟦κλ⟧


... only allow one digit to be in that cell.

Ｅυ⪫⊞Ｏι⁰


Pretty-print the output so it can be pasted directly into a solver. (Would be 5 bytes shorter to print it as a Python array literal.)

The output from the CMS solver can be converted back into a pretty grid:

Ｆ⁸¹⊞υωＷＳＦ№ιvＦΦＩ⪪⁻ιv¦ ›λ⁰§≔υλ÷λ⁸¹Ｅ⪪υ⁹⪫ι


Try it online! Link is to verbose version of code. Takes input as a list of newline-terminated lines.

# Jelly, 50 bytes

9;þ¤Z;3/$3ÐƤẎ;;Z¤;€þ9Ẏ ŒJ;þ9ZŒc€ẎN;¢ ŒJ;"FẠƇW€;Çḅ9  A monadic Link that accepts a list of rows of digits, with zeros representing unknown digits and yields a list of lists of integers. Try it online! (footer formats for the the linked tool.) This will print the solved sudoku using output from the linked tool. ### How? Treat each triple of row, column, and digit as a variable, giving $$\9^3=729\$$ variables (the code uses one indexing of each, so these are variables $$\[91,819]\$$). Outputs the givens as single variable clauses, then pairs of negated variables to assert that no cell contains more than one digit, then nonets of variables to assert that each digit appears in each box, row, and column. 9;þ¤Z;3/$3ÐƤẎ;;Z¤;€þ9Ẏ - Link 1: no arguments
9                      -     nine
;þ                    -     table with concatenation
-> Rows as lists of nine [row, column] pairs
$3ÐƤ - last two links as a monad for each non-overlapping three: Z - transpose ;3/ - three-wise reduction with concatenation Ẏ - tighten -> Boxes as lists of nine [row, column] pairs ; - concatenate {Rows} Z - transpose {Rows} -> Columns ; - concatenate -> Boxes + Rows + Columns þ9 - table with {[1..9]} of: ;€ - concatenate to each Ẏ - tighten -> Clauses to assert that no digit repeats in any box, row, or column ŒJ;þ9ZŒc€ẎN;¢ - Link 2: list of lists of integers 0-9, Sudoku ŒJ - multidimensional indices {Sudoku} -> all [row, column] pairs þ9 - table with {[1..9]} of: ; - concatenate Z - transpose Œc€ - unordered pairs of each Ẏ - tighten -> all pairs of variables representing two digits in the same cell N - negate ;¢ - concatenate results of Link 1 ŒJ;"FẠƇW€;Çḅ9 - Main Link: list of lists of integers 0-9, Sudoku ŒJ - multidimensional indices {Sudoku} -> all [row, column] pairs F - Flatten {Sudoku} ;" - zip with concatenation -> all [row, column, value] triples ẠƇ - keep if all -> all [row, column, value] triples with non-zero values W€ - wrap each in a list ;Ç - concatenate results of Link 2 ḅ9 - convert from base nine  # ATOM315294 264 bytes {v="";r=v;c=v;g=v;e=v;p=v;h=100;s=" ";b="\n";l="0\n";n=1~9;n∀{n∀{n∀{t=h*$2+10*$1+*;1~(9-*)∀p+=-t+s+(-t-*)+s+l;v+=t+s;r+=h*$2+10**+$1+s;c+=h**+10*$1+$2+s;g+=(*+2)/3*h+($1-1)/3*300+10*((*-1)%3+1)+30*(($1-1)%3)+$2+s};v+=l;r+=l;c+=l;g+=l;~{$2.(*-1).($1-1)!=0:e+=h*$1+10**+$2.(*-1).($1-1)+" "+l}}};v+b+r+b+c+b+g+b+e+b+p}  (Some minor optimizations, using global variables and one character saved on defining l {h=100;s=" ";b="\n";l=0+b;n=1~9;n∀{n∀{n∀{t=h*$2+10*$1+*;1~(9-*)∀$p+=-t+s+(-t-*)+s+l;$v+=t+s;$r+=h*$2+10**+$1+s;$c+=h**+10*$1+$2+s;$g+=(*+2)/3*h+($1-1)/3*300+10*((*-1)%3+1)+30*(($1-1)%3)+$2+s};v+=l;r+=l;c+=l;g+=l;~{$2.(*-1).($1-1)!=0:$e+=h*$1+10**+$2.(*-1).($1-1)+" "+l}}};v+b+r+b+c+b+g+b+e+b+p}  Version 3 - The v conditions were no longer necessary to include in the solution, and the b variable is redundant. Thanks @Neil! {h=100;s=" ";l="0\n";n=1~9;n∀{n∀{n∀{t=h*$2+10*$1+*;1~(9-*)∀$p+=-t+s+(-t-*)+s+l;$r+=h*$2+10**+$1+s;$c+=h**+10*$1+$2+s;$g+=(*+2)/3*h+($1-1)/3*300+10*((*-1)%3+1)+30*(($1-1)%3)+$2+s};r+=l;c+=l;g+=l;~{$2.(*-1).($1-1)!=0:$e+=h*$1+10**+$2.(*-1).($1-1)+" "+l}}};r+c+g+e+p}


## Usage

input=[[8,0,0,0,0,0,0,0,0],[0,0,3,6,0,0,0,0,0],[0,7,0,0,9,0,2,0,0],[0,5,0,0,0,7,0,0,0],[0,0,0,0,4,5,7,0,0],[0,0,0,1,0,0,0,3,0],[0,0,1,0,0,0,0,6,8],[0,0,8,5,0,0,0,1,0],[0,9,0,0,0,0,4,0,0]];
input INTO
{h=100;s=" ";l="0\n";n=1~9;n∀{n∀{n∀{t=h*$2+10*$1+*;1~(9-*)∀$p+=-t+s+(-t-*)+s+l;$r+=h*$2+10**+$1+s;$c+=h**+10*$1+$2+s;$g+=(*+2)/3*h+($1-1)/3*300+10*((*-1)%3+1)+30*(($1-1)%3)+$2+s};r+=l;c+=l;g+=l;~{$2.(*-1).($1-1)!=0:$e+=h*$1+10**+$2.(*-1).($1-1)+" "+l}}};r+c+g+e+p}  ### Try it online ### Explanation The algorithm constructs several "sections" of output, generating a total of 729 boolean variables of the form xyz where it is true if the xth column and yth row has value z, and false otherwise. With the triple for loop (n∀ n∀ n∀), it creates CNF output for the sudoku rules • v: Each cell must have a value from 1 to 9 v+=(h*$2+10*$1+*+s);  • r: Each row must contain each of the values from 1 to 9 r+=(h*$2+10**+$1+s);  • c: Each column must contain each of the values from 1 to 9 c+=(h**+10*$1+$2+s);  • g: Each 3x3 subgrid must contain each of the values from 1 to 9 g+=((*+2)/3*h+($1-1)/3*300+10*((*-1)%3+1)+30*(($1-1)%3)+$2+s)

• p: No cell can have more than one number in it. It creates an array from 1 to the remainder and places pairs of negative numbers representing every combination of two numbers inside a single cell.
1~(9-*)∀p+=-t+s+(-t-*)+s+l;


Then, the input is used to generate the rules for e, which takes each given non-zero cell and declares that particular rule.

e+=h*$1+10**+$2.(*-1).(\$1-1)+" "+l


Finally, all rules are concatenated and returned.

v+b+r+b+c+b+g+b+e+b+p

• You have no negative numbers in your answer, which means that simply setting all cells to hold all digits will appear to satisfy every grid.
– Neil
Commented Jun 10, 2023 at 19:53
• Oops you're right, I forgot the most important rule of sudoku, that each cell can't have more than 1 number. Editing the solution. Commented Jun 11, 2023 at 3:07
• Having done this, I believe you don't need the v rules, since in order to place all 9 digits in separate cells in one row, column or square you will necessarily need to place one digit in each cell.
– Neil
Commented Jun 11, 2023 at 7:06
• That's a good point as well, it looks like it still passes the test cases when I take out the v component, a few more characters saved! Commented Jun 11, 2023 at 16:09

# JavaScript (Node.js), 201 181 bytes

x=>P(i=>P(j=>P(k=>P(l=>k<l?[[i+j+k,i+j+l],[i+k+j,i+l+j],[k+i+j,l+i+j]]:[P(k=>[-i%3*3-k%3-1+[0|k/3+(~-i/3|0)*3+.8]+j]),[-i+j+x[i-1][j-1]]]))))
P=(f,n=9)=>n?[...P(f,n-1),...f([n])]:[]


Try it online!

• Some variables unused to make it base 10, easier to concat
• Variables are negated, so 81 elements not chosen
• Loop through [i,j,k,l]. When k<l it means "On (i,j) dimension at least one of k and l is not chosen"; When k>=l it's "At least one is chosen"(only tested one dimension) and input condition
• Since other few conditions made there only 81 chosen at maximum, if it's 81 non-empty sets then each have exactly one. Removed the part from exclusive rule.