Sudoku as a SAT problem

Question

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\$.

Task

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 code-golf, 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]]

Answer 1

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!

Answer 2

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.

Answer 3

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
                ¤      - nilad followed by link(s) as a nilad:
   ¤                   -   nilad followed by link(s) as a nilad:
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

Answer 4

ATOM 315 294 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

Answer 5

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.