AX to the Not

I''ve been pining for the East Coast, or at least a programming job I like, practically since I've moved here, and now that everything is getting shaken up and I'm actually getting off my ass and doing something about it, I have a girl I don't want to move away from.  Seems like incredibly poor timing to me.  What I should have done is dated someone for the past three years and then break up now...basically the opposite of what I'm doing.

I suppose thats the cost of treating life as an adventure.  I'm a leaf on the wind.  Leaves probably shouldn't complain about where they end up.

I had an interview with a local company scheduled for Tuesday, as in, today.  Unfortunately I read the email incorrectly and scheduled it for Thursday in my calendar, shuffled around shit at work, and told everyone that I had the interview Thursday.

The silver lining is that my one manager--the one who liked to call me into his office and tell me I'm doing everything wrong--isn't around to rub it in.


3-SAT

Anyway, here is a 3-sat algorithm I have been thinking about.  For all I know it has been done before.  In developing it, I made a fatal flaw somewhere because the algorithm doesn't actually work.  It does, however, end up with an interesting property.  So here it is.

First, the most brutal of the brute force methods.  Replacing a variable, say x, with 0, recursively seeing if the problem is solvable, and if it is not, declaring that x must be 1 and then solving what's left.  Runs in 2 ^ number of variables.

Consider a problem that includes these:

(x y z)(!x a b)

Assigning actual values

let x = 0:    (x y z)(!x a b) =>  (y z)

if that ends up being unsat, then x = 1:  (x y z)(!x a b) =>  (a b)

Replacing with other variables

let x = y:    (x y z)(!x a b) =>  (y z)(!y a b)
if that ends up being unsat, x must equal !y:   (!y y z)(y a b) => (y a b)

Replacing with expressions of other variables

