What does this prove?

Question

Unfortunately, this image is too big for me to provide a transcription.

Hint:

LOK

Additional hint:

What is something that people like to prove for with games?

Last hint:

3-SAT

Hint:

Solving does not require the colors; the colors aid in helping you.

Hint:

This image proves that the puzzle game LOK is NP-complete by reducing it to 3-SAT.

Since the hint is given, a viable solution must explain how it works.

Answer 1

As explained in the hints, the diagram suggests a proof that the puzzle game LOK is NP-hard, by showing how to encode an arbitrary instance of the NP-complete problem 3-SAT as a LOK puzzle.

A LOK puzzle takes the following form:

• There is a grid of cells. A cell can be absent, or blank, or blacked out, or contain a letter, or contain a wildcard.
  • We will not need wildcards in the proof and I'll ignore them from now on.
• In most LOK puzzles the goal is to black out all the non-absent cells.
  • But not, as it happens, in the ones used for this proof; see below.
• The rules take the form "if such-and-such a pattern appears in the grid, you can black out the cells in the pattern if you also do such-and-such".
  • Several of the rules are never used in the proof, and I shall ignore them.
• The other way to solve a LOK puzzle, besides blacking out all the cells, is to find and black out the word GRIVA.
  • Note that this word almost appears in the diagram given.

The rules we will need are as follows:

• A "word" is formed as follows.
  • Start in a letter-containing cell of the grid.
  • Head north, south, east, or west.
  • Pass over absent or blacked-out cells.
  • If you reach a cell containing an X, you may keep going or turn 90 degrees left or right.
  • If you reach a blank cell, you must stop.
  • You may stop at any other time, and the "word" consists of all non-X letters encountered along the way, in order.
• If the word LOLO appears in the grid, you may black it out provided you also do the following:
  • Find some southwest-to-northwest line of cells.
    • At least one cell on this line must be neither absent nor blacked out.
  • Black out all non-absent cells along the line.
• No letter has any other game-relevant effect besides what has already been described.

And the idea of the proof is as follows:

• In our initial grid, the word GRIVA is almost there but not quite: we have GRIV but the A is missing.
• There is an A elsewhere in the grid.
• We can form GRIVA, and win, if and only if we are able to set up a path from the end of GRIV to where the A is.
• There are absent cells and Xs that would let us do it, except that there are other letters (in this diagram they are all Z) in the way.
• Our goal is to black out all those Zs.
• Things are set up so that we can do that iff we can find a "satisfying assignment" for -- i.e., solve -- the corresponding 3-SAT problem.

So I'd better explain what 3-SAT is. It concerns logical formulae built out of variables and the operators and, or, and not. You should think of the variables, and the formulae built from them, as propositions that can be either true or false. Any variable, on its own, is a formula. (The formula is true if and only if the variable is.) If "F" is a formula, then "not F" is also a formula, true precisely when F is false. If "F" and "G" are formulae, then "F and G" and "F or G" are also formulae, and you can guess when those are true. We also use parentheses to disambiguate the order in which the operations are performed, like in algebra.

The Boolean satisfiability problem (SAT for short) is: given a logical formula, is there a way of making the variables true/false that makes the whole formula true? (If so, then we call such a way of picking true/false for the variables a "satisfying assignment", and we say that the formula is "satisfiable".) For instance, if A and B are variables, then "A and not B" is satisfiable, by making A true and B false; but "A and not A" is not satisfiable.

So far as anyone knows, there isn't an efficient way to determine whether a given formula is satisfiable. (There is a standard way of making that statement precise, but the details aren't important here.)

The same remains true if we restrict the allowable formulae as follows. (1) They are all in "conjunctive normal form". (2) Each "clause" in the conjunctive normal form has at most three "literals" in it. I'd better explain what all that means.

• A literal is either a variable, or "not" in front of a variable.
• A CNF clause is a bunch of literals joined with "or".
• A formula is "in conjunctive normal form" if it is a bunch of CNF clauses joined with "and".

We call a satisfiability problem where the formula is in conjunctive normal form with at most three literals per clause an instance of "3-SAT".

Why would anyone care about this stuff? It turns out that there's a very wide range of types-of-problem with the properties that (1) no one knows an efficient way to solve any of them, but (2) if there is an efficient way to solve one of them then we can turn that into an efficient way of solving any of the others. SAT is one of these. So is 3-SAT.

