NAND rewriting

I think somewhere between '01 and '04 I was interested in SAT problems. At that point in time there was an unoutspoken vibrance in the field that NP problems might be tackled.

At that time I concentrated on NAND, or Sheffer stroke, rewriting. I figured if people were close to breaking some barrier then there should be some rewrite strategy to a solution that didn't suffer from exponential blowup during the path.

NAND terms are beautiful little mathematical expressions and the rewrites I came up with had pleasant forms so I wrote several small programs.

One of the things I stumbled upon was a 3SAT formula after I looked for a while at the truth table for NAND.

x y z
0 0 1
0 1 1
1 0 1
1 1 0

Every row has at least one zero (-x+-y+-z), and certain pairs have at least one one (x+z) and (y+z).

I checked the conjunction and realized I had a linear translation from circuits to 3SAT.

Meanwhile, I was reading satlive.org and noticed that people were unaware of that and posted the solution there thinking Armin Biere would at least pick it up.

Years later I learned I had rediscovered a solution from Tseitin from the sixties or something, years before SAT solvers became relevant. Nowadays I think everyone who studies the problem a bit would've come up with it.

The NAND rewriting strategy never panned out, stuff kept exploding. Moreover, rewriting is extremely slow in comparison to cheaply manipulating arrays in what is very fast (learning) local search.

I can still somewhat rewrite NAND terms in my head or play pebble games on them, but that doesn't seem to be a marketable skill.

But, ah well, I comfort myself that I was in the good company of Knuth who, for at least a while, thought that P=NP.