Solving LinkedIn Queens with Haskell

· Agnishom Chattopadhyay

[Thanks to James Haydon for his suggestions on improving the post and the code quality]

On LinkedIn, you can play a variant of the N-Queens problem. A community version of the game (rather, puzzle) can be found here.

Recently, we saw it solved using SAT solvers, using SMT Solvers, using APL and MiniZinc. Today, I will try solving it using Haskell, a slightly more conventional language.

The Puzzle

You are given a N-colored square-shaped board of size N. You must place N queens on the board such that:

  • Each row, each column, and each color region has exactly one queen.
  • No two queens touch each other diagonally.

Note that placing two queens in the same diagonal is acceptable, as long as they are not diagonally adjacent (unlike in Chess).

For instance, one can verify that the following is the only solution for the given colored board.

Haskell Setup

We will use Data.Array from the array library to represent the problem.

type Color = Int
type Row = Int
type Column = Int

type Problem = Array (Row, Column) Color

mkProblem :: [[Color]] -> Problem
mkProblem colorsList =
  Array.array
    ((0, 0), (n - 1, n - 1))
    [((i, j), color) | (i, row) <- zip [0 ..] colorsList, (j, color) <- zip [0 ..] row]
  where
    n = length colorsList

size :: Problem -> Int
size problem = n + 1
  where
    ((_, _), (_, n)) = Array.bounds problem

problem1 :: Problem
problem1 =
  mkProblem
    [ [0, 1, 1, 1, 1],
      [2, 3, 2, 1, 2],
      [2, 3, 2, 1, 2],
      [2, 2, 2, 4, 4],
      [2, 2, 2, 2, 2]
    ]

The problem shown above is encoded as problem1 in the code. I have encoded a few larger examples in this file.

Backtracking, Soundness and Completeness

[Source Code for Attempt 0]

We will tackle the problem using a backtracking approach. This means, we will place a queen on a plausible cell on the board; check if the current configuration can be extended to a full solution; continue if so, and backtrack otherwise, finding a different plausible cell to put the queen on.

To aid our discussion, let us introduce some terminology.

  • A partial placement is a set of positions on the board.
  • A partial placement is sound if it does not violate any of the constraints of the problem, i.e., no two queens are in the same row, column, color region, or are diagonally adjacent. We usually refer to such placements as partial solutions.
  • If a partial placement has N queens, it is complete.
  • A partial solution p extends q if p has all the queens placed in q, and possibly more.

We can describe our backtracking algorithm using this terminology. The algorithm maintains a partial solution. It extends the partial solution by placing additional queens at each step, until enough queens have been placed (i.e, the solution is complete). At the end, we check to see if the solution is also sound. One can see that a sound and complete partial solution solves the given problem, in the sense defined in the previous section.

We represent partial solutions using a Set (Row, Column), the set of currently placed queens. The definition of soundness and completeness can be encoded as a Boolean predicate as follows.

type Partial = Set (Row, Column)

sound :: Problem -> Partial -> Bool
sound problem partial = soundRows && soundColumns && soundColors && soundCorners
  where
    soundRows = all (soundRow partial) [0 .. size problem - 1]
    soundColumns = all (soundColumn partial) [0 .. size problem - 1]
    soundColors = all (soundColor problem partial) [0 .. size problem - 1]
    soundCorners = all (soundCorner partial) partial

complete :: Problem -> Partial -> Bool
complete problem partial = Set.size partial == size problem

We encode our backtracking computations using MonadLogic monads from the LogicT library. This is a generalization of the list monad, which can be used to encode non-deterministic (i.e, branching) computation. Since LogicT is a monad transformer rather than a monad (like the list monad), it can also be composed with other monadic effects. The LogicT library also provides a few additional sophisticated ways of weaving together non-deterministic computations: it makes available interleave, a fair disjunction, which guarantees that the second computation will make progress even if the first computation is non-terminating. This can also be useful in some cases even if the computations are finite, since an interleaved exploration strategy wouldn’t have to exhaust the first branch before exploring the second one. The library comes with a few instances of monads (and monad transformers) which satisfy MonadLogic including ListT(certain older versions of ListT were implemented incorrectly), SeqT and StreamT.

