Try to solve Sudoku in various ways (SAT, CSP)

Let's try solving Sudoku with various logic programming and see its advantages and disadvantages. I would like to introduce the following five

Definition of Sudoku rules

Define a rule to see if your program has taken over the definition

  1. One number in one square
  2. One same number per line
  3. One same number in one column
  4. One same number in one block
  5. Satisfy the input

Suppose the input is represented by a tuple (x, y, i) that the condition "the value i is in the row x column y of the cell", and the entire input is represented by a list of that tuple.

SAT

** SAT Solver ** is an algorithm that finds whether there is a boolean value that satisfies a logical expression called CNF (Conjunctive Normal Form). CNF is represented by the logical product of a set of literal ORs (such as $ x_1 \ vee \ neg x_2 \ dots \ vee x_n $) called ** clauses **.

Now let's convert the rules to SAT.

Definition

Suppose $ g_ {x, y, i} $ is true when "the value i is in the row x column y of the cell". Conversely, $ g_ {x, y, i} $ is false when you say "the value i does not fit in the row x column y of the cell (other values fit)".

Rule 1 (one number per square)

If you think about it easily, it looks like this

(g_{x,y,1} \wedge \neg g_{x,y,2} \wedge \dots \wedge\neg g_{x,y,9}) \vee(\neg g_{x,y,1} \wedge g_{x,y,2} \wedge \dots \wedge\neg g_{x,y,9}) \vee \dots \vee\\
(\neg g_{x,y,1} \wedge \neg g_{x,y,2} \wedge \dots\wedge g_{x,y,9})

But this is not a form of CNF, so if you expand it like the distributive law (?) And simplify it, it will be as follows.

(g_{x,y,1} \vee g_{x,y,2} \vee \dots g_{x,y,9}) \wedge (\neg g_{x,y,1} \vee \neg g_{x,y,2})\wedge (\neg g_{x,y,1} \vee \neg g_{x,y,3}) \wedge \dots \wedge\\
(\neg g_{x,y,8} \vee \neg g_{x,y,9})

Rules 2,3,4 (one same number in one row (column, block))

The condition that "there is one or more numbers i in line x" can be written as follows:

g_{x,1,i} \vee g_{x,2,i} \vee \dots g_{x,9,i}

