The Ghost in the Serif

So do, I warn you
I see things when I hold you
But I’ve whispered: "it’s alright"
It is you and me and a long night

You're a ghost in the doorway,
I can see through, but I hold tight,
I’ll just stay on holding until it hurts,
I just want you to know you're lovely

Kryptonite is an amazing song.  My band started playing it, and for once I'm doing the riffs and not just playing rhythm.  Something came over us--at least two of us--when we played that song.  I experience a pronounced, special sort of feeling of pure joy the first time I played a song with other people.  It was Gambler, and it was months ago with mostly the same people I play with now.  When we played Kryptonite together last practice, at just the moment the song started to mesh together, I experience that feeling all over again.  Some songs are more fun to listen to;  some songs are more fun to play.  Kryptonite is both.  And I can play the solo!  But no, back to "something came over us."  It was probably measurable empirically, because we noticed it while playing the next song, "I'm Just a Girl" by No Doubt.  Typically I have difficulty playing the riff up to tempo, but when we played it will all of the energy we had just after playing Kryptonite, something was very different.  I didn't have trouble with the riff at all--not until I started thinking about it.  My fingers were flying over the strings, and everything felt very...light to the touch.  It was as if previously I had been smacking trees with a bat, and now I was just tipping strands of grass over with a feather.  I've been excited before, but in this particular case I experience a marked improvement in my skills.  Oh, and so did our drummer.  Our vocalist and guitarist didn't say anything;  they probably thought we were crazy.

Doctor Who is a show that I am watching now.  Sometimes the faces of all the past lives flash on the screen.  Sometimes the faces of all the girls I've loved, or nearly loved, flash in my mind.  I have a new one to add to the list.  I have no ill will towards her--I hope that she goes on and has an amazing life and that everything she hopes for comes true;  I just wish it hadn't ended the way it did, and that I could have been a better boyfriend, and that I wouldn't feel the way I do now.  I realize, once again, probably, that feelings of sadness for that person don't completely go away.  They just become another ghost in the corner of your eye that you pretend you don't know is there.

My Research is at a standstill.  Actually its not, but it feels that way.  I'm not generating or solving 3-SAT instance right now.  I'm acquiring hardware and figuring out the most boring of details involved in generating a trillion instances.  I have been pretty hairbrained since my last post, going back and forth about which way to do it--my hardware? ec2? azure, since I work there?  Should I write another generator in Ruby so its easier to run in linux--oh wait, theres mono?   For now, I've settled on playing with a some new toys I bought for myself, and we're gonna see if I can get some generators running 24/7.  Then, I hope to investigate running a SAT generator on GPUs.  Then, once I have all that worked out, I'm going to start reading the existing SAT research.  Actually I already started, but I'm going to put effort into it.  All I know so far is c/v = 4.26 and something I don't understand about c = v^(3/2).  After that, when we get to the last 700 million instances or so, I'll spin up EC2 or Azure instances.  And then figure out a proof?  Or prove myself wrong.

[Edit]
Fun fact:  this post has been classified as "pornography" by the genius web filter installed in the offices of a certain large software company.

The Angels Have the Phone Box

What is the absolute most important thing to be concerned about when trying to prove P=NP?  Is it the rigor of your mathematical proof?  The soundness of your implementation?  The depth of your testing?  Is it the peers who review your work?  Your sample size?  No.  It is none of these things.  The absolute most important thing you need to worry about is making your implementation play the "Job's done!" clip from the video game Warcraft II [1] [2] [3] [4].

Now that...hey it just finished another batch!  Anyway, now that...now I forget what I was going to say in this paragraph.

Generating a million instances for a SAT instance with 16 variables (and running a brute-force solver to count the number of solutions for each one) took more than a day.  So, obviously ramping that up by a thousand is going to take years.  I don't want to be one of those guys that spends ten years on a hair-brained polynomial time algorithm to post on the internet and get laughed at.  I want to be the guy who spent slightly less than maybe a month on a hair-brained polynomial time algorithm to post on the internet.  Corollary:  I don't have a thousand computers.

I do have one desktop with 4 cores, an old desktop with fried video cards thanks to my bitcoin endeavours, an old eepc that was filled with viruses because of unprotected surfing, and an apple air that I bought to make working from home more productive shortly before finding a new job at possibly the only company on the planet where I am never going to be able to work from home on a computer made by apple.  Oooh!  There it goes again!

