Hillel Wayne wrote about solving the LinkedIn Queens problem with SMT in his Computer Things newsletter, inspired by Ryan Berger's post on using SAT. This post describes using MiniZinc to solve the problem in a more readable way.

The Game

Similar to N-Queens and Star Battle, goal is to place nn queens on a n×n chessboard. Rules for attacking are a hybrid of chess pieces (queen attacks same row/column and adjacent squares). There are nn connected areas with different colors and one Queen in each. Example: 9×9 LinkedIn Queens puzzle with unique solution.

MiniZinc

Use the constraint modelling language MiniZinc, designed for expressing combinatorial optimization problems. Download the MiniZinc IDE bundled with several solvers (developed and tested with version 2.9.2). For a full introduction, see the MiniZinc Handbook.

The MiniZinc model

Divide into four parts: data, variables, constraints, and search/ output.

• Representing an instance: Use MiniZinc to specify values in the main .mzn file and bind them in a data file .dzn. Let n represent the board size, N be the set of integers based on n, and board be the set of colored areas.
• The variables: Use an array of N variables, one for each row, with a domain specifying the column where the Queen for that row is. This has benefits like guaranteeing the right number of queens and ensuring one queen per row.
• The constraints: Use simple arithmetic constraints, the all_different constraint, and looking up values in an array with a variable index. Ensure a single queen in each column, no queens adjacent to each other, and each area gets its own queen.
• Search and output: Use solve satisfy; to find a satisfying solution. The output statement builds up the board with squares having queens represented as q.

The full program

Putting it all together, this is the full program to solve the puzzle. Include "globals.mzn", define data (board size, colors, and board layout), declare variables (column position of queens), add constraints (ensuring single queen in each column, no adjacent queens, and each area has a queen), and use solve satisfy; and output to display the solution.

Solving the instance

Using different solvers:

• Gecode: Built-in standard solver gives a solution in a few milliseconds with 29 failures before finding the solution. Gist can be used to visualize the search tree.
• OR-Tools CP-SAT: A Lazy Clause Generation constraint programming solver with a powerful portfolio. Solves the problem in a bit more time without any failures.
• The HiGHS MIP Solver: Another built-in solver that translates the model into a different representation. Solves the problem quickly with just a single node.

Using more pre-processing

Using the -O5 option with Gecode does all the pre-processing (domain shaving or singleton arc consistency), and Gecode can now solve the problem without any search.

Summary

The LinkedIn Queens/Star Battle problem is easy to solve with combinatorial optimization solvers. MiniZinc has two main features that make it attractive for modelling these types of problems: clarity and readability of models and the ability to experiment with different solvers. For larger and more complicated problems, the differences start to add up.