let x = y+w:   (x y z)(!x a b) =>  (y w y z)(...yeah this didn't really go anywhere.

Replacing with expressions of other variables, part 2

let x = xa (lack of space means "and" as in, intersection":   (x y z) =>  (xa y z)

however, we only do that to x.  We don't change !x:

(x y z)(!x a b) =>  (xa y z)(!x a b)

Why the hell would you do this?  Two reasons.  Well, at least two.  First, it makes the problem strictly less satisfiable.  Draw a truth table for variables x,y,z,a and expressions (x y z),(xa y z) and you will see why:  it adds a single extra 0 in the (xz y z) column.  I would give you the table here but I am too lazy to write an html table right now.

Second, if saying x = xa makes the problem unsat, well then, x must not equal to xa.  Actually that statement is probably the one that is not true, but I don't understand why.  Anyway, thanks to some guy named DeMorgan:

x != xa  =>    x = (!x !a)   [that is:  not x, or not a]

So:

let x = xa:  (x y z)(!x a b) =>  unsat?  well then x = !(xa) = (!x !a) so (x y z)(!x a b) => (!x !a y z)(!x a b)


The interesting point here is that x becomes !x.  Sure there is a !a also, but there are no more x literals, only !x.  We can set !x to true and eliminate all of those expressions.

Replacing with expressions and taking it way, way to far

So we have this trick where we let x = xa.  Intuitively, (xa y z) should make the problem easier to solve because now that expression conflicts with all expressions that contain a !a.  But lets not bother with that.  No one said we could only intersect/and x with one other literal.

What if we did something like let x = xyzabw ?  It would make the SAT instance much harder to solve, making our job so much easier in the sub problem.

And then, what if we chose these other variables in such a way that eliminates all of the non-standard and'd expressions?  For example:

(x y z)
(x w a)
(x g h)
(x j k)

let x = xywgj

Thanks to the simple theorem that x*y + y == y:

(x y z) => (xywgj y z) =>  (y z)
(x w a) => (xywgj w a) => (w a)
(x g h) => (xywgj g h) => (g h)
(x j k) => (xywgj j k) => (j k)

And, if we find that instance unsolvable, well then x != xywgj, and in fact x = (!x !y !w !g !j).  Fancy that:

(x y z) => (!x !y !w !g !j y z) => TRUE

The expression becomes satisfied not only because there are no x's to conflict with !x, but because the expression has both a !y and a y in it.  Effectively, but solving a subproblem where x = xywgj and finding it unsat, we can simply eliminate every expression with an x OR a !x.

Important:  eliminating every expression (sorry, clause) with both literals of a variable in it (ex: x and !x) makes the problem strictly more solvable.  Interesting.

Something is wrong here

Some of you may be thinking "wait, this can't be right."  You are right.  This approach is flawed.  Not sure why, but its probably related to the fact that I'm only changing x.  If my approach was correct, you could simply write an algorithm that removes all of the clauses for every variable until it finds the problem unsat.  Clearly, that isn't the case:  removing clauses willy nilly has this strange effect of making any sat instance satisfiable, even if I found it in the "unsat" category of satlib.

Binary Search

But we can't give up yet!  I never like to give up on a SAT algorithm until long after repeated experiments have proven me a hopeful idiot.  What to do?

This is where two properties I discovered become interesting.  Long have I searched for a way to use binary search on 3-SAT.  If only we had some way, I thought, to test a solution, and if finding it unsat, had some way to know if the real solution was to the left or to the right of the one we tested.  In this context to the left or right can mean anything...more 1's in the solution, a higher integer represented by the 1s and 0s in the solution...whatever you want.

Guess what:  we can kind of construct such a search!  Doing my crazy shit with the x = xabcd... nonsense (which effectively sets x to 0) makes the problem strictly less solvable (technically, it guarantees that the new problem is at least as hard as the old one...usually harder).  This means that if we did that "and" trick with a whole bunch of variables without any of them causing the instance to be unsat, and then at the end discovered that what we had was satisfiable, well, we'd be done:  we made the problem harder to satisfy, and still found it satisfiable.  Game over;  we won.

To go the other direction, we do the thing that makes it strictly more solvable (in reality the new problem is guaranteed to be at least as easy to solve as the previous one, to "stricly" is the wrong word to use).

So for a given variable, x, we know that x=xabc... makes an instance that is less solvable, and x != xabc... makes an instance that is more solvable.  Lets say that the less solvable route is taking us "to the left" and the more solvable route is "to the right."   Also, lets say that we must always investigate these variables in the same order, that is, if we go left (choose x = xabc...) on x and then act upon y, and then other variables until we reach some result at the bottom of the tree, the next time, when we go right on x (choose x != xabc...), we MUST do y next, again.

Once you do this, I think, you can take some arbitrary path down the search tree.  Sure, the number of nodes in the tree, or even along the bottom, is exponential, but once we DO get to the bottom, depending on our answer (sat vs unsat), we know which direction to go in:  if we got a SAT answer, we need to search to the left.  If we got an UNSAT answer, we need to search to the right.

For example, lets sat for variables x,y,z,a,b we went LRRRR  (this actually takes us to the half-way point) and then we got a SAT answer.  We should go to the left.  We can go half way between our current position, and the left side of the tree, by taking the search path LLRRR.  If that new position was SAT, we could move on to LLLRR and if it was unsat... LRLRR.  Just draw a binary tree and this will make sense.

What exactly are we searching for?  Well, we can find the place where the leaf instances switch from UNSAT to SAT in what I believe is a polynomial number of steps (something like log2(2^n) ) although I could be wrong about that also.

Here is the problem:  I can't decide what we accomplish but doing so.  Sure, intuitively, the farther left you are (where it changes from UNSAT to SAT), the more likely it is that the original problem was satisfiable, and the more right you are, the more likely it is to be unsat.  But can we infer an exact solution without doing more work?  I'm not sure we can.

Maybe this approach can help us find the "critical section," as in the subset of clauses in the instance that by themselves make the instance unsatisfiable.

So that was fun.  I think I'm going to put this algorithm away until I can figure out some use for what it provides.  Just thought I'd share.



 [edit]
the-25-best-tech-companies-to-work-at-in-2012-2012-6