P vs. NP: let's think out loud

We all know this question. It is listed as one of the seven millenium problem by Clay Mathematic Institute. We also know that most people believe that P is different from NP. For example, in the P vs. NP Poll by Gasarch (published in ACM SIGACT Newsletter), out of the 77 people who offered opinion, 61 believed that P is different from NP, 9 believed that P = NP, and others believed that the question is "formally independent" in some form. Well, what do you believe? If you are as yet undecided, I will try to unravel the reasons why most people believe that P is different from NP, and then speak about why it is equally reasonable to believe that P = NP. I will not talk about whether P vs. NP is formally independent of ZFC.

Two most common reasons for believing that P is different from NP are the following:

1. There are (literally) tons of problems which are NP-complete (i.e. if one is in P, and all will be in P), and nobody has been able to devise any polynomial-time algorithm for any of these problems. However, from our experience, we know that we are "good" at devising polynomial-time algorithms, but not very good at proving lower bounds. [Just look at all the great
   algorithms we have devised. Also witness that we can't even prove that satisfiability for propositional logic cannot be solved in O(n²).]
   
2. We can intuitively think of P as the set of problems for which we can produce proofs in polynomial time, and of NP as the set of problems for which, given a proof, we can check that it is indeed a proof in polynomial time. Well, from our experience with math, we know that producing proofs is usually much harder than verifying proofs.
   

Well, both of these reasons sound very reasonable. However, I also think that there are holes in these arguments (because of which, it is equally reasonable to believe that P = NP). Most people associate the complexity class P with the set of problems that we can solve "efficiently", and classify non-polynomial algorithms as bad (or inefficient) algorithms. [If you have done some computer science courses, you should see this immediately.] But this is a wrong assumption. For example, the Simplex algorithm for solving linear programming runs in exponential time in the worst case (I believe the same is true in average case), but the algorithm runs very efficiently in practice. There are also polynomial-time algorithms for linear programming, but it seems that none of those have outperformed the simplex algorithm in practice. Furthermore, the exponentiallity of the simplex algorithm's running time only occurs on some pathological examples that never appear in practice. On the other hand, there are many polynomial-time algorithms that do not actually run efficiently in practice. A counterexample for this (quoting Cook's paper) is due to a result by Robertson-Seymour that says that every minor closed family of graphs can be recognized in O(n³), but the hidden constant is so huge that the algorithm is inefficient in practice.

So, maybe there exist polynomial-time algorithms for satisfiability for propositional logic, it's just that the smallest exponents are so big (maybe bigger than the number of atoms in the visible universe, 10⁹⁰). [Of course, the time hierarchy theorem tells us that there is an problem solvable in n^k, but not solvable in n^k-1.] Perhaps, the smallest size of the polynomial-time algorithm that solve satisfiability for propositional logic already outnumbers 10⁹⁰. Who knows! Perhaps, we are good at devising efficient algorithms, but not so good at devising polynomial-time algorithms in general. Maybe the following question is more relevant: assuming that P = NP, give an upper bound on the size of the algorithm (by this I mean, multi-tape Turing Machine) that solves satisfiability in polynomial-time; does it necessarily consist 10, 100, or 10⁹⁰ states?