Anyway, ...once again I forget--oh right.  So one idea I have, partly thanks to my failed bitcoin experiments (never spend a thousand dollars on top of the line graphics cards that each require two power connectors and then try to save $40 on a cheap power supply two weeks before the bitcoin market crashes), is to write some cuda (or whatever) code and use some GPUs to do the work.  The difference between the CPU and GPU for bitcoin mining was incredible, and I believe that SAT could be equally paralellizable.  I would want to be personally, absolutely certain that I was right about this thing before doing that, though, because that is a lot of work an I'm lazy.


Anyway, I think I'm going to break down the trillion problems into four categories:

1. Breadth Testing:   Tiny problems (16ish variables) - SAT and UNSAT instances - c/v in [2.5,6.02] ?
2. Breadth Testing:   Small problems (20ish? variables) - UNSAT only - c/v in [3.26,5.26] ?
3. Targeted Testing:  Small problems, UNSAT only in [2.5,3.26] and SAT only in [4.26, something]
4.  Depth Testing:  Medium problem (50?  100?) at c/v = 4.26.  Skip brute force checks ahead of time.


Where c/v is clause to variable ratio.  Small and tiny problems will probaby have to be well under 30 variables, because that is when the time required for a simple brute force solver gets ridiculous.  Unless I utilize GPUs.

#3 might be the most useful.  Unless I'm an idiot, my algorithm is guaranteed to stay within O(n^10), and, in fact, can only reach n^10 IFF the instance is UNSAT.  The only danger is reaching a stage before then where the algorithm cannot continue.  I have a fuzzy idea in my head that it will never reach this point.  Solving a trillion instances would give enough credence to that fantasy to try to prove it.

The Trillion Instance Algorithm

"It was first suggested that a googolplex should be 1, followed by writing zeros until you got tired."

--Kasner and Newman

 

"And so it came to pass that Ryu, son of Dragon the Shogun, ascended the steps of the great Temple of The Real Projective Plane, and stared into the mobius vortex.  By surviving he earned the right to study with the Don, and learn his mathematics.  And when Ryu, son of the Dragon, left that temple he found the Don's mathematics more powerful than the math of any warrior he encountered, and Ryu laid waste to the land, for in the vortex he had lost his sanity, and for the rest of his life the drum beats in his mind never ceased."

Yeah, anyway.  After scribbling on enough paper to kill a few trees (not that it matters) I came up with a 3-SAT algorithm, and coded it in two days.  This time I am certain that the upper bound is O( n ^ 10 ) but uncertain that it will solve all 3-SAT instances.  With this algorithm, there is no risk of it exceeding the upper bound; it will simply get stuck and sit down in the sand and cry boolean tears.

Obviously,  since programming is, to me, more fun than mathematical proofs, my next instinct was to think about simply solving every 3-SAT algorithm in existence.  I tried calculating an upper bound on the number of 3 sat instances that could exist.  For a problem of 20 variables, the number of possible instances that can exist is a number with hundreds of decimal places.  This might be the first time I've noticed a finite set of things that could not be adequately described by the word fuckload.  Maybe a...oh wow there are actually words that go that high.  So, its less than a centillion, however so much more than a vintigillion that its not even worth comparing.

Anyway.  I don't have the hard drive space to store that many instances, and lets not even talk about the issue with duplicates.

Instead, I am making it my goal to solve a trillion instances with my new algorithm, which doesn't even have a name (other than "Algorithm.cs") because I've just given up naming these things.  All it takes is one boring meeting and another 3-SAT algorithm pops into my head.

Anyway, once I solve a trillion instances...I suppose I would take it more seriously and do the actual legwork to create a proof.  Although, I am much more a fan of this model:

1. Solve one trillion instances
2.  ...
3. Prove P=NP !

Step 2 is actually the same exact step in the standard startup business model:

1.  Cool idea
2.  ...
3. Profit!

So I know I'm not that crazy.  Whatever the case, it's nice to have a distraction.

I'm pretty sure I write a post like this every time I think I've gained traction with one of my 3-SAT ideas.  I'm pretty sure of this because when I was calculated the total number of possible instances, I remembered how to do it because I did it before, and I remembered how I wrote about it last time.  So, welcome to recycled content.

Day 2 of Recovery

Thanks to a certain jackass I disabled access to this blog to everyone but me.  Then I realized that I had given the link to my "In Seattle, the Ducks Ride You" post to a paralegal that is drafting a deposition (fuck, even that makes me miss my ex-gf!) for use in a legal case against the duck fuckers.

In case this person needs to review the entry for factual accuracy, I am re-allowing access until the deposition is ready and signed.