If you add the condition that "there are no more than two numbers i in line x" to this, it becomes rule 2, but if you combine it with rule 1, that condition becomes unnecessary. Because there is one or more numbers 1-9 in each of the 9 cells, [Pigeonhole Principle](https://ja.wikipedia.org/wiki/%E9%B3%A9%E3%81% AE% E5% B7% A3% E5% 8E% 9F% E7% 90% 86) Therefore, there can only be one number for each.

By the way, the condition that "there are no more than one number i in line x" is as follows.

(\neg g_{x,1,i} \vee \neg g_{x,2,i})\wedge (\neg g_{x,1,i} \vee \neg g_{x,3,i}) \wedge \dots \wedge(\neg g_{x,8,i} \vee \neg g_{x,9,i})

The same applies to columns and blocks, so they are omitted.

Rule 5 (satisfy input)

The condition that "the value i is in the row x column y of the cell" means that $ g_ {x, y, i} $ is assigned true.

Implementation

So I will solve it using pysat's minisat.

from pysat.solvers import Minisat22
from itertools import product, combinations


def grid(i, j, k):
  return i * 81 + j * 9 + k + 1

def sudoku_sat(arr):
  m = Minisat22()

  #Rule 1
  for i, j in product(range(9), range(9)):
    m.add_clause([grid(i, j, k) for k in range(9)])
    for k1, k2 in combinations(range(9), 2):
      m.add_clause([-grid(i, j, k1), -grid(i, j, k2)])

  #Rule 2,3
  for i in range(9):
    for k in range(9):
      m.add_clause([grid(i, j, k) for j in range(9)])

  for j in range(9):
    for k in range(9):
      m.add_clause([grid(i, j, k) for i in range(9)])

  #Rule 4
  for p, q in product(range(3), range(3)):
    for k in range(9):
      m.add_clause([grid(i, j, k) for i, j in product(range(p*3, p*3+3), range(q*3, q*3+3))])

  #Rule 5
  for a in arr:
    m.add_clause([grid(a[0], a[1], a[2] - 1)])
  if not m.solve():
    return None
  
  model = m.get_model()
  return [
    [
      [k + 1 for k in range(9) if model[grid(i, j, k) - 1] > 0][0]
      for j in range(9)
    ]
    for i in range(9)
  ]

CSP

~~ This is a copy / paste of university assignments ~~

** CSP (Constraint Programming) ** is an algorithm that solves the following $ V, D, C $ problems.

Premise

Suppose the variable $ v_ {x, y} $ is the value of the cell in row x column y. That is:

Rule 1 can be satisfied only with this premise.

Rules 2,3,4 (one same number in one row (column, block))

If you write down the rule, it will be as follows

(v_{x,0}, v_{x,1})\in\{(1,2), (1,3), \dots (9,8)\} \\
(v_{x,0}, v_{x,2})\in\{(1,2), (1,3), \dots (9,8)\} \\
\vdots\\
(v_{x,7}, v_{x,8})\in\{(1,2), (1,3), \dots (9,8)\} 

However, CSP usually has a convenient function called ʻAll Different`, which makes it easy to describe.

\text{AllDifferent}(v_{x,0}, v_{x,1},\dots,v_{x,8})

The same applies to columns and blocks.

Rule 5 (satisfy input)

Rule 5 can be incorporated from the domain, but it is represented by a constraint for the purpose of separating the input from the fundamental rule part of Sudoku. The constraint that "the value i is in the row x column y of the cell" is as follows

v_{x,y} \in \{i\}

Implementation

Solve using python-constraint.

from constraint import Problem, AllDifferentConstraint, InSetConstraint

def sudoku_csp(arr):

  def grid(i, j):
    return '{}_{}'.format(i, j)

  p = Problem()

  for i, j in product(range(9), range(9)):
    p.addVariable(grid(i, j), range(1, 10))
  
  for i in range(9):
    p.addConstraint(AllDifferentConstraint(), [grid(i, j) for j in range(9)])
    p.addConstraint(AllDifferentConstraint(), [grid(j, i) for j in range(9)])

  for m, n in product(range(3), range(3)):
    p.addConstraint(
      AllDifferentConstraint(),
      [grid(i, j) for i, j in product(range(m*3, m*3+3), range(n*3, n*3+3))]
    )

  for a in arr:
    p.addConstraint(InSetConstraint([a[2]]), [grid(a[0], a[1])])

  solution = p.getSolution()
  return [
    [
      solution[grid(i, j)]
      for j in range(9)
    ]
    for i in range(9)
  ]

Finally

If I do the Advent calendar in this condition, I'm going to die, so I'll cut corners next time.

Recommended Posts

Try to solve Sudoku in various ways (SAT, CSP)
Various ways to extract columns in a NumPy array
Try to solve Sudoku at explosive speed using numpy
I want to solve Sudoku (Sudoku)
Various ways to calculate the similarity between data in python
Try to calculate Trace in Python
Try to put data in MongoDB
6 ways to string objects in Python
Cython to try in the shortest
Various ways to create an array of numbers from 1 to 10 in Python.
Try logging in to qiita with Python
Try to reproduce NumPy's add.at in Julia
I tried to let optuna solve Sudoku
I wanted to solve ABC159 in Python
Various ways to create a dictionary (memories)
Various comments to write in the program
Various ways to destroy resources with scope
Various ways to read the last line of a csv file in Python
Try to display the Fibonacci sequence in various languages in the name of algorithm practice
Try to solve the fizzbuzz problem with Keras
[Python] List Comprehension Various ways to create a list
First steps to try Google CloudVision in Python
Various ways to execute .py files on Windows
Try to implement Oni Maitsuji Miserable in python
3 ways to parse time strings in python [Note]
Try to calculate a statistical problem in Python
3.14 π day, so try to output in Python
Try auto to automatically price Enums in Python 3.6
Try to solve the Python class inheritance problem
Try to separate Controllers using Blueprint in Flask
Try to solve the man-machine chart with Python
Try to calculate RPN in Python (for beginners)
Try to imitate Rails' _method parameter in webapp2
Note that the method of publishing modules to PyPI has changed in various ways.