For the purpose of the most naïve solution, we will simply pick N queens and check if the placement is sound. Potential positions for new queens are generated by the candidate computation. If such a candidate is available, we add it into the partial solution; otherwise, we return the current placement of queens. A guard placed in the computation will discard a branch if the condition is not met. Thanks to the monadic interface, we do not need to handle the backtracking control-flow directly.

candidate :: (MonadLogic m) => Problem -> Partial -> m (Row, Column)
candidate problem partial = do
  let n = size problem
  x <- choose [0 .. n - 1]
  y <- choose [0 .. n - 1]
  -- this cell should not have been already picked
  guard $ (x, y) `Set.notMember` partial
  pure (x, y)

-- do an action n times
repeatM :: (Monad m) => Int -> (a -> m a) -> a -> m a
repeatM n f = foldr (>=>) pure (replicate n f)

extend :: (MonadLogic m) => Problem -> Partial -> m Partial
extend problem partial = do
  pos <- candidate problem partial
  -- place a queen on the candidate cell
  pure $ Set.insert pos partial

solution :: (MonadLogic m) => Problem -> m [(Row, Column)]
solution problem = do
  endState <- repeatM (size problem) (extend problem) Set.empty
  guard $ sound problem endState
  pure (Set.toList endState)

Running LogicT

An instance of LogicMonad is the monad Logic, also included in the LogicT library. One can use the observe :: Logic a -> a to read off the first value of the computation.

This version of the solution solves the 5x5 puzzle shown above in around quarter of a second.

ghci> :l src/Attempt0.hs 
...
ghci> :set +s
ghci> observe $ solution problem1
[(0,0),(1,3),(2,1),(3,4),(4,2)]
(0.24 secs, 337,664,536 bytes)

Simple Elimination

[Source Code for Attempt 1]

The original version of this game allows marking cells as eliminated, as a convenience to the user. For example, after placing the queen in the cell shown below, we could mark the others as ’eliminated'.

To improve our solution, we will start marking certain cells as eliminated. We adapt the Partial data structure to accomodate these marks. Note that our use of Map means we can have cells which neither have a queen, nor are marked as eliminated.

data Attempt = HasQueen | Eliminated
  deriving (Show, Eq)

type Partial = Map (Row, Column) Attempt

From now on, we will ensure that our algorithms always deal with sound partial solutions. The Eliminated marks can be used for this. When we place a queen at a cell, we will mark the cells in the same row, same column, of the same color, and around the corners as eliminated. Then, when we generate candidates, we will ignore candidates which are marked as Eliminated.

placeQueen :: Problem -> (Row, Column) -> Partial -> Partial
placeQueen problem (x, y) partial =
  elimCorners (x, y) problem
    . elimColumn y problem
    . elimRow x problem
    . elimColor color problem
    $ newBoard
  where
    newBoard = Map.insert (x, y) HasQueen partial
    color = problem ! (x, y)

candidate :: (MonadLogic m) => Problem -> Partial -> m (Row, Column)
candidate problem partial = do
  let n = size problem
  x <- choose [0 .. n - 1]
  y <- choose [0 .. n - 1]
  -- only pick unmarked cells
  guard (isNothing (Map.lookup (x, y) partial))
  pure (x, y)

The backtracking code can be simplified slightly. We no longer need to check for soundness explicitly.

extend :: (MonadLogic m) => Problem -> Partial -> m Partial
extend problem partial = do
  pos <- candidate problem partial
  -- place a queen on the candidate cell
  pure $ placeQueen problem pos partial

queenView :: Partial -> [(Row, Column)]
queenView partial = [(x, y) | ((x, y), status) <- Map.toList partial, status == HasQueen]

solution :: (MonadLogic m) => Problem -> m [(Row, Column)]
solution problem = do
  endState <- repeatM (size problem) (extend problem) Map.empty
  pure $ queenView endState

This version of the code solves the 5x5 puzzle an order of magintude more quickly.

