HELLA YES

Hail to the King, Baby:

uuf75-0100.cnf
UNSATISFIABLE cluster = 0, 21, 49

Thats the sexy little message my algorithm had waiting for me when I got up this morning.

For two days now I've been watching my algorithm do its thing.  Ever fearful of bugs that would get my hopes up for nothing, I initially had it print everything it was doing to the screen.  It actually looked like them matrix in reverse.  I stared at it for hours, transfixed, perhaps the way some people watch sports.  Things things called "jumps" were bad--we didn't like them.  "Merges" were good though--I was rooting for them.  The first time I ran my algorithm with a sizeable UNSAT instance, it ran all night inside the Eclipse console, slowed down by the time it took to print everything out.  I had to go to work, and since there is a heat wave of over 32.7C (90F) and I live in the 6th floor in a building made by idiots who thought I wouldnt need airconditioning, I had to stop the algorithm and turn my computer off.

I bundled up my code and went off to work, telling my self I would restart the algorithm on my work computer...maybe in a screen session so I could hide it.  Unfortunately, the tool I used to bundle the code was git, and I didn't know what staging was, so the code was missing some chunks when I got to work.  Very sad.  That was friday.

I came home and worked on my algorithm some more.  Reduces the text output so it would go faster and waste less time on IO.  Then I ran it again, on an UNSAT problem with 75 variables.  It went quicker this time.  I watched it for hours, fascinated.  It was clear that the algorithm had quickly discovered (after 3 or 4 hours) that the first variable (X) must be False, but the companion discovery it needed, that X must be true, did not come quickly.  It got it though.

Here is where I stand:  I have an algorithm that performs a polynomial number of operations and then throws an exception.  Thus far it has solved every problem in less than half of its allotted operations, however I have no idea how to prove that it will never need more, and I have no idea if there is some worst-case problem lurking out there in the realm of possibility that my algorithm cannot handle.

My current strategy involves making it solve every 3-sat problem I can get my hands on.  The only problem is, polynomial doesn't mean fast.  My algorithm does no more than m^3 steps, where m is the number of variables.  However, each of those steps takes about m^c, where c is some constant that would make any algorithms professor very cross.  This is mostly because in my excitement I programmed some of the most inefficient code ever--I didn't care, so long as it was polynomial.  Well...now I do care.  Because it takes forever to run.

Now, I suppose, I'll try an optimize it.  Maybe find a supercomputer I can run it on.  It might not be that bad...maybe it didn't actually run all night.  I went to bed at like 12:30 or 1:00 am, so for all I know it could have stopped shortly after.  Maybe what I need to do is add timing information.

[Edit]
First optimization:  when I have to search through two enormous lists of clauses, I no longer copy them to a third list first.

SatLib


[Nothing to see here]
Q. Why can't I connect to my EC2 instance
A. You used your private key from last time you tried aws instead of the one you just created for your instance, you didn't open up the SSH port using amazons lame security editing interface, and you tried to ssh in as yourself instead of 'root' (need to prepend root@)

setting up what I need on Fedora Core
useradd -m bob
passwd bob
# you still can't ssh in as bob...
scp -i /home/dave/awskeys/sat/sat.pem /home/dave/msat4.git root@longassname.amazonaws.com:/
msat4.git
yum install git-core -y
yum install screen -y
vim /etc/sudoers  #add new user

#have to download the jdk from sun's retarded website, which you can only access with a fat, modern browser
#scp it to the EC2 instance
#run suns intaller; its a pain the ass

#(do this as the user)
export PATH=$PATH:/opt/jdk1.6.0_21/bin
echo "export PATH=$PATH:/opt/jdk1.6.0_21/bin" >> .bashrc
export JAVA_HOME=/opt/jdk1.6.0_21/
echo "export JAVA_HOME=/opt/jdk1.6.0_21/" >> .bashrc
or: export PATH=$PATH:$JAVA_HOME/bin
#edit sshd_config and set ChallengeResponseAuthentication to yes
#also change PasswordAuthentication to yes


compling like eclipse does it but without ant because fedora core SUCKS
#using junit from eclipses plugin folder.  figure that can't fail
scp -i /home/dave/awskeys/sat/sat.pem ./junit-4.1.jar root@longassname.amazonaws.com:/home/bob/

export cp=`find lib -iname '*.jar' -exec echo -n {}: \;`.
javac -d bin `find src -iname '*.java'` -cp $cp

Screen
# when you run screen you will see:
#    Cannot open your terminal '/dev/pts/0' - please check.
# because you had to log in as root because AWS is dumb.
# execute this:
sudo chmod o+rw /dev/pts/0

to detach Ctrl+a,d
to reattached:  screen -r

rename window:  Ctrl+a, Shift+A
look at windows:  Ctrl-a, Shift+"


[edit]
It takes 6 hours for my linux box to prove that a 75-variable problem is unsatisfiable:

started at: Sat Jul 10 11:47:02 PDT 2010
ended at: Sat Jul 10 11:47:02 PDT 2010
total time: 21611586 ms

Somebody is going to be renting a lot of EC2 instances....