Homework 3

Jio Gim, Creative IT Engineering, POSTECH
Student ID: 20160087, Povis ID: iknowme

🤔 Tip: This page uses KaTeX feature of Gitlab. If you are watching this document in Github, look this prerendered README.

Sudoku Board

How I used CNF to solve E/O Sudoku game

Value Mapping

In my solver (named SUDOKUS), $`x_{(i,j,k)}`$ which means whether if $`i`$ th row $`j`$ th column has value $`k`$ is mapped to $`ijk`$. For example, when $`777`$ is true, the cell of $`7`$ th row $`7`$ th column should have a value of $`7`$.

CNF Making

Below items are conjuncted.

• All possibilities for an empty cell
  For all empty cells, add condition of its all possibilities. For instance, in the cell of $`7`$ th row $`7`$ th column on right figure, the number $`1`$, $`3`$, $`5`$, $`7`$, $`9`$ cannot be in there. So in this case, the condition $`(x_{(7,7,2)}\lor x_{(7,7,4)}\lor x_{(7,7,6)} \lor x_{(7,7,8)})\land \lnot x_{(7,7,1)} \land \lnot x_{(7,7,3)} \land \lnot x_{(7,7,5)} \land \lnot x_{(7,7,7)} \land \lnot x_{(7,7,9)}`$ will be included to the CNF sentence. In this phase, Even/Odd Sudoku rules are also applied.

• Basic Sudoku rules
  There're three major rule: $`1`$ to $`9`$ in each sub-grid, in each column, and in each row. This can be expressed in CNF as below.

  • Sub-grid level
    $`(x_{(1,1,1)} \lor x_{(1,2,1)} \lor x_{(1,3,1)} \lor x_{(2,1,1)} \lor x_{(2,2,1)} \lor x_{(2,3,1)} \lor x_{(3,1,1)} \lor x_{(3,2,1)} \lor x_{(3,3,1)})`$
    $`\land (x_{(1,1,2)} \lor x_{(1,2,2)} \lor x_{(1,3,2)} \lor x_{(2,1,2)} \lor x_{(2,2,2)} \lor x_{(2,3,2)} \lor x_{(3,1,2)} \lor x_{(3,2,2)} \lor x_{(3,3,2)})`$
    $`\cdots`$
    $`\land (x_{(1,1,9)} \lor x_{(1,2,9)} \lor x_{(1,3,9)} \lor x_{(2,1,9)} \lor x_{(2,2,9)} \lor x_{(2,3,9)} \lor x_{(3,1,9)} \lor x_{(3,2,9)} \lor x_{(3,3,9)})`$

  • Row level
    $`(x_{(1,1,1)} \lor x_{(1,2,1)} \lor x_{(1,3,1)} \lor x_{(1,4,1)} \lor x_{(1,5,1)} \lor x_{(1,6,1)} \lor x_{(1,7,1)} \lor x_{(1,8,1)} \lor x_{(1,9,1)})`$
    $`\land (x_{(1,1,2)} \lor x_{(1,2,2)} \lor x_{(1,3,2)} \lor x_{(1,4,2)} \lor x_{(1,5,2)} \lor x_{(1,6,2)} \lor x_{(1,7,2)} \lor x_{(1,8,2)} \lor x_{(1,9,2)})`$
    $`\cdots`$
    $`\land (x_{(1,1,9)} \lor x_{(1,2,9)} \lor x_{(1,3,9)} \lor x_{(1,4,9)} \lor x_{(1,5,9)} \lor x_{(1,6,9)} \lor x_{(1,7,9)} \lor x_{(1,8,9)} \lor x_{(1,9,9)})`$

  • Column level
    $`(x_{(1,1,1)} \lor x_{(2,1,1)} \lor x_{(3,1,1)} \lor x_{(4,1,1)} \lor x_{(5,1,1)} \lor x_{(6,1,1)} \lor x_{(7,1,1)} \lor x_{(8,1,1)} \lor x_{(9,1,1)})`$
    $`\land (x_{(1,1,2)} \lor x_{(2,1,2)} \lor x_{(3,1,2)} \lor x_{(4,1,2)} \lor x_{(5,1,2)} \lor x_{(6,1,2)} \lor x_{(7,1,2)} \lor x_{(8,1,2)} \lor x_{(9,1,2)})`$
    $`\cdots`$
    $`\land (x_{(1,1,9)} \lor x_{(2,1,9)} \lor x_{(3,1,9)} \lor x_{(4,1,9)} \lor x_{(5,1,9)} \lor x_{(6,1,9)} \lor x_{(7,1,9)} \lor x_{(8,1,9)} \lor x_{(9,1,9)})`$

  • For all sets of disjunctions above: Make negative tuples of nonsame elements of them to make no any duplicated candidates get still alive in solutions.
    $`(x_{(1,1,1)} \lor x_{(2,1,1)} \cdots x_{(9,1,1)})`$ $`\rightarrow (\lnot x_{(1,1,1)} \lor \lnot x_{(2,1,1)}) \land (\lnot x_{(1,1,1)} \lor \lnot x_{(3,1,1)}) \land \cdots \land (\lnot x_{(8,1,1)} \lor \lnot x_{(9,1,1)})`$

References

• XOR to CNF: https://math.stackexchange.com/questions/636119/find-dnf-and-cnf-of-an-expression
• Compared Solver: https://sudokuspoiler.azurewebsites.net/OddEvenSudoku

Development Notes

• DO NOT USE Lombok → It does not supports Java 10.
• Logging in file output is now turned off to keep my score safe. It can re-turned on by uncommenting all comments in src/test/resources/logback-test.xml.