N-Queens Solver - Saga Examples

This example solves the N-Queens problem using two effects: Choose for nondeterministic search and Fail for pruning invalid placements.

The idea: place N queens on an NxN board so no two threaten each other. Each queen goes in its own row, so we just need to choose a column per row. The Choose handler explores all possibilities and Fail prunes the dead ends.

Effects

We define two effects. Choose picks an element from a list nondeterministically, and Fail aborts a branch of the search:

effect Choose {
  fun choose : List a -> a
}

effect Fail {
  fun fail : String -> a
}

The handler

all_solutions is where the magic happens. When choose is called, the handler resumes once for each option and collects the results with flat_map. When fail is called, it returns an empty list (no solutions down this path). A successful computation wraps its value in a singleton list:

handler all_solutions for Choose, Fail {
  choose options = List.flat_map (fun x -> resume x) options
  fail _ = []
  return value = [value]
}

This is a multi-shot continuation: resume is called multiple times in the choose arm, once per option. The handler effectively turns a sequential program into a backtracking search.

Safety check

A helper that checks whether placing a queen at a given column conflicts with any already-placed queen. placed is a list of columns for rows already filled, bottom to top:

fun guard : Bool -> Unit needs {Fail}
guard True = ()
guard False = fail! "pruned"

fun safe : (col: Int) -> (placed: List Int) -> Bool
safe col placed = {
  let rows_back = List.range 1 (List.length placed)
  let checks = List.zip placed rows_back
  List.all (fun pair -> {
    let (c, dist) = pair
    c != col && Int.abs (c - col) != dist
  }) checks
}

Solver

The solver places one queen per row. It chooses a column, checks if it's safe, and recurses. The effects handle the backtracking automatically:

fun solve : (n: Int) -> (placed: List Int) -> List Int needs {Choose, Fail}
solve n placed =
  if List.length placed == n then List.reverse placed
  else {
    let col = choose! (List.range 1 n)
    guard (safe col placed)
    solve n (col :: placed)
  }

fun queens : (n: Int) -> List (List Int)
queens n = solve n [] with all_solutions

Running it

main () = {
  println "4-Queens solutions:"
  let solutions = queens 4
  List.iter dbg solutions
  println $"Found {List.length solutions} solutions"

  let eight = queens 8
  println $"8-Queens: found {List.length eight} solutions"
} with {console}

Output:

4-Queens solutions:
[2, 4, 1, 3]
[3, 1, 4, 2]
Found 2 solutions

8-Queens: found 92 solutions

Full source

effect Choose {
  fun choose : List a -> a
}

effect Fail {
  fun fail : String -> a
}

handler all_solutions for Choose, Fail {
  choose options = List.flat_map (fun x -> resume x) options
  fail _ = []
  return value = [value]
}

fun guard : Bool -> Unit needs {Fail}
guard True = ()
guard False = fail! "pruned"

fun safe : (col: Int) -> (placed: List Int) -> Bool
safe col placed = {
  let rows_back = List.range 1 (List.length placed)
  let checks = List.zip placed rows_back
  List.all (fun pair -> {
    let (c, dist) = pair
    c != col && Int.abs (c - col) != dist
  }) checks
}

fun solve : (n: Int) -> (placed: List Int) -> List Int needs {Choose, Fail}
solve n placed =
  if List.length placed == n then List.reverse placed
  else {
    let col = choose! (List.range 1 n)
    guard (safe col placed)
    solve n (col :: placed)
  }

fun queens : (n: Int) -> List (List Int)
queens n = solve n [] with all_solutions

main () = {
  println "4-Queens solutions:"
  let solutions = queens 4
  List.iter dbg solutions
  println $"Found {List.length solutions} solutions"

  let eight = queens 8
  println $"8-Queens: found {List.length eight} solutions"
} with {console}