Computational Complexity and other fun stuff in math and computer science from Lance Fortnow and Bill Gasarch
Saturday, November 05, 2005
Bringing Complexity to Your iPod
Welcome to ComplexityCast, the first of a very occasional podcast, an
audio version of this weblog. First up, Bill Gasarch and I talk
about the P versus NP problem. Download the MP3
(3.4MB, 20 minutes) or subscribe to the Podcast Feed.
That was great! Also, it's a very interesting forum for things that you wouldn't see in a blog post, a book, a paper... or basically anywhere else other than being right next to professors talking.
At my undergrad college we would have departmental teas and I got a lot from it, just finding out what professors talk about and what they consider interesting.
That was a lot of fun. I loved the comment about how we should have papers which say 'Here is a lame result - but it doesn't naturalize!' and agree wholeheartedly.
I've long been fascinated by the question of whether there's a general technique for proving NP-complete problems unsatisfiable other than using a backtracking algoritm. After much cogitation, the only technique I've come up with is a slightly bizarre one involving linear programming. Specifically, if the sum of a bunch of values must be at least (for example) 57.3, and each of those numbers must be exactly 0 or 1, then the sum must be at least 58, and that can be thrown in as a new constraint.
This technique hasn't (yet) been demonstrated to actually solve anything faster than other techniques can, but I would hope that any result based on it, even for a very artificial problem, would be viewed as publication-worthy for sheer novelty value.
Note to anonymous: You don't need an iPod to play it. It's an MP3 and if you're using a web-browser right now you are more than likely to have the capacity to play MP3s.
Note to anonymous: You don't need an iPod to play it.
I know. But I am less inclined to sit at my desk listening to a 10 minute podcast, than I would be to listen to it while walking (if I had an iPod). And I could skim through a transcript in about 1 minute. =)
Why do you want Lance to waste his time transcribing the mp3 file? Why don't you listen to it at your desk and transcribe it so that the rest of us can read it. Maybe next time someone else will return the favor.
The technique you mention is studied as part of the 'cutting planes' approach to propositional proofs and satisfiability. It is a respected technique about which there are many important open questions.
Combining cutting planes ideas with backtracking methods is an area of current research on satisfiability programs. Limited special cases are used in current 'pseudoBoolean solvers' using backtracking algorithms and there are more general applications of integer programming algorithms using these and other ideas. Making really good use of these ideas is still wide open.
There is also research on using the kind of inferences you described for proving UNsatisfiability. Pudlak showed that it can be exponential to write down such cutting planes proofs for a specific family of formulas but there is still a great deal to be learned about its general utility as well as related cutting planes methods such as polynomial threshold or Lovasz-Schrijver proof systems which involve higher degree inequalities.
To get an idea of the variety of approaches to satisfiability there is an old 1996 survey due to Gu, Purdom, Franco, and Wah that lists a large number approaches and gives many references. (From a practical point of view take the runtimes listed with a grain of salt since current solvers are orders of magnitude faster than those considered in 1996.)
But Scott, would you get excited if someone produced evidence that your technique can't naturalize?
Paul, thanks for the link, although I know about a fair amount of that stuff already (I was the one who came up with walksat). The technique I have in mind isn't cutting planes, it's an approach for proving problems unsatisfiable (people do keep thinking it's cutting planes though). Basically, you find a minima, round up, throw that in as a new constraint, and repeat until all the round-ups have resulted in there being no solution at all.
The difficulty comes from how 3sat problems can be solved with any variable set to anywhere from 1/3 to 2/3, so if you have, say, 100 variables, roundups will typically be from 33 to 34 at best, and that's across all variables - if you do minima involving only a subset of variables it tends to smush all the weirdness to the un-minimized ones, resulting in a roundup from 0 to 1 or 1 to 2. The measure of the space removed by such roundups is so small that they don't converge on a solution.
My thought is that one can avoid such difficulties by concentrating on the only slightly artificial problems where there are clauses of the form 'of this assignment to all variables, at least half are correct'. One of these days I'll have to figure out how to get Python's linear programming bindings working (I'd have done this experiment years ago, but I haven't had access to a decent LP package)
this comment is not related to the iPod post, it is just about a new name to our area. what do you say about: "digital machine engineering"? or just digital engineering?
English is not my native language, and besides I can read every word of this blog, I can't understand all words of that cast... If you got a transcript, send to me, please? my mail is osias AT hotmail.com.
PS: If you want, I can pay you transcribing/translating any Brazilian song you want...
Cool! I'm sure this will add texture to your coverage of Complexity.
ReplyDeleteThat was great! Also, it's a very interesting forum for things that you wouldn't see in a blog post, a book, a paper... or basically anywhere else other than being right next to professors talking.
ReplyDeleteAt my undergrad college we would have departmental teas and I got a lot from it, just finding out what professors talk about and what they consider interesting.
That was a lot of fun. I loved the comment about how we should have papers which say 'Here is a lame result - but it doesn't naturalize!' and agree wholeheartedly.
ReplyDeleteI've long been fascinated by the question of whether there's a general technique for proving NP-complete problems unsatisfiable other than using a backtracking algoritm. After much cogitation, the only technique I've come up with is a slightly bizarre one involving linear programming. Specifically, if the sum of a bunch of values must be at least (for example) 57.3, and each of those numbers must be exactly 0 or 1, then the sum must be at least 58, and that can be thrown in as a new constraint.
This technique hasn't (yet) been demonstrated to actually solve anything faster than other techniques can, but I would hope that any result based on it, even for a very artificial problem, would be viewed as publication-worthy for sheer novelty value.
How about posting a transcript for those of us without iPods? (Wishful thinking, I'm sure...)
ReplyDeleteNote to anonymous: You don't need an iPod to play it. It's an MP3 and if you're using a web-browser right now you are more than likely to have the capacity to play MP3s.
ReplyDeleteNote to anonymous: You don't need an iPod to play it.
ReplyDeleteI know. But I am less inclined to sit at my desk listening to a 10 minute podcast, than I would be to listen to it while walking (if I had an iPod). And I could skim through a transcript in about 1 minute. =)
Dear Anonymous,
ReplyDeleteWhy do you want Lance to waste his time transcribing the mp3 file? Why don't you listen to it at your desk and transcribe it so that the rest of us can read it. Maybe next time someone else will return the favor.
Anonymous-who-wishes-for-a-transcript,
ReplyDeleteClearly you haven't heard Bill Gasarch speak. You don't know what you're missing...
anonymous-who-wants-a-transcript is a retard. you can't skim a 20 minute recording in a minute.
ReplyDeleteBram,
ReplyDeleteThe technique you mention is studied as part of the 'cutting planes' approach to propositional proofs and satisfiability. It is a respected technique about which there are many important open questions.
Combining cutting planes ideas with backtracking methods is an area of current research on satisfiability programs. Limited special cases are used in current 'pseudoBoolean solvers' using backtracking algorithms and there are more general applications of integer programming algorithms using these and other ideas. Making really good use of these ideas is still wide open.
There is also research on using the kind of inferences you described for proving UNsatisfiability. Pudlak showed that it can be exponential to write down such cutting planes proofs for a specific family of formulas but there is still a great deal to be learned about its general utility as well as related cutting planes methods such as polynomial threshold or Lovasz-Schrijver proof systems which involve higher degree inequalities.
To get an idea of the variety of approaches to satisfiability there is an old 1996 survey due to Gu, Purdom, Franco, and Wah that lists a large number approaches and gives many references. (From a practical point of view take the runtimes listed with a grain of salt since current solvers are orders of magnitude faster than those considered in 1996.)
Paul Beame
But Scott, would you get excited if someone produced evidence that your technique can't naturalize?
ReplyDeletePaul, thanks for the link, although I know about a fair amount of that stuff already (I was the one who came up with walksat). The technique I have in mind isn't cutting planes, it's an approach for proving problems unsatisfiable (people do keep thinking it's cutting planes though). Basically, you find a minima, round up, throw that in as a new constraint, and repeat until all the round-ups have resulted in there being no solution at all.
The difficulty comes from how 3sat problems can be solved with any variable set to anywhere from 1/3 to 2/3, so if you have, say, 100 variables, roundups will typically be from 33 to 34 at best, and that's across all variables - if you do minima involving only a subset of variables it tends to smush all the weirdness to the un-minimized ones, resulting in a roundup from 0 to 1 or 1 to 2. The measure of the space removed by such roundups is so small that they don't converge on a solution.
My thought is that one can avoid such difficulties by concentrating on the only slightly artificial problems where there are clauses of the form 'of this assignment to all variables, at least half are correct'. One of these days I'll have to figure out how to get Python's linear programming bindings working (I'd have done this experiment years ago, but I haven't had access to a decent LP package)
this comment is not related to the iPod post, it is just about a new name to our area. what do you say about: "digital machine engineering"? or just digital engineering?
ReplyDeleteDear Anonymous-who-had-no-iPod.
ReplyDeleteEnglish is not my native language, and besides I can read every word of this blog, I can't understand all words of that cast... If you got a transcript, send to me, please? my mail is osias AT hotmail.com.
PS: If you want, I can pay you transcribing/translating any Brazilian song you want...
Ahh, there's nothing quite like a enjoying a spirited discussion of P v NP while driving to work. Thanks guys.
ReplyDelete