ghci> :l src/Attempt1.hs 
...
ghci> :set +s
ghci> observe $ solution problem1
[(0,0),(1,3),(2,1),(3,4),(4,2)]
(0.02 secs, 1,060,264 bytes)

However, it still has trouble with the 8x8 puzzles. It takes 150 seconds to solve this puzzle.

ghci> observe $ solution problem2
[(0,3),(1,5),(2,1),(3,7),(4,0),(5,2),(6,6),(7,4)]
(151.08 secs, 266,889,169,608 bytes)

Detecting Dead Ends Early

[Source Code for Attempt 2]

Our first serious attempt at improving the algorithm is to realize that in certain cases we may be able to tell early that a certain partial solution cannot be extended to a full solution, and thus we should avoid exploring the subtree in such cases.

Let us call a partial solution a dead end if it cannot be extended to a full solution. We want to find a predicate pred on partial solutions which can detect dead ends, i.e, pred(p) => deadEnd(p). To do so, it is often helpful to maintain additional information which makes computing the predicate easier. (Note that some partial solution p may be a dead end even if it satisfies pred(p). We need to strike a balance between how expensive it is to compute pred, and the accuracy with which it detects dead ends.)

Here, we will track the number of uneliminated cells in each row, column and color region. If we have a row with no queens and all cells eliminated, then we know that no queens placed in the future can be a complete solution.

We ammend our Partial type to track this information.

data Remaining = Satisfied | AvailableCandidates Int
  deriving (Show, Eq)

data Partial = Partial
  { attempts :: Map (Row, Column) Attempt,
    rowCandidates :: Map Row Remaining,
    columnCandidates :: Map Column Remaining,
    colorCandidates :: Map Color Remaining
  }
  deriving (Show, Eq)

decrease :: (MonadLogic m, Ord k) => k -> Map k Remaining -> m (Map k Remaining)
decrease key candidates =
  case Map.lookup key candidates of
    Just (AvailableCandidates n) -> do
      -- Note: the condition is (n > 1)
      -- we do not want to be left with 0 candidates
      guard (n > 1)
      pure $ Map.insert key (AvailableCandidates (n - 1)) candidates
    _ -> pure candidates

Every time we eliminate a cell, we use the decrease function to update the available candidates for that row, column or color region. If we do have a queen placed in a row, column or color region already, we mark it as Satisfied, and this does not count towards the bad scenario where the subtree is abandoned. Precisely stated, if r = rowCandidates ! i and r = AvailableCandidates m, then there are m values of j such that lookup attempts (i, j) = Nothing. Similar invariants for columns and colors apply.

Note that this function performs a computation in a MonadLogic m, and it discards the branch if the number of candidates go to zero. Thus, the signature of placeQueen has to also be updated to do a monadic computation instead.

placeQueen :: (MonadLogic m) => Problem -> (Row, Column) -> Partial -> m Partial
placeQueen problem (x, y) partial = elimAll newPartial
  where
    newAttempts = Map.insert (x, y) HasQueen partial.attempts
    newRowCandidates = Map.insert x Satisfied partial.rowCandidates
    newColumnCandidates = Map.insert y Satisfied partial.columnCandidates
    color = problem ! (x, y)
    newColorCandidates = Map.insert color Satisfied partial.colorCandidates
    newPartial =
      Partial
        { attempts = newAttempts,
          rowCandidates = newRowCandidates,
          columnCandidates = newColumnCandidates,
          colorCandidates = newColorCandidates
        }
    elimAll =
      elimCorners (x, y) problem
        >=> elimColumn y problem
        >=> elimRow x problem
        >=> elimColor color problem

With this version, we can solve 8x8 puzzles in reasonable time, but the algorithm can still be tuned further.

ghci> :l src/Attempt2.hs 
...
ghci> observe $ solution problem2
[(0,3),(1,5),(2,1),(3,7),(4,0),(5,2),(6,6),(7,4)]
(1.67 secs, 2,821,798,576 bytes)

Generating Candidates Carefully

[Source Code for Attempt 3]

So far, we have been generating candidates simply by looking for the first uneliminated cell. Instead, we could track potential candidates for each row, column and color more directly, and pick from the remaining candidates.

