Download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
language ESSENCE 1.3.0
 
$ prob057: Killer Sudoku
$ Essence model by Andrew Martin
$
$ Licenced under CC-BY-4.0 : http://creativecommons.org/licenses/by/4.0/
$ Problem details available at http://www.csplib.org/problems/prob057/
$
 
given gridSize : int(1..)
given numHints : int(1..)
given maxHintCells : int(1..)
 
letting dHintGrid be domain int(1..numHints)
letting dIndivHint be domain int(1..maxHintCells)
letting dSolutionGrid be domain int(1..gridSize*gridSize)
letting dHintFormat be domain int(1..2)
 
letting hintSumIndex be maxHintCells + 1
 
$FORMAT = [[x,y],[x,y],...,[sum of cells,cells in hint]
given hintMatrix : matrix indexed by [dHintGrid, int(1..hintSumIndex), dHintFormat] of int(0..)
 
find solutionGrid : matrix indexed by [dSolutionGrid, dSolutionGrid] of dSolutionGrid
 
$Rows, columns
such that
    forAll i : dSolutionGrid . allDiff(solutionGrid[..][i]) /\ allDiff(solutionGrid[i][..])
 
$Boxes
such that
    $for each box
    forAll gridColumn, gridRow : int(0..gridSize-1) .
 
        $bijective function ensures allDiff on 2d submatrix
        exists numberMapping : function (total, bijective) dSolutionGrid --> dSolutionGrid .
             
            $for each element within the box
            forAll boxColumn, boxRow : int(1..gridSize) .
                 
                $all elements are different
                numberMapping(boxColumn + ((boxRow-1)*gridSize)) = solutionGrid[(gridColumn*gridSize) + boxColumn][(gridRow*gridSize) + boxRow]
 
$Hints
such that
    forAll hintSet : dHintGrid .
 
        $ensure sum of hint cells is equal to given sum
        (sum index : int(1..hintMatrix[hintSet][hintSumIndex][2]) . (solutionGrid[ hintMatrix[hintSet][index][1] ][ hintMatrix[hintSet][index][2] ] ) ) = hintMatrix[hintSet][hintSumIndex][1]