Caleb Stanford


ProvableP vs ProvableNP


logic complexity-theory math

Introduction and Background

The versus question asks: is it possible to determine whether a Boolean formula is satisfiable, in time polynomial in the length of the formula? Determining whether a Boolean formulas is satisfiable is called the SAT problem, and programs which solve the problem are called SAT solvers. SAT solvers are used in many modern programming tools (usually, for automatically solving some system of constraints), so the SAT problem is of great practical importance today. And it is often suggested that a solution to “ versus ” would resolve whether there exists any efficient algorithm at all for SAT.

There are a number of reasons why this suggestion could be wrong, or at least, a number of ways to argue against it. But here’s a particular thought: what if (that is, SAT can be solved in polynomial time), but the polynomial-time algorithm is beyond our ability to find – and in particular, beyond our ability to prove correct? What if there exists some magic algorithm that happens to work, but there doesn’t exist any proof that it works? Or perhaps there doesn’t exist any proof that it runs in polynomial time? Such a scenario would be an unsatisfying resolution to versus , in a way: because practically speaking, we generally only trust algorithms that we can prove correct.

The question I’m trying to motivate is: does ? That is, what happens if we restrict our attention to algorithms which can be proven correct? Is this question answerable, or is it just as hard as versus ?

Summary

It turns out that if and only if . I’ll define what I mean by and . This post is adapted from a question and answer I made on Computer Science StackExchange.

The ProvableP versus ProvableNP question

Fix a logic that is strong enough to encode statements about Turing machines. By this I mean the same requirements as Godel’s second incompleteness theorem; but for the purposes of this question, just assume the following:

  • is consistent (it doesn’t prove False); and

  • implies the Peano arithmetic axioms of (PA).

Then define

There’s an issue with this definition: how do we encode languages (of which there are uncountably many) as finite objects in order for the logic to have something to say about them? In particular, how do we encode formulas for and ? Let us assume that languages are subsets of the natural numbers , and that any in or must be given by an arbitrary formula of the symbols of , i.e. it is any definable subset of .

From the definition we have that . But does ? How does this relate to the original vs question?

The Answer

Obligatory warning: to my knowledge, this proof has not been rigorously checked by someone else :) But we now argue that

For the forward direction, assume , and consider any language in . Note that is accepted by a nondeterministic Turing machine , such that there exists a polynomial which bounds the longest execution branch of on input a string of length . Then let be a nondeterministic Turing machine with the following description: first, count the input length ; second, calculate ; and finally, runs for at most steps nondeterministically. If doesn’t halt (this never actually occurs, but doesn’t know that for sure), rejects.

Now observe that (more specifically, PA) proves that runs in time . Moreover, can describe “the language of strings accepted by ” by a formula (roughly, “there exists an sequence of configurations such that the sequence is a run of and ends in an accept state”). Then we have that proves . Therefore, . But we know (even if doesn’t) that by construction. So . But , so .

The backward direction is a similar trick. Assume and that . Then , so . From here, we know there is some Turing machine and polynomial such that runs in time and . Let be a deterministic Turing machine which, on input of length , first calculates , and then runs for at most steps. If doesn’t halt, returns a default value, say .

Then similarly to before, proves that halts in time and therefore that . it follows that , but we know (even if doesn’t) that . Thus, .

Coq Logo Vector Image


research miscellaneous

If you’re familiar with the Coq proof assistant, you may recognize their logo (a brown rooster shape). However, it’s difficult to find a good (high-resolution) image of their logo online — the image file on their website is a sad 66x100 pixels. Probably not good enough for use in a presentation or poster.

I made a vector version of the image (actually in September 2017) which I’m posting online now. This was made in Inkscape. The lines may differ very slightly from the original logo. I hope someone finds this useful!

Vector image (SVG):

Coq Logo SVG

500x804 image (PNG):

Coq Logo 500x804

1000x1607 image (PNG):

Coq Logo 1000x1607

Traal -- Deciphered Scroll Messages


games

It happens to be an appropriate day of the year to share this short and elegant puzzle game: Traal by Alan Hazelden and Jonathan Wighting. (Also, if you like difficult elegant puzzle games, check out Alan Hazelden’s page. A Good Snowman Is Hard To Build is probably one of my favorite puzzle games on Steam.)

Actually, the reason I’m posting isn’t just to share some cool puzzle games; it’s because I googled for the deciphered texts of the scrolls in Traal, and couldn’t find anyone who had posted them. So, here they are (spoilers below).

There are 11 scrolls in the game. Here is what a scroll looks like:

Traal scroll

Deciphered Scroll Messages

Spoiler:

1. THE LAST PERSON TO FIND THIS WAS IMPALED WHILE GETTING OUT.

2. BEWARE STRANGER THIS IS AN EVIL PLACE NO GOOD WILL HAPPEN HERE.

3. ONLY A FOOL WOULD SUFFER GREAT DANGER FOR LITTLE GAIN.

4. THESE SCROLLS WILL NOT HELP YOU THEY EXIST FOR MY AMUSEMENT ALONE.

5. SOMETIMES ONE WILL SEE MORE WHEN ONE ONLY LOOKS AHEAD.

6. BROKEN GLASS CUTS DEEP AND NOTHING HERE CAN FIX IT.

7. THREE WISE EYES SEE NO EVIL SEE NO EVIL AND SEE NO EVIL.

8. EVIL TWINS ARE TWINS IN EVIL.

9. WHEN ALL EVIL FACES YOU WEAR ONLY DARKNESS.

10. AN END AWAITS YOU BEYOND HERE BUT IT IS NOT A PRETTY ONE.

11. WHATEVER YOU DO DO NOT COLLECT ALL OF THESE SCROLLS A TERRIBLE FATE AWAITS.

All of the messages are related directly to the rooms they are in, except for scrolls 2 and 4:

1. This is the scroll hidden behind the fake spikes and spike maze. Hence the (accurate) message about getting impaled on the way out.

3. This is the scroll in the optional side room. Hence, "great danger for little gain".

5. This is in the crossroads room that you can get through by only walking ahead.

6. This scroll is blocked behind a bunch of glass that you have to break.

7. This is in the room with three mushroom-shaped enemies ("three wise eyes")

8. This is in the room with two mushroom-shaped enemies ("twins").

9: This is in the room that requires a blindfold to get past (blindfold = "wear only darkness").

10 and 11: These two are in the room just before the end, so they warn you about your fate.

The scrolls are just cryptograms (each English letter is represented as a certain symbol). So you can solve them with an online cryptogram solver, but the time-consuming part is reading the symbols and writing down an arbitrary letter for each symbol, so that you can input that into a solver. Also, the words on the scrolls wrap from one line to the next, so you have to figure out which line breaks to remove.

Older Posts »