To do this, we update our Partial type once again. The function remove now plays the same role as that of decrease before.

data Remaining a = Satisfied | AvailableCandidates (Set a)
  deriving (Show, Eq)

data Partial = Partial
  { attempts :: Map (Row, Column) Attempt,
    rowCandidates :: Map Row (Remaining Column),
    columnCandidates :: Map Column (Remaining Row),
    colorCandidates :: Map Color (Remaining (Row, Column))
  }
  deriving (Show, Eq)

remove :: (MonadLogic m, Ord k, Ord a) => k -> a -> Map k (Remaining a) -> m (Map k (Remaining a))
remove key a candidates = do
  case Map.lookup key candidates of
    Just (AvailableCandidates s) -> do
      -- Note: the condition is (|s| > 1)
      -- we do not want to be left with 0 candidates
      guard (Set.size s > 1)
      let newSet = Set.delete a s
      pure $ Map.insert key (AvailableCandidates newSet) candidates
    _ -> pure candidates

The following function generates candidates based on candidates for each row.

rowCandidate :: (MonadLogic m) => Partial -> m (Row, Column)
rowCandidate partial = do
  (r, remaining) <- choose $ Map.toList partial.rowCandidates
  s <- case remaining of
    AvailableCandidates s' -> pure s'
    Satisfied -> empty
  c <- choose s
  pure (r, c)

One could also define columnCandidate or colorCandidate similarly. Now, we could set candidate to be either of these three. There is no need to try all of them. Indeed, consider the case in which there are no candidates available from rowCandidate; this means that any candidate from columnCandidate or colorCandidate would definitely violate the row constraints.

This version is slightly better, but the computation still takes substantial time.

ghci> :l src/Attempt3.hs
...
ghci> observe $ solution problem2
[(0,3),(1,5),(2,1),(3,7),(4,0),(5,2),(6,6),(7,4)]
(1.42 secs, 2,175,494,584 bytes)

Ranking Candidates

[Source Code for Attempt 4]

If we consider the following puzzle (problem2, from before), we immediately notice that we must place a queen in the marked square. That’s because this color has exactly one square, and thus the queen of that color must be placed there.

We can formalize this intuition as follows. Let’s fix a partial solution p. Call a set of candidate cells X a strategy (w.r.t. the partial solution p) if every complete solution q that is an extension of p exactly one queen with X. In other words, a strategy is a set of candidate cells at least one of which must be ‘correct’.

Initially, we know that each color, column and row must each contain exactly one queen, which makes them strategies (for the empty partial solution). For each (sound) partial solution, some subset of these regions (rows, colors or columns) would continue to be strategies.

In our algorithm, the Remaining type associated with each row, column or color tracks strategies for each partial solution, for the same reason.

type Strategy = Set (Row, Column)

strategies :: Partial -> [Strategy]
strategies partial =
  [Set.fromList [(r, c) | c <- Set.toList s] | (r, AvailableCandidates s) <- Map.toList partial.rowCandidates]
    ++ [Set.fromList [(r, c) | r <- Set.toList s] | (c, AvailableCandidates s) <- Map.toList partial.columnCandidates]
    ++ [Set.fromList [(i, j) | (i, j) <- Set.toList s] | (_, AvailableCandidates s) <- Map.toList partial.colorCandidates]

When we have a strategy with exactly one candidate (i, j), we should prefer to immediately place a queen at (i, j). By the definition of a strategy, this guarantees that unless the original partial solution was a dead end, we will not be backtracking this decision.

Given a strategy with m candidates, we may have to backtrack m - 1 times before we succeed. To increase the chances that we backtrack as little as possible, we should prefer strategies with fewer candidates.

candidate :: (MonadLogic m) => Partial -> m (Row, Column)
candidate partial
  | null availableStrategies = empty
  | otherwise = choose bestStrategy
  where
    availableStrategies = strategies partial
    -- We choose the strategy with the least number of candidates
    bestStrategy = minimumBy (compare `on` Set.size) availableStrategies

