travelling salesman problem - xkcd 399
If you are a programmer, it is likely that you have at least a vague understanding of what an NP-complete problem is; even if it’s just, “those really hard ones”.
What you may not know, is that, although NP-complete problems are difficult in general, a significant proportion of them are easy in practice and there are tools, called SAT solvers, that can efficiently solve this subset.
SAT solvers allow you to ask questions like, “does there exist an x such that y is true?”. This is incredibly useful for hardware or software verification since you can effectively ask, “is there an input that causes this invariant to break?”.
However, there are caveats. Since SAT solvers attempt to solve the SAT problem, it must be possible to translate your problem into a propositional expression. In practice this means that you can only verify properties about programs that don’t have loops or hardware that forms combinational circuits. (If you unroll your loops up to some fixed bound, you are doing bounded model checking).
Another limitation is that, although you can pose questions like, “does there exist an x such that y is true?” or “for all x is y true?”, you can’t ask questions like “does there exist an x such that for all y, z is true?”.
It turns out, although NP-complete problems are hard, there are more difficult classes of problems.
There is an interesting trend amongst the kinds of puzzles that people like to solve. Many of them are NP-complete, and conversely many NP-complete problems can be made into interesting puzzles.
In the same manner, many two-player games are PSPACE-complete. PSPACE is the class of problems that can be solved using polynomial space and PSPACE-complete problems are the hardest problems in PSPACE. PSPACE contains NP, so it is more difficult.
Just as the canonical NP-complete problem is SAT, the canonical PSPACE-complete problem is QBF and so a QBF solver is a tool to help you win two-player games (with caveats).
QBF has the same limitation as SAT in that, we still can’t express loops, so our two-players games must have a polynomial number of turns. In other words, we can devise strategies for tick-tack-toe, but not chess.
PSPACE problems are hard, but there are yet more difficult classes of problems. For example, chess belongs to a class called EXPTIME-complete.
Whilst SAT solvers have been widely adopted for real problems, QBF solvers have not. Progress is being made, but we simply don’t yet have QBF solvers that work effectively on large problems.
This is a shame since, if we did, we could do things like program synthesis; “does there exist a program, such that for all inputs, these invariants hold?”.
For my part, I’ve have been writing my own solver, which I hope to blog more about in the future.