In a sense, if you're a practical-minded person, P vs. NP doesn't really matter at all, and there is technical reason why. Recall that the linear speedup theorem (look at Papadimitriou's Computational Complexity) says that if a problem is solvable in `f(n)`, then for any `epsilon > 0`, there exists an algorithm that solves the same problem which runs in `epsilon f(n) + n + 2`. So, if your algorithm runs in 2ⁿ, then just use this theorem to speed up your algorithm for all n that is relevant in practice. [Of course, if you check the proof, the size of the resulting algorithm grows quite so quickly in the size of `n`, that there is no way you can write your algorithm on earth. So, the practically-minded people will probably settle with heuristics instead.]

Anyway, I think that it is very possible [correction: 'very' -> 'equally'] that P equals NP, and the proof of which is non-constructive (or we may never actually find the proof, because the length of the shortest possible proofs exceeds the number of atoms in the visible universe).

Toronto's temperature: the extremes

The last couple of weeks have been quite hot in Toronto (mostly around 25 degrees C). I actually heard that this is unusually hot for September in Toronto. The humidity just makes it worse. You'll find yourself taking a shower three to four times per day.

Since last night, Toronto's temperature has cooled off quite a bit. Throughout today it's been around 18 degree C, just the perfect temperature. I wish it would be like this all year round. But that was just wishful thinking, because I have to be prepared for -20 degrees C in December and January. Actually somebody told me that during winter in Toronto, the wind can be quite strong. This will just make it worse ...

Favorite Logic of September 2005: First-order logic (1)

next

Some time ago I promised to make a series of postings on "My Favourite Logic of The Month" every month starting from September 2005. Well, here we officially start until we run out of "nice" logics.

Why first-order logic (FO)? It is the simplest non-trivial logic that we can use to express many mathematical statements. In fact, it is believed that first-order set theory is sufficient to axiomatize mathematics. Besides, most of you have already been exposed to FO, which will make my task much simpler. If any terminologies here sound obscure, check out preliminaries.

We will take a look at three aspects of FO: (1) the problem of testing satisfiability and finite satisfiability, (2) model-checking, and (3) expressive power. I am trying to cover topics that hopefully satisfy finite model theorists, and other logicians. In this posting, I will only speak about (1), saving the other two for some time next week.

Satisfiability: given an FO formula, test whether it is satisfiable. Well, what can we say about this problem with respect to FO? It is undecidable (actually r.e.-complete) [correction: complete for co-r.e, thanks to Richard Zach.]; this is a well-known result proven by Turing, which shattered Hilbert's dream to axiomatize mathematics. If you're into this kind of problem, check out the following book

The Classical Decision Problem by Grädel et al.

Actually, many fragments of FO are decidable, but most are provably intractable. The most complicated such result that I know of is Rabin's result of the decidability of monadic second order theory of infinite binary tree. [Whatever this means, but we may want to delve into this awesome result in the near future.] Although decidable, the problem has non-elementary complexity.

Finite Satisfiability: given an FO formula, test whether it has a finite model. I believe that this problem, if decidable, has more practical applications, e.g., databases. Unfortunately, this problem is also undecidable (actually complete for co-r.e.) [correction: complete for r.e.]. This result is due to Trakhtenbrot. Combining this result and that satisfiability is complete for co-r.e., we can readily imply that completeness theorem, which says that satisfiability is r.e. [correction: satisfiability is co-r.e., thanks to Richard Zach.], fails in the finite. Trakhtenbrot's result in fact marks the beginning of finite model theory. Later on, Fagin proved a logical characterization of NP with a technique that is "isomorphic" to that used to prove Trakhtenbrot's theorem (see this page). For more on finite satisfiability of FO, see Libkin's Elements of Finite Model Theory.

CAPTCHA

It stands for Completely Automated Public Turing Test to Tell Computers and Humans Apart. Although I still wonder why it is abbreviated CAPTCHA instead of CAPTTTCHA, it was (re)brought to my attention due to the spam I got for my posting yesterday. Anyway, CAPTCHA is developed by researchers from Carnegie Mellon University. Here is their main website. Briefly, the goal of CAPTCHA project is to use Artificial Intelligence to help internet security (e.g. to prevent spams). The underlying assumption behind CAPTCHA is that there are tasks that humans can do, but computers can't. For example, since I enabled the word verification (from CAPTCHA project), each time you wish leave a comment on this blog, you will be asked to read and verify a distorted text (which is an image file). Although the task seems trivial to humans, tasks like this are non-trivial for computers (at least for now). We don't know whether computers will someday possess our ''intelligence''. But CAPTCHA is one reason why a 'no' answer will have positive impact on our society.

Ironically, the distorted texts are actually generated by computers ...

Back!

Hello all! It's been quite some time since I blogged last. But I am happy to inform you that I can start blogging again on a regular basis.

A little bit about my summer internship in Los Alamos ... I'll start with my work in Los Alamos. I worked mostly on the complexity aspect of Sequential Dynamical Systems (SDS). Briefly, SDSs are a formal model of computer simulation (somewhat like cellular automata) proposed by Los Alamos researchers. I won't tell you more about it (if you are curious as to what they are, read this survey). Anyway, in retrospect Los Alamos was a nice place to visit. The scenery was awesome, the people were friendly, and you can do some cool research there. [Fortunately, what Jon said didn't happen to me or any of my friends.] The down side, however, is that there is pretty much nothing else in Los Alamos. The town is practically dead after 6 --- there is virtually nobody walking on the street. And ... to my surprise, there was no shopping mall whatsoever in Los Alamos. One has to go to Santa Fe, which is the closest biggest city to Los Alamos, to find the nearest shopping mall. Anyway, I will put some pictures from my stay in Los Alamos when I finish developing the pictures.

It is a nice feeling to know that I will be doing logic on a regular basis from this time onwards. I arrived in Toronto last Saturday to start my graduate studies. I haven't completely settled yet, but I couldn't help myself blogging again after the internet connection was set up in my apartment here. Incidentally, this week is Toronto's Computer Science Department's orientation week. I am so happy to meet many logicians here, including some of the most well-known ones. For instance, Moshe Vardi (Rice University) came to visit this Tuesday and gave a talk outlining the development of logic and how computer science was born. I, and I believe most people in the audience (including the non-logicians), found the talk extremely entertaining and insightful. As my advisor, Leonid Libkin, put it this morning, Vardi has the rare gift to be both a top-notch researcher and an excellent speaker. [As you and I know, most researchers who do great research are poor at explaining their research to others.]

Anyhow, that is all I have for now. As a final remark, I haven't forgotten about my favourite logic of the month and will write on it some time next week after I have completely settled.