sudoku.taq

$ java -jar taq.jar sudoku

Running query sudoku in global scope 
4, 1, 2, 3,
2, 3, 4, 1,
1, 2, 3, 4,
3, 4, 1, 2,

Description

sudoku.taq demonstrates numeric analysis of a 4x4 matrix to fill in the missing cells of a Sudoku puzzle. Two things stand out in this example

  1. The query statement consists of chained stages that summarize the steps taken to solve the puzzle
  2. A context list across 3 different scopes (row, col, square) map out strategies for navigating the matrix

$ list<axiom> path

// Table to encode a number in range 1 - 4 as a bit value
// Zero represents "any number"
axiom list encode
( bit )
{ 0xF }
{ 1 }
{ 2 }
{ 4 }
{ 8 }

// Table to decode bit value back to number
// Any invalid bit value is decoded to zero
axiom list decode
( number )
{ 0 }
{ 1 }
{ 2 }
{ 0 }
{ 3 }
{ 0 }
{ 0 }
{ 0 }
{ 4 }
{ 0 }
{ 0 }
{ 0 }
{ 0 }
{ 0 }
{ 0 }
{ 0 }

// Matrix coordinates to navigate the cell groupings
// There are 3 groupings, each in separate scope for
// access using a context list variable
scope row
{
axiom list path
(row, col)
{ 0,0 }{ 0,1 }{ 0,2 }{ 0,3 }
{ 1,0 }{ 1,1 }{ 1,2 }{ 1,3 }
{ 2,0 }{ 2,1 }{ 2,2 }{ 2,3 }
{ 3,0 }{ 3,1 }{ 3,2 }{ 3,3 }
}

scope col
{
axiom list path
(row, col)
{ 0,0 }{ 1,0 }{ 2,0 }{ 3,0 }
{ 0,1 }{ 1,1 }{ 2,1 }{ 3,1 }
{ 0,2 }{ 1,2 }{ 2,2 }{ 3,2 }
{ 0,3 }{ 1,3 }{ 2,3 }{ 3,3 }
}

scope square
{
axiom list path
(row, col)
{ 0,0 }{ 0,1 }{ 1,0 }{ 1,1 }
{ 0,2 }{ 0,3 }{ 1,2 }{ 1,3 }
{ 2,0 }{ 2,1 }{ 3,0 }{ 3,1 }
{ 2,2 }{ 2,3 }{ 3,2 }{ 3,3 }
}

// The puzzle is solved using a 4x4 matrix
list<axiom> matrix
{}

// The puzzle implemented as a 16-integer matrix
flow puzzle
(
integer s11, integer s12, integer s13, integer s14,
integer s21, integer s22, integer s23, integer s24,
integer s31, integer s32, integer s33, integer s34,
integer s41, integer s42, integer s43, integer s44,
matrix@ += axiom { s11, s12, s13, s14 },
matrix@ += axiom { s21, s22, s23, s24 },
matrix@ += axiom { s31, s32, s33, s34 },
matrix@ += axiom { s41, s42, s43, s44 }
)

// Encode puzzle initial parameters
// Cells missing numbers are encoded as a bit value containing candidate numbers
flow encode_puzzle
{ cursor row(matrix) }
(
{
? fact row,
j = 0,
{
item = row[0][j],
encoded = 0xF,
?? (item != 0) encoded = encode[item]->bit,
row[0][j] = encoded,
? ++j < 4
},
row++
}
)

// Eliminate bit values for matrix groupings
flow eliminate
{ cursor group(path) }
(
. i = 0,
{
j = 0,
group = i * 4,
mask = 0,
{
index = matrix[group->row][group->col],
item = decode[index]->number,
?? (item != 0) mask |= encode[item]->bit,
group++,
? ++j < 4
},
j = 0,
group = i * 4,
{
row = group->row,
col = group->col,
flags = matrix[row][col],
item = decode[flags]->number,
?? (item == 0) matrix[row][col] = flags & ~mask,
group++,
? ++j < 4
},
?: ++i == 4
}
)

// Convert puzzle bit values to numbers
flow decode_puzzle
{ cursor row(matrix) }
(
{
? fact row,
j = -1,
{ ?? (++j < 4) row[0][j] = decode[row[0][j]]->number },
row++
}
)

// Print final solution
flow print_puzzle
{ cursor row(matrix) }
(
list<term> r,
{ ?? (r = row++)
print(r[0], ", ", r[1], ", ", r[2], ", ", r[3], ",")
}
)

// Solve sudoku
query sudoku(puzzle)
(
0, 0, 2, 3,
0, 0, 0, 0,
0, 0, 0, 0,
3, 4, 0, 0
) -> (encode_puzzle)
-> (row.eliminate)
-> (col.eliminate)
-> (row.eliminate)
-> (col.eliminate)
-> (square.eliminate)
-> (square.eliminate)
-> (decode_puzzle)
-> (print_puzzle)