This version of the code is quite fast.

ghci> :l src/Attempt4.hs
...
ghci> observe $ solution problem2
[(0,3),(1,5),(2,1),(3,7),(4,0),(5,2),(6,6),(7,4)]
(0.01 secs, 1,948,544 bytes)

Simplification and Further Optimizations

[Source Code for Attempt 5]

After the previous attempt, we always generate candidates from the set of strategies. After placing each new queen, we update the strategies to remove elements which we mark as eliminated. Therefore, the Eliminated marks are no longer necessary, since we implicitly track them in the strategies. Formally, if a cell (i, j) is in one of the strategies we have maintained, then (i, j) can be added to the partial solution without violating soundness. So, we can have our partial solution track only queens :: Set (Row, Column).

Next, we observe that we traverse the set of strategies every time we generate a candidate to find the smallest ones. Instead, we could employ a data structure to maintain them in sorted order. Conveniently, Haskell’s Data.Set is already such a structure. It comes with lookupMin which can return the smallest element. Thus, we endow Strategy with an Ord instance, to allow us to use Set on them directly.

newtype Strategy = Strategy {unStrategy :: Set (Row, Column)}
  deriving (Show, Eq)

instance Ord Strategy where
  compare (Strategy s1) (Strategy s2) =
    -- prefer smaller sets first
    case compare (Set.size s1) (Set.size s2) of
      EQ -> compare s1 s2
      other -> other

data Partial = Partial
  { queens :: Set (Row, Column),
    strategies :: Set Strategy
  }
  deriving (Show, Eq)

The candidate function uses lookupMin as discussed.

candidate :: (MonadLogic m) => Partial -> m (Row, Column)
candidate partial = do
  -- choose the strategy with the smallest set of candidates
  Strategy s <- case Set.lookupMin partial.strategies of
    Just strat -> pure strat
    Nothing -> empty -- no strategies left, fail
    -- choose a queen from the strategy
  choose s

When we place a queen at (i, j), we now need to update the strategies carefully.

  1. We remove all the strategies which contain (i, j). They have already been satisfied.
  2. From each remaining strategy, we remove the cells directly attacked (i.e., the cells in the same row, column, color region, and around the corners) by the queen at (i, j).
  3. If some strategy is now empty, we fail.
placeQueen :: (MonadLogic m) => Problem -> (Row, Column) -> Partial -> m Partial
placeQueen problem (x, y) partial = do
  -- add a queen to the board
  let newQueens = Set.insert (x, y) partial.queens
  -- remove all the strategies which contains the new queen
  let strat1 = Set.filter (Set.notMember (x, y) . (.unStrategy)) partial.strategies
  -- from each strategy, remove the directly attacked candidates
  let attacked = directlyAttacked (x, y) problem
  let newStrategies = Set.map (eliminateFromStrategy attacked) strat1
  -- fail if this makes some strategies empty
  -- then we are out of candidates
  guard $ Set.notMember (Strategy Set.empty) newStrategies
  pure $
    Partial
      { queens = newQueens,
        strategies = newStrategies
      }

This simplification gives us a modest performance improvement, and simplifies the code.

Further Optimizations

[Source Code for Attempt 6]

Call a set of candidates X a coronation (w.r.t a partial strategy p) if every cell in X appears in every completion of p. Each singleton strategy is a coronation. If we take the union of all singleton strategies, we also get a coronation.

When we have a coronation, we could merge a few executions of solve into one by placing all the queens in the coronation at once. Rather than iteratively filtering candidates in strategies, a lot of the updates and checks can be combined.

coronation :: Partial -> Set (Row, Column)
coronation partial = Set.unions $ Set.map (.unStrategy) $ Set.takeWhileAntitone (\(Strategy s) -> Set.size s == 1) partial.strategies

solve :: (MonadLogic m) => Problem -> Partial -> m Partial
solve problem partial = do
  let super = coronation partial
  if not $ Set.null super
    then do
      -- if there are super strategies, place all queens from them
      newPartial <- placeManyQueens problem super partial
      solve problem newPartial
    else
      -- otherwise, continue with the usual candidate selection
      ifte
        (candidate partial)
        ( \pos -> do
            newPartial <- placeQueen pos partial
            solve problem newPartial
        )
        ( do
            -- Completeness: ensure enough queens were placed
            guard $ Set.size partial.queens == size problem
            pure partial
        )

