I have always been puzzled with the definition of NP: **N**on-deterministic **P**olynomial time complexity. A problem is in NP if it can be solved by an algorithm that runs in polynomial time on a non-deterministic Turing Machine, a computer that can “guess” which path to take toward the right answer when given a choice.

I never quite understood this, or managed to build a good intuition on how it worked. What does it mean to guess? If such a powerful computer could guess, why could it not guess the right answer to the problem right from the start? Why would it have to go through a polynomial number of steps?

This short post will show how a basic understanding of the List Monad helped me (and can therefore help you as well) building an intuition on how a non-deterministic Turing machine behaves, and how you can get a feel of how it would be to program one such computer, thanks to Haskell.

### Once upon a time…

A few weeks ago, a paper was published, which claims to have found the solution of the famous P vs NP problem. This got me interested in looking back at the courses of my long gone student past.

I ended up searching for an online course, and found this great video from Erik Demaine, a short but quite entertaining overview of P, NP and NP-completeness complexity classes. At 8 minutes 50 seconds in the video, he explains why the Boolean Satisfiability Problem (**SAT**) is in NP.

Here is the content for his board after the explanation:

guess: x1 = True or False guess: x2 = True or False ... guess: xN = True or False check if formula on (x1, x2 ... xN) is True or False

Now, **if you know about the List Monad, you should see it right there**, in front of you. This insight might give you an idea of what “a non-deterministic computer guess” could be. At least, it did for me.

Let us explore this below.

### Non-deterministic computation = List Monad

A lot of Monad tutorials start with the Maybe and List monads. Most good tutorials will also mention that the List Monad models **non-deterministic computations**. It sounds like it must somehow be connected to the NP non-deterministic Turing machine. Let us see how.

###### I see a Monad in your SAT NP proof

To understand the similarities between the board of Erik Demaine and the List Monad, let us translate the SAT NP proof from Erik Demaine into Haskell code. Thanks to the List monad, the translation is pretty simple.

Here is the original board he wrote:

guess: x1 = True or False guess: x2 = True or False ... guess: xN = True or False check if formula on (x1, x2 ... xN) is True or False

Below is our Haskell version. We added a function name, introduced an *or* to stop at the first result, but mostly, our task was to **replace occurrences of “guess” by the bind (<-) operator**:

satExample :: Bool | |

satExample = or $ do | |

x1 <- [True, False] -- "guess" is replaced by bind (<-) | |

x2 <- [True, False] | |

{- ... -} | |

xN <- [True, False] | |

pure (formula x1 x2 {- ... -} xN) |

So our List Monad bind operator is analog to the “guess” of a non-deterministic Turing Machine.

###### Back to List Monad tutorials

Now that we have seen the similarities, let us look for an online Monad tutorial and check the definition it provides for **non-deterministic computation**. If we pick this one from FP complete, we can read:

[..] non-deterministic computation. It’s the kind of computation that, instead of producing a single result, might produce many.

The connection with the definition of NP is not direct, but pretty close. A non-deterministic computation returns several results. A non-deterministic Turing Machine is able to magically pick a “good” result among theses results, by guessing which one will lead to one “yes” outcome (there might be many).

###### From exponential to non-deterministic polynomial complexity

Let us go back to our translation of the SAT NP proof in Haskell:

satExample :: Bool | |

satExample = or $ do | |

x1 <- [True, False] -- "guess" is replaced by bind (<-) | |

x2 <- [True, False] | |

{- ... -} | |

xN <- [True, False] | |

pure (formula x1 x2 {- ... -} xN) |

Executed on a usual computer, this function will explore the search space of all potential variable assignments for x1, x2 up to xN, and stop at the first one for which the formula returns a positive answer. This code has therefore an exponential time complexity.

But on a non-deterministic computer, and as explained by Erik Demaine, each guess can be performed in constant time. And these guesses correspond to the bind operator of the List Monad. So, provided *formula* runs in linear time, the **non-deterministic complexity** of our *satExample* algorithm is linear.

###### Estimating the non-deterministic complexity of an algorithm

Generalising to all decision problems (problems whose answer is either True or False) and to non deterministic computations, we can reason that:

*Given a non-deterministic computation*

**f**occurring inside the decision problem**D**, and returning a set of result**R**, a non-deterministic Turing machine is able to pick a value from**R**which leads to a “yes” answer for**D**(if it exists) in constant time.*In the List Monad, the non-deterministic algorithmic complexity of the statement y <- f x is therefore equal to the non-deterministic algorithmic complexity of f, however many results f may return.*

This gives us a way to estimate the **non-deterministic complexity** of an algorithm: we refactor the algorithm in Haskell in such as way that the List Monad bind operators becomes visible. Then we derive its complexity, by counting each bind operator as constant time assignments: O(1).

We can do this for SAT, as well as any other algorithm. Take your favorite search-like algorithm, write it using the List Monad, then you can visually estimate its complexity on an fantasized non-deterministic Turing machine of the future. I am not sure it is terribly useful, but hey, it is still fun.

###### Example of SAT

Let us look at the code of a complete (and completely naive!) SAT solver (*). Our solver takes as input an instance of a SAT problem **pb**, and returns if there exists an assignment of the variables that makes the formula True.

Our implementation has been refactored to make each bind operator of the List Monad visible:

sat :: SAT -> Bool | |

sat pb = or $ do | |

assignment <- forM (allVars pb) $ \var -> do | |

val <- [True, False] | |

pure (var, val) | |

pure (evalSat assignment pb) |

**allVars**extract all the variables from the SAT instance (normalised as a conjunction of disjunction)**evalSat**checks if the SAT instance is verified for a given assignment of the variables

Assuming the algorithmic complexity of *allVars* and *evalSat* are linear, and counting each bind operation as O(1) assignments, we can clearly see that the non-deterministic complexity of the *sat* algorithm is linear as well (there is a linear number of calls to bind).

The full code for this naive SAT evaluator is available in this GitHub Gist.

*(*): A real SAT solver would explore the search space by cutting branches early. It would use a clever ordering for the variable assignment, would use constant propagation to identify dead-end as soon as possible, as well as other clever tricks such as unit propagation.*

*The goal of all these tricks is to reduce the exponential exploration space. Interestingly, if we could ever have a non-deterministic Turing machine, we would not need such tricks. In fact, they would only slow down the algorithm.*

### Conclusion

It is funny how we can revisit a problem we already looked at several times, and yet suddenly see it from another perspective. A perspective which was there all along, in front of our eyes, but that we could not see.

It is also interesting to notice how expressive Haskell is. The do-notation and monads allows us to express different models of computation with ease.

Thanks to this, we can use Haskell to **experience how programming would look like in a different world**, in which we had a different kind of hardware to run our software.

And I really wished I could have a non-deterministic Turing machine at home.

Follow @quduval