module sudoku

abstract sig Number {}

one sig One, Two, Three, Four, Five, Six, Seven, Eight, Nine 
extends Number {}

// We assume only one Board configuration.
one sig Board {
    // cells map a row and a column to one number.
    cells: Number -> Number -> one Number
}

fact rowsAreUnique {
    all r : Number |
        Number = Board.cells[r][Number]
}

fact colsAreUnique {
    all c : Number |
        Number = Board.cells[Number][c]
}

fun div3(n : Number) : Number {
    let divTable = One -> One + 
                             Two -> One +
                             Three -> One + 
                             Four -> Two +
                             Five -> Two +
                             Six -> Two +
                             Seven -> Three +
                             Eight -> Three +
                             Nine -> Three |
    divTable[n]
}

pred sameBlock(r, c, r', c' : Number) {
    div3(r) = div3(r') and div3(c) = div3(c')
}

pred blocksOfOne(r, c : Number) {
    sameBlock(One, One, r, c)
}
run blocksOfOne



//fact blocksAreUnique {
//    all r, c, r', c' : Number |
//        (sameBlock(r, c, r', c') and (r != r' or c != c'))
//            implies (Board.cells[r][c] != Board.cells[r'][c'])
//}



// The following puzzle was on the sudoku.com main page.
pred samplePuzzle() {
    let problem = One -> Two -> Six +
                             One -> Four -> One +
                             One -> Six -> Four +
                             One -> Eight -> Five +
                             Two -> Three -> Eight +
                             Two -> Four -> Three +
                             Two -> Six -> Five +
                             Two -> Seven -> Six +
                             Three -> One -> Two +
                             Three -> Nine -> One +
                             Four -> One -> Eight +
                             Four -> Four -> Four +
                             Four -> Six -> Seven +
                             Four -> Nine -> Six +
                             Five -> Three -> Six +
                             Five -> Seven -> Three +
                             Six -> One -> Seven +
                             Six -> Four -> Nine +
                             Six -> Six -> One +
                             Six -> Nine -> Four +
                             Seven -> One -> Five +
                             Seven -> Nine -> Two +
                             Eight -> Three -> Seven +
                             Eight -> Four -> Two +
                             Eight -> Six -> Six +
                             Eight -> Seven -> Nine +
                             Nine -> Two -> Four +
                             Nine -> Four -> Five +
                             Nine -> Six -> Eight +
                             Nine -> Eight -> Seven
        |
        all r, c: Number |
            Board.cells[r][c] = problem[r][c]
}

run samplePuzzle