solution :: (MonadLogic m) => Problem -> m [(Row, Column)]
solution problem = do
  endState <- solve problem (mkPartial problem)
  pure (Set.toList endState.queens)

Here, we write an explicitly recursive function solve, since we may place more than one queen at a time. Note the use of the ifte from the LogicT library. We cannot do this easily using the usual if _ then _ else construct, since there is no associated Bool to check. In the event that there are no candidates avaiable, we check using the guard if enough queens have been placed.

By virtue of maintaining soundness, we can guarantee that our algorithm never encounters a partial solution with more than N queens, either. If we did place more than N queens, there would be at least one row (or column, or color region) with more than one queen, violating soundness.

The function placeManyQueens is similar to placeQueen, except that it handles a set of queens at once. Note that we do have to check whether this set of queens in the coronation is sound, i.e, if they attack each other.

placeManyQueens :: (MonadLogic m) => Problem -> Set (Row, Column) -> Partial -> m Partial
placeManyQueens problem positions partial = do
  -- check if the set is sound
  guard $ sound problem positions
  -- remove all the strategies which contains any of the new queens
  let strat1 = Set.filter (Set.disjoint positions . (.unStrategy)) partial.strategies
  -- from each strategy, remove the directly attacked candidates
  let attacked = Set.unions $ Set.map (partial.directlyAttacked !) positions
  let newStrategies = Set.map (eliminateFromStrategy attacked) strat1
  -- fail if this makes some strategies empty
  -- then we are out of candidates
  guard $ Set.notMember (Strategy Set.empty) newStrategies
  pure $
    partial
      { queens = Set.union positions partial.queens,
        strategies = newStrategies
      }

We use another optimization to speed up the computation of placeQueen and placeManyQueens. We precompute the set of cells directly attacked by each cell in the problem. The type Partial for this version is as follows.

data Partial = Partial
  { queens :: Set (Row, Column),
    strategies :: Set Strategy,
    directlyAttacked :: Array (Row, Column) (Set (Row, Column))
  }
  deriving (Show, Eq)

This version of the code is consistently faster, but the improvement is very small.

Heaps vs Sets

Strictly speaking, rather than maintaining the strategies in sorted order, we only need to be able to efficiently find the smallest strategy. This is exactly what a heap does. We can use a heap to maintain the strategies, and use insert and deleteMin to add and remove strategies efficiently.

We implemented a version of the algorithm using Data.Heap (from the heaps library). Unfortunately, this version is slightly slower.

A couple of things we observed about Heap vs Set:

  • Set automatically deduplicates elements. With Heap, one has to call Heap.nub to remove duplicates.
  • A monadic version of map, Heap.mapM is available in the Heap library. In the Set library, there is no Set.mapM. Thus, in Set, we cannot use the pattern of using a guard to fail immediately when we find an empty strategy.

SMT Solvers

[Source Code for SMT Encoding]

SMT solvers, such as Z3, can solve constraint satisfaction problems involving a number of domains (called theories) including boolean logic, arithmetic, and arrays. Using the sbv library, we can encode our problem as constraints for Z3 in a straightforward manner.

We pick N symbolic integers. The i-th integer represents the column j in which the queen of row i is placed. The constraints can be exressed as follows:

-- for each row, the column where the queen is placed
-- ranges from 0 to n-1
rangeConstraints :: [SInteger] -> SBool
rangeConstraints js = sAll (\y -> y .>= 0 .&& y .< n) js
  where
    n = fromIntegral $ length js

-- no two queens are in the same column
columnConstraints :: [SInteger] -> SBool
columnConstraints js = 
  sAll 
    (\(a, b) -> a ./= b) 
    [(a, b) | (i, a) <- zip [(0 :: Int) ..] js, (j, b) <- zip [0 ..] js, i < j]