After that, I don't know.  I'd like to write some custom blog software that blocks access to people who both have Seattle IP addresses and don't know how to use proxies, but I don't know how I would handle mobile phones, and I am trying to concentrate on learning C# as I ramp up on projects at my new job at Bikrosoft.

Part of the reason that my now ex-girlfriend and I are splitting is that I am unable to provide an adequate amount of emotional affection.  Affectation might be the best I can do.  Maybe I am like The Doctor...maybe I should just search for some kind of female companion and forget about all this romantic nonsense.

At this point, it seems possible that our relationship could be saved, if I insisted on meeting with her and hashing everything out and promising to make real changes...tell her she is beautiful more frequently, etc.  I can't figure out if it is the right choice or not.  I want to live with no regrets, but I don't know if I will regret getting back together, or letting her slip through my fingers.  Maybe I would regret either, and there is no easy answer.

I wish that I could edit my own brain and disable loneliness, love, longing...really all of the L emotions.  Probably take out sadness while I'm at it.

Stark's Legacy

 This post is about 3-sat! Yay!!!!

To quote wikipedia:

http://en.wikipedia.org/wiki/3-SAT#3-satisfiability

3-satisfiability is a special case of k-satisfiability.  Oh.  Who knew?  K = 3.  This is one of Karp's 21 NP-Complete problems?  What is NP-Complete?  Glad you asked.  But first, more from wikipedia:

There are two classes of high-performance algorithms for solving instances of SAT in practice: the conflict-driven clause learning algorithm, which can be viewed as a modern variant of the DPLL algorithm (well known implementation include Chaff, GRASP) and stochastic local search algorithms, such as WalkSAT.

A DPLL SAT solver employs a systematic backtracking search procedure to explore the (exponentially sized) space of variable assignments looking for satisfying assignments. The basic search procedure was proposed in two seminal papers in the early 60s (see references below) and is now commonly referred to as the Davis–Putnam–Logemann–Loveland algorithm ("DPLL" or "DLL"). Theoretically, exponential lower bounds have been proved for the DPLL family of algorithms.

In contrast, randomized algorithms like the PPSZ algorithm by Paturi, Pudlak, Saks, and Zani set variables in a random order according to some heuristics, for example

It feels like something has been ripped out, and I am bleeding off into some dimension I can't see.  I know that this type of wound closes on its own eventually, but until then, it feels like someone has hung a heavy garment bag on my soul, and I am restless...unable to think or focus on any one thing for too long.  I dread going to my job tomorrow because I'm going to face it without her random chats to brighten my day.

A long time ago, I spotted a book called Game of Thrones in the airport bookstore, and ended up hating it, only to find that one of my friends absolutely loves this book.  I did everything I could to rain on his parade, everything I could to ruin it for the billions of people on this planet that needed to be saved from what appeared to be some new and daring form of literature but was actually just a soap opera written to be marketable.  But I digress.

Ostensibly in response to my hatred of this book, this friend of mine revealed to my girlfriend the secretly public location of this very blog.  The security of this blog is based on preventing people in Seattle from reading it, mostly by doing silly things to keep the posts out of relevant search indexes.

At the time I thought nothing of it, and was already planning my next response:  waiting for the last Game of Thrones book to be released, staying up all night to read it and take notes on the major plot twists, and then flying across the country and renting a generator and large speakers and blasting my friends house with a speech revealing the ending of the last book.  I figured that kind of response was on the same level.

Then my girlfriend read my blog, focusing specifically on the parts about her.  I was not prepared for a real problem to occur here.  At first, my sarcasm and use of negative words as compliments infuriated her.  Then, she read a post that cut far deeper, right down to a existing fissure in our relationship.  The actual post was something that, if part of a scrubs episode, would have been a sudden plot development that becomes a major but surmountable set back that ultimately leaves J.D. still dating the girl.  In real life, though, things are different.


While I watched my close college friend get married in an elaborate catholic wedding, my girlfriend was crying, alone, in the hotel room.  A few days later we broke up as she dropped me off at my apartment.

The suffocating feeling that is like a vice squeezing the life out of your heart has actually gone away, mostly, and in its wake is nothing but the dull emptiness that lingers after every girl disappears.

Perhaps expecting this to happen, and preventing myself from getting to emotionally attached, became a self fulfilling prophecy.  Perhaps its true that we really weren't compatible.  Whatever the case, I cannot even begin to put into words all of the things I am going to miss about her, and the thing that hurts the most is knowing that it was my carelessness that hurt her.

Unfortunately, its just another noir ending.  Here's looking at you, kid.