And, finally, the point of this question is that the game called LOK, or even the simplified and stripped-down version I've described above, is also one of these. The part of that statement that's more difficult to prove is that if you can determine efficiently whether any LOK game is winnable then you can also determine efficiently whether any 3-SAT problem is solvable.

I indicated above that we were going to set things up so that the obstacle to winning the LOK game is that there are a bunch of Zs getting in the way of a path that would let us spell out GRIVA and win. So the idea is going to be that each clause in our 3-SAT problem corresponds to a set of Zs, with one Z for each literal in the clause; and then we will be able to join everything up provided we can black out at least one Z from each set.

We will do the blacking-out using LOLOs: we'll have as many instances of LOLO as we have variables, and arrange that for each variable V we can black out either all the Zs corresponding to "V true", or all the Zs corresponding to "V false", with a single LOLO: that is, we'll put all the V-true literals on one diagonal line and all the V-false ones on another.

Finding a satisfying assignment means making every clause in our 3-SAT instance true. Each of those clauses can be true in up to three ways (that's the 3 in 3-SAT). So what we'll have is a bunch of sets of up to three "parallel" connections, arranged so that we can join the A to the GRIV precisely when each set-of-up-to-three connections works out.

With that overview in mind, let's take a look at the diagram and see how it's been done in this case. Look first at the groups of three Xs at top and bottom, which have helpfully been coloured in four shades of blue. Each pair-of-groups-of-three is one of our parallel connections, corresponding to one of our 3-SAT clauses. In this case each clause has exactly three literals. These are the Zs in between the blue Xs at top and bottom; they too are shaded, the same way as the clauses they're part of but brown rather than blue.

The path joining GRIV to A, if there is one, is going to end up running from the bottom-left Xs, up through a lightest-brown Z to the top-left Xs, then across to the next set of Xs at the top and back down through a second-lightest-brown Z to the bottom, then across to the next set of Xs at the bottom, then up through a second-darkest-brown Z to the top, then across to the last set of Xs at the top, down through a darkest-brown Z to the bottom, and from there to the A.

There is no other way to get from the bottom-left Xs to the A. Doing this requires us to black out one of the Zs from each "triple column". So far, so good. So where exactly do we put our blocking Zs? Answer: for each variable we choose two SW-to-NE diagonals, all different. One of the two is for literals that are just the variable. The other is for ones that are NOT-the-variable. And we have as many LOLOs as there are variables.

But how do we make sure we use just one LOLO per variable? (Suppose our formula is "(A or B) and (not A or not B)"; this formula can in fact be satisfied legitimately, but we don't want to let it be "satisfied" by taking both A and not-A. So we had better construct our LOK puzzle in a way that doesn't allow that.)

Each of those pairs of diagonal lines corresponds to one variable. Let's say the upper line is for "A" and the lower for "not A". Notice that each pair of diagonal lines (that we might black out one of using a LOLO) passes through a pair of Xs near the southwest, which I've highlighted here. If we take both A and not-A for any variable, we'll destroy both Xs in one of those pairs. So let's think some more about what the path from GRIV to A actually has to look like.

(But first, I might as well say explicitly what formula is being represented here: calling the variables A, B, C, D from top to bottom, and using the convention that "A" comes above "not A", it is: (not-A and B and not-C) or (A and B and D) or (A and not-C and D) and (not-B and C and not-D).)

I've now shown the only way a path can get from GRIV to A. It can use either the upper or the lower Xs in each of those horizontal segments, but if both are unavailable then the path is blocked.

So now we can describe the whole recipe. Given a 3-SAT problem, we construct:

• Groups of Xs at top and bottom, one pair of groups per 3-SAT clause, one X in each group per term in the clause. Staggered as shown in the diagram. The layout here works if the number of clauses is even; if it's odd, the simplest adaptation is to have one extra group of Xs to transfer from top to bottom.
• Same structure as in the southwest corner of the diagram, with one LOLO-structure per variable.
• Diagonal lines through the Xs as in the diagram, each pair of diagonal lines corresponding to one variable.
• For each term in each clause, put a Z in the column determined by which clause and which term, and in the diagonal line determined by which variable and whether it's negated.

The resulting LOK puzzle is doable if and only if the original formula is satisfiable.