-- no two queens are touching corners
-- queen[i] - queen[i+1] != 1 or -1
cornerConstraints :: [SInteger] -> SBool
cornerConstraints js =
  sAll
    (\(a, b) -> a - b ./= 1 .&& a - b ./= -1)
    [(a, b) | (a, b) <- zip js (drop 1 js)]

-- no two queens are in the same color region
-- for each pair of cells (i, j) and (k, l),
-- color ! (i, j) == color ! (k, l) ==> not (queen[i] = j && queen[k] = l)
colorConstraints :: Problem -> [SInteger] -> SBool
colorConstraints problem queens = 
    sAll 
      f 
      [(i, j, k, l) | 
        i <- [0 .. n - 1], 
        j <- [0 .. n - 1], 
        k <- [i .. n - 1], 
        l <- [0 .. n - 1], 
        (i /= k || j < l)]
  where
    n = size problem
    f (i, j, k, l) = 
      (fromBool $ problem ! (i, j) == problem ! (k, l)) 
        .=> sNot (queens !! i .== fromIntegral j .&& queens !! k .== fromIntegral l)

We observe that our solution is orders of magnitude faster than calling the SMT solver. However, it is instructive to keep in mind that our benchmark includes the time it takes to compute the constraints, do interprocess communication with z3, and so on. As suggested by the blogpost involving approaching this problem with MiniZinc, the actual solving time is much smaller.

Benchmarks

We ran our benchmarks using the tasty-bench library. For the two problems discussed above, the time taken are as follows.

ProblemAttempt 0Attempt 1Attempt 2Attempt 3Attempt 4Attempt 5 (Heap)Attempt 5 (Set)Attempt 6SMT Solver (Z3)
Problem 117.6 ms19.1 μs21.7 μs20.0 μs20.5 μs22.3 μs11.7 μs10.8 μs5.18 ms
Problem 2-17.057 s193 ms172 ms65.5 μs101 μs52.2 μs48.6 μs13.4 ms

Next, we benchmarked our code on the puzzles available in the community version of the game. They contain puzzles of board sizes ranging from 7 to 11. We ran our algorithms on all puzzles of size N at a time. The times shown are the average time taken to solve a puzzle of size N. For some of the entries in the table, we timed out. This means that completing all the problems together and doing them multiple times as required by tasty-bench took more than 60 seconds.

SizeAttempt 1Attempt 2Attempt 3Attempt 4Attempt 5 (Heap)Attempt 5 (Set)Attempt 6SMT Solver (Z3)
7 (48 problems)269.66 ms5.15 ms4.75 ms189 μs214 μs168 μs159 μs11.02 ms
8 (145 problems)-81.11 ms72.12 ms197 μs269 μs166 μs152 μs20.62 ms
9 (137 problems)---310 μs448 μs275 μs243 μs32.03 ms
10 (60 problems)---463 μs664 μs430 μs376 μs51 ms
11 (17 problems)---682 μs900 μs652 μs605 μs67 ms

Conclusion

This is an instance of a constraint-satisfaction problem, similar to other puzzles like Sudoku, or the original N-Queens. This is what makes them a great candidate for solution via SAT or SMT solvers, as noted by previous bloggers. There are a few knobs we can tweak to make our algorithm perform better:

  • How do we decide where to place the next queen?
  • When there are multiple options to do so, in which order do we explore them?
  • How can we quickly decide that a partial solution cannot be extended to a full solution?

Furthermore, computing each of the heuristics above can be expensive. Therefore, we have to strike a balance between the time spent on computing sophisticated heuriststics, and the time spent on actually exploring the search tree.

In the general case, these problems can be very hard to solve. However, we can hope that the instances which appear on LinkedIn would be easier. Since these puzzles would be supposed to be enjoyable for humans, there are likely reasonable heuristics one can pick to solve them. In particular, if we do so, we can hope to detect bad branches early, and backtrack quickly.

We obtained a solution which is less than 150 lines of Haskell, and is arguably quite fast. We have heavily used Set and Map, which are persistent data structures, making it easy to access ‘older’ versions of our computation state, when we backtrack.