Fabienne : Whose motorcycle is this?
Butch : It's a chopper, baby.
Fabienne : Whose chopper is this?
Butch : It's Zed's.
Fabienne : Who's Zed?
Butch : Zed's dead, baby. Zed's dead.

This repository was inspired by a series of six puzzles initiated on the Stratego.com web forum. Below a brief description and solutions to all six puzzles, presented in increasing level of sophistication (which is not entirely the chronological order).
The solution diagrams use . to denote an empty square, # as an inaccessible and impassable lake, B as a bomb, and 2 as a scout (which is 2nd in the ranking of the various pieces).

All solutions were generated by Microsoft's open scource Z3-solver, using its Python bindings (and NumPy for array manipulations). You can easily reproduce the analyses on a machine with Python 3 and the pip package installer:

git clone https://github.com/rhalbersma/zed.git
cd zed
python3 -m pip install virtualenv
python3 -m virtualenv .env
source .env/bin/activate
pip install -r requirements.txt

and you are good to go to run the various scripts in this repo's src folder. All the dependencies are handled for you through the virtual environment. Once you are done with the analysis, you can run

deactivate

to get back your regular development environment.

This puzzle was first posted (without answer) in February 2014 by forum member maxroelofs.
In November 2017, I posted the answer (at the time, using a brute force C++ program to confirm my hand-made solution).
The minimum number of bombs satisfying the constraints == 6.
Z3 finds the solution by direct minimization within 1 second.

. . . . . . . . . .
. B . . B . . B . .
. . B . . B . . B .
. . . . . . . . . .

This puzzle and its answer were first posted in February 2014 by forum member Napoleon 1er.
The link to the original answer no longer shows the solution diagram.
In November 2017, I posted the answer (at the time, using a brute force C++ program to confirm my hand-made solution).
The minimum number of bombs satisfying the constraints == 7.
Z3 finds the solution by direct minimization within 1 second.

. . . . . B . . . .
. B . . B . . B . .
. . B . . . . . B .
. . . . . B . . . .

In graph theory, this number is called the domination number.
In November 2017, I posted this puzzle and its answer (at the time, an unverified hand-made solution).
The minimum number of scouts satisfying the constraints == 8.
Z3 finds the solution by direct minimization within 1 second.

. 2 . . . . . . . .
. . . . . 2 . . . .
. 2 . . . . . . . .
2 . . . . . . . . .
. . # # . . # # . .
. . # # . . # # . .
. . . . . . . . . 2
. . . . . . . . 2 .
. 2 . . . . . . . .
. . . . 2 . . . . .

In graph theory, this number is called the the independence number.
This puzzle and its answer were first posted in February 2014 by forum user Napoleon 1er.
The link to the original answer no longer shows the solution diagram.
In November 2017, I posted the answer (at the time, an unverified hand-made solution).
The maximum number of scouts satisfying the constraints == 14.
Z3 finds the solution by direct minimization within 1 second.

. . . . . . 2 . . .
. . . 2 . . . . . .
. . . . . . . 2 . .
. . 2 . . . . . . .
2 . # # 2 . # # . 2
. 2 # # . 2 # # 2 .
. . . 2 . . . . . .
. . . . . . . 2 . .
. . 2 . . . . . . .
. . . . . . 2 . . .

This puzzle was first posted (without answer) in February 2014 by forum member maxroelofs.
In July 2018, I posted the answer (using the Z3-solver).
The maximum number of scouts satisfying the constraints == 18.
Z3 proofs N == 18 within 1 second, and disproofs N == 20 within a minute.
Direct minimization seems out of reach since Z3 does not recognize that N has to be even.

2 . . . . . . . . .
. . . . . . . . . 2
. . . 2 . . . 2 . .
. . 2 . . . 2 . . .
. 2 # # . . # # . 2
2 . # # 2 2 # # 2 .
. . . . . . . . 2 .
. 2 . . . . . . . .
. . . . . . 2 2 . .
. . 2 2 . . . . . .

This puzzle was first posted (without answer) in February 2014 by forum member The Prof.
In July 2018, I posted the answer obtained from private communication with computer scientist Wieger Wesselink.
This solution had been found by Wesselink in collaboration with his colleague Hans Zantema (using the Z3-solver).
The maximum number of scouts satisfying the constraints == 24.
My current Z3 script proofs N == 24 within 15 minutes, and finds no disproof for N == 25 within an hour.
The Wesselink-Zantema approach manages to proof/disproof N == 24/25 within 10 seconds each.

. . . 2 B 2 . . . . 
. . 2 B 2 B 2 . . . 
. . . 2 B 2 B 2 . . 
. . . . 2 B 2 . . . 
2 . # # . . # # 2 . 
. . # # . 2 # # . 2 
. . . 2 . B 2 . . . 
. . 2 B . 2 B 2 . . 
. 2 B 2 B . 2 . . . 
. . 2 B 2 . . . . .

The Z3-solver is easy to use, but also easy to misuse. In particular, it's hard to predict its performance.
A constraint rewrite, or even a reordering can induce a 10X speedup, or a 10X speed penalty.
The following open challenges are identified (pull requests welcome!):

• Make problem 5 amenable to direct minimization
• Push problem 6 to within the same ballpark as the Wesselink-Zantema approach

Apart from accepting answers to these challenges, this repo is in maintenance mode and no longer actively being developed.

Thanks to Wieger Wesselink for introducing me to the world of SMT solvers, for stimulating discussion, and for staying 100X ahead of me on the sixth and hardest puzzle.

Copyright Rein Halbersma 2018-2021.
Distributed under the Boost Software License, Version 1.0.
(See accompanying file LICENSE_1_0.txt or copy at http://www.boost.org/LICENSE_1_0.txt)