Knights, Puzzles, and Hypermodels

I, being a huge nerd, am a fan of logic puzzles. One of the most famous ones is "Knights and Knaves": you have a bunch of statements from people, where statements from knights are always true and statements from knaves are always false. Like if we had

You see A and B. A says "we are both knaves".

If A was a knight, then it would be self contradictory, so A is a knave. But then the state "we are both knaves" is false, so B is a knight. A while back I wrote about using formal methods to solve these puzzles.

I also like making puzzles. I came up with a variation of Knights and Knaves called "Knights and Knaves Express", which I put up here. From the intro:

It's time to drag the Island of Knights and Knaves kicking and screaming into the 19th century! We're going to run a train. For these puzzles, you'll have a set of stations with possible connections, and you need to find a route that starts at one station, goes through every other station exactly once, and ends in a station. IE if our map was

 A -- B -- C
 |    |    |
 D -- E -- F

Valid routes might be A B C F E D, or A D E B C F, but A B E D C F is invalid. The ordering matters: A B C is a different route from C B A.

But also, every station is run by either a Knight or a Knave. The stationmaster has a set of requirements for the route. Knights tell the truth about their requirements, but Knaves always lie. You must plan the route so that every requirement by a Knight is satisfied, and every requirement by a Knave is unsatisfied. IE if we have

 A --- B
 |     |
 -- C --

If C says "I must come first", if C is a Knight, then the route starts at C. But if C is a knave, the route does not start with C.

The extra dimension gave me a lot of room to come up with interesting puzzles. But it also added a big problem. A well-designed puzzle should only have one solution. If we have three people, and each can be a knight or a knave, we have 8 combinations to check. That's not too bad to check by hand. If we then add in three connected stations, there's now 3!2³ = 48 combinations. Even if you're willing to check them all by hand, you can easily make a mistake and leave your puzzle "cooked".

I wrote an Alloy solver to check for solutions. If the model finder found only one solution, then the puzzle was good. But this was incredibly tedious, since Alloy can't tell me how many solutions it found in advance. To make matters worse, I wanted to write some puzzles where you only needed to solve for the route. IE you couldn't figure out unambiguously which station masters were knights and which were knaves, but you could uniquely figure out the station ordering. So multiple "models" were fine, as long as some subset of their structure was identical.

The more you push this, the worse Alloy gets. The problem here is that most formal methods deal with system properties, while this is a hyperproperty. Hyperproperties are requirements over the set of system behaviors. In this case it would be "all solutions have the same route." It's not enough to see one solution to see if this is true or not; you have to look at every single solution and make sure they're identical.

I've written a little about hyperproperties here. One solution we can do is "lift" the hyperproperty into hypermodel. Instead of speccing out "the puzzle", I'd spec out the "universe of puzzles". This could work but is a lot harder to do than a regular model and requires a lot more cleverness.¹ That tells me it's the wrong tool for the job.

What's the right tool? Constraint solving! A constraint solver takes a bunch of math equations and gives you solutions that satisfy them. What makes them appropriate here is that they can output multiple solutions really easily. This is because they're often used to minimax some value, so you want to see intermediate solutions as it finds better and better optimizations. Here we're not optimizing anything, but we can use the same machinery to spit out unique solutions.

The Spec

I'm using MiniZinc, which I've written about here. I'm sure there are better tools, but MiniZinc is what I know how to use, sorta kinda. Here's the spec.

include "globals.mzn";

int: N; % Changed per puzzle

% UNIVERSAL STUFF
% False represents a knave
array[1..N] of var bool: P; % People
array[1..N] of var 1..N: route; 
constraint alldifferent(route);

array[1..N] of var 1..N: location; % in route
constraint forall(i in 1..N) (location[route[i]] = i);
% Does a path exist?
array[1..N, 1..N] of bool: path;

% Valid route
constraint forall(i in 2..N) (path[ route[i-1], route[i] ]);
predicate claim(int: claimer, var bool: statement) = P[claimer] <-> statement;

% PUZZLE SPECIFICS GO HERE

solve satisfy;

output [show(if P[n] then "K" else "V" endif) ++ " " | n in 1..N] ++ [show(route)];

Going from top down: N is the number of people. P is an array of var booleans. Knights are represented by true and knaves by false. Being a var means it's one of the values the optimizer has to figure out, as opposed to N and path, which are fixed in the model.

route represents the final train path. So route = [2, 1, 4, 3] would mean that the train starts at station 2, then goes to 1, then to 4 and finally to station 3. The alldifferent constraint tells the solver every element of the array must be unique, and it can't pick something like [1, 1, 1] as a solution.

Since a lot of the stationmaster requests are about their relative place in the route, I added location as a helper value. location[3] is the 3rd station's place in the route. Using the example of route I gave earlier, that'd be location[3] = 4. route and location channel each other: solving one completely determines the other. I don't need both, but it makes writing constraints more convenient. I added a channel constraint to enforce this.

path represents which stations could be connected to which other stations. If route[1][2] is true, then the route can go from station 1 to station 2. In the representation, this means that [1, 2] could be a valid subsequence of route. This is enforced by the "valid route" constraint.

Then we get to the claims. I did a similar thing I did in the Alloy post. If person A makes claim X, then either A is a knight and claim X is true, or A is a knave and claim X is false. In other words, "A is a knight IFF X is true", which in MiniZinc is <->. Note the statement is var bool: since it may or may not be true, it's something we need to explicitly be solving for.

Finally, we have the output. This is where using MiniZinc really helps me. Right now i'm having it output everything about every solution, and if two lines are different then I know the puzzle is cooked. But I could also have it just output the route if I wanted to design a puzzle where that's specifically what you need to solve for.

In Practice

Let's take the first puzzle in the list:

At least one of the two stationmasters is a Knave.

A -- B

A: "Start at my station."

B: "End at my station."

We model the puzzle like this;

N = 2;

path =
[| false, true, |
   true, false|]; 

% A: Start at my station
constraint claim(1, route[1] = 1);

% B: End at my station
constraint claim(2, route[2] = 2);

% At least one Knave
constraint exists(n in 1..N)(not P[n]);

Then running it:²

.\minizinc.exe -a .\knights-knaves-express.mzn
"V" "V" [2, 1]

Let's try removing one constraint to show how it finds multiple solutions:

- constraint exists(n in 1..N)(not P[n]);

Now rerunning it:

 .\minizinc.exe -a .\knights-knaves-express.mzn
"V" "V" [2, 1]
----------
"K" "K" [1, 2]
----------
==========

So we know that requirement is necessary.

Hyperhypermodels

Now that I shaved my yak, I need to find a hairier yak. Showing that the solution is unique is all well and good, but that just makes a puzzle "valid". It doesn't make it interesting. What makes a puzzle "interesting" isn't something a machine can figure out, but there are some ways it can help. One "interesting" feature of a puzzle is that all clues are necessary to solve it. There are no clues you can take away and still have the same unique answer.

This is one step up from the hyperproperty. To tell if a puzzle is valid, we need to assert a property on the set of possible solutions. To tell if a puzzle has an independent basis, we need to assert a property on all possible solutions of variations of the puzzle. I don't think the constraint solver can help here.

I suspect we could check our hyperhyperproperty by writing a template program that generates all possible variations, runs the constraint solver on all of them, and checks to see if any two have the same unique solution. I've done something like this before. Alternatively, I can be satisfied with the MiniZinc model and rely on my human skills going forward. We have to stop automating somewhere.

If you're reading this on the web, you can subscribe here. Updates are once a week. My main website is here.

My new book, Logic for Programmers, is now in early access! Get it here.