Sunday, July 11, 2010

I happen to have no dress in my cabin.

I've spent the weekend watching my computer solve 3-SAT problems, and trying to make it go faster.  I think I got the 75-variable instances down to 2 hours.  Thats a lot better.  While I was waiting for these two finish, I decided that it would be a great idea to play with some Legos.  I have long avoided bringing any Legos into my home, because they are incredibly addictive.  But, concentrating on a problem for long periods of time seems to erode my common sense.


I went to a store and bought a tiny, inexpensive ($6) set, a Lego car, and built it.    I don't like the fact that you can't put a little Lego person inside, but I do like the way it looks.Here is a picture:


















And then I build this Pirate ship:



They have a lot of fancy new pieces and fancy new colors now.  Still ridiculously expensive.  I bought it because I've never owned a "big" pirate ship--I only had like a small pirate interceptor.  And technically it isn't a pirate ship because it is the red coats ship, or whatever.  The lego store didn't have any ships flying the jolly roger.  While it is big by Lego standards, it is actually kind of small by mine.  For one thing, they didn't bother putting cannons on the top deck.  Why would you go to the trouble of having a lower deck if not more room for cannons?  Also, I'd like to a bigger superstructure, with walkways instead of ladders, etc.  Maybe four times as many cannons.  This thing...it can be a scout.

Anyway, my 3-Sat algorithm, Ultimatum, is kicking ass.  It can solve any satisfiable instance fairly quickly, and the unsatisfiable ones are getting knocked out in polynomial time.  I still don't understand why it works, and I didn't do much work in that direction over the weekend because I focused entirely on making it not take forever.  A 50-variable problem took like a minute, and a 75-variable problem took six hours.  Thats not very handy, espeically since right now I believe the biggest threat to the polynomiality of Ultimatum is the larger problem instances.  After some optimizations a 50-variable problem now runs in two minutes, and a 75-variable one takes two hours.  I'm gonna call that progress.

My next steps are uncertain.  I am dying to publish or at least share my discovery with the rest of the world but I feel like I can't, or shouldn't, until I can prove why it works.  I've had a number of ideas about how to prove that Ultimatum is polynomial and they all turned out to be stupid.  I am actually considering giving up, again, and for a little while, because I'm probably going to need to hit this thing from a fresh angle.  Also, I still don't believe that I've actually solved it.  This time I have actual evidence before my eyes, but I have oscillated between thinking that I have it and realizing that I don't far too often to believe it.  Except for when I was standing in the Lego store, trying to convince myself to buy the pirate ship.  Turns out telling yourself that you are going to be famous and get a million dollars is enough blow $180 on a plastic toy for children.  Silly, I know.  Be proud of me; the Taj Mahal was $300.

I could make my own test problems, sure, but the whole exponential nature of NP-Complete problems makes it difficult to test anything more than 30 variables.  So for now I'll just lay low and make sure I can solve every problem in satlib.  And then, when my brain has a chance to rest, maybe I will overdose on caffeine for a week and try to figure out what the proof is.

I heard that people proved something about graphs of a certain size (4?) always being planar by simply enumerating every possible graph of size four.  Maybe I could do that?  Probably not.  Enumerating every 3-sat problem is intractable.

Wow.  Legos are so damn expensive Amazon has my ship I just bought for only a cent cheaper.  I think I'm going to build an armada.  If I can afford it.  This sucks.  The sets I wanted as a kid are like twice the price now, since they only ever ran for three years.  Whatever.  I'm gonna go play with my pirate ship.  Wait!  I need another one.  It needs a friend.  To battle.

When I worked at Neoquest there was this pirate game you could play.  It involved punching shapes out of cards and building tiny cardboard ships.  And there were dice involved.  Some of the images in this search link show them.  I want to find a copy of that game so I can read the rules--maybe we could make a Lego version of it.  I like this idea because I could then maybe rationalize buying every Lego pirate ship every made.

[Edit]
You can thank Evan for this link.

No comments:

Post a Comment