Koka is a strongly typed functional-style language with effect types and handlers. In this post I attempt to solve the sudoku puzzle using Koka and its effect handlers.

Converting a sudoku puzzle to an exact cover problem is a well known way of solving the puzzle programmatically. Here we skip the conversion of the puzzle to the exact cover matrix and take the exact cover matrix directly as the input.

Implementing Algorithm X for the exact cover problem

The main solve function looks something like the below:

fun solve(grid: list<list<int>>): <div,console,ndet,exn,sudoku|e> maybe<list<int>>
    if grid.length == 0 then return Just([])
    val col = choose_min_column(grid)
    val row_idx = choose_row(grid, col)
    var row := []
    match(grid[row_idx])
        Just(something) -> row := something
        Nothing -> throw-exn(Exception("Invalid row " ++ row_idx.show, ExnError))
    
    val col_set = get_columns_with_1(row) 
    val row_set = get_rows_with_1(grid, col_set) 
    val new_grid = remove_rows_and_cols(grid, row_set, col_set) 
    val new_sol = solve(new_grid)
    match(new_sol)
        Nothing -> 
            Nothing
        Just(new_solution) -> 
            val new_soln_mod = update_row_indices(grid.length, row_set, new_solution)
            Just([row_idx] ++ new_soln_mod)

This is the implementation of the Algorithm X for the exact cover problem by Donald Knuth. We choose a column deterministically - one with the least number of 1s. We then choose a row non-deterministically for the chosen column. Once we get the index of a possible row to be included in a solution, we get the conflicting columns and rows to the column and the newly chosen row. After we remove the conflicting rows and columns, we recurse on the solve function with the smaller exact cover matrix.

We incrementally choose rows from the exact cover matrix to include in the final solution. If at some point we realize the current set of rows included in the solution does not give us the right final solution, we need to backtrack and choose a different row. In Koka we can do this with effects in an elegant way.

This is the effect type and its control operation. The control operation takes the grid and the constraint column index as inputs, and returns the index of the chosen row. Using this operation in the function introduces the sudoku effect in the function type along with the other effects.

effect sudoku
	control choose_row(grid: list<list<int>>, col: int): int

Backtracking with multiple resumption

Here, choosing the row non-deterministically is the effectful operation. If a row is an eligible candidate to be included in an exact cover matrix’s solution (i.e. we have grid[row][col] == 1), we resume with that row’s index. And we continue with finding the rest of the solution that works with the currently chosen row. If at any point we need to backtrack, we can go to the point of execution where we resumed with the previous wrong value and resume with the next possible row. This is a nice feature of Koka where with an effectful operation we can resume as many times as needed.

The effect handler looks like:

fun solveHandler(action) {
    with control choose_row(grid: list<list<int>>, col: int)
        foldl(grid, (0, Nothing), 
            fn((idx: int, prev_soln: maybe<list<int>>), row) 
                if (is-just(prev_soln)) then (idx, prev_soln)
                else if (row[col].default(0) == 1) then (idx + 1, resume(idx))
                else (idx + 1, Nothing)
        ).snd
    action()
}

And we can finally use the handler function with the solve function like so: solveHandler({ solve(grid) })

With the with control block we add the code to handle the choose_row control operation of the sudoku effect. This handler is applied on the action at the end of the block - which is just the main solve function.

Through the choose_row effect we try to choose different rows such that the constraint corresponding to column c is true. Hence the condition where we check row[col].default(0) == 1. If we want to choose this row, we resume with the index for the row. If this row is indeed present in the final solution, when we recurse on the solve function, we will return Just(solution) all the way through. This is captured in the first condition where if we’ve received a valid solution from the function, we ignore the rest of the foldl and return this solution. In case the row we resumed with earlier is not the right choice, leading to dead ends with the reduced exact cover matrix, we return Nothing from the solve function. Now if the next row is a valid option, we resume with the new index, else we just pass a Nothing along to the foldl to skip over to the next row. In the end we return the second value in the tuple returned by foldl (the first value in the tuple is used to store and propagate the index).

In the end, if get a Nothing, there is no valid solution for this exact cover matrix. If there is one, we get the Just(solution).