#sat solvers

I am inherently, a very lazy person. And I cannot stand being bored. This has, of course, resulted in me being really into coding and automation.

And when I begin my journey as a mathematician, thirteen-year-old me was really sure I'd figure out how to write just the right algorithm that would automatically solve all math problems. But this is actually really hard.

Now, naively, it's really easy. You just write a code that takes the axioms of a system, your premises, and then just tries to apply every single possible rule to generate more statements until it either proves or disproves what you want.

But two problems arise: halting problem, and the fact that it takes a really, really, long time to get anything done.

Maybe you can mitigate the halting problem somehow or something, you could additionally try adding proving the statement is unprovable as a stopping condition, but maybe it is unprovable that it's unprovable, or maybe it's unprovable that it's ... I'll stop.

But that doesn't much matter if it's going to take a twenty years to prove a single statement. At that point, you might as well prove it yourself.

Let's say we have a proof checker, it starts with a proof and then tells you that it is valid. If we run this algorithm backwards, then... shouldn't we get a valid proof?

This, quite obviously, doesn't work. Or at least, doesn't work easily. (The fact that it doesn't work is tied with P vs NP) It's less obvious when you're trying to do this without realising you're trying to do this. But for some reason it took me a while to realise why that wasn't 'easier'.

The reason it doesn't work finally clicked with a Rubik's cube. If I run an algorithm like CFOP on a cube to solve it, then I can run CFOP backwards to get the original position, starting from a solved cube? Nope. Mathematically, the best I can do is reduce it to 1/12th of the states, leaving some 43 quintillion (43,252,003,274,489,856,000) possible starting points which all end up in the same ending point. Running an algorithm backward isn't just some trivial thing. It's a whole millennium problem, you get a million dollars if you figure all of this out, since running verification backwards is what all of P vs NP is.

At some point after that, I learned there's a whole field of math devoted to this.

And today, I watched a YouTube video about someone trying to run Conway's Game of Life backwards. It's not easy to find even one possible backwards step. And I remembered this.

Today, I happened to be working on a SAT solver. And noticed the sat solver had another sat solver inside of it. In retrospect, that should have been obvious.

Now, for those who don't know, here is what a SAT solver does, and what its applications are:

A SAT solver takes a statement made of negations, conjunctions, disjunctions, and atomic statements and then returns an assignment of the atomic statements that makes the statement true.

For example: A or B, this can be satisfied as A = True and B = False.

This is the quintessential NP-complete problem. All the others can actually be reduced to it. So for the list of problems that a SAT solver can solve, see link below.

Modern methods have been trying to make it really really fast. Unfortunately, we haven't been able to beat the polynomial time barrier. Most people think it's impossible, but no one has actually shown that it is impossible.

I'm really naive, perhaps, in that I think P=NP. I may just believe that because it'd be so cool if it were true. So far no one has proved me wrong.

Now, whilst working on one of these SAT solvers, I realised something: the input for the solver has to be in conjunctive normal form, and there's a preprocessor that converts the statement into conjunctive normal form, that is

Anding a bunch of ors of atomic statements and their negations.

(a or b) and (c or (not a)) and (a or c) and ((not a) or c or f)

To get them there, the preprocessor system that converts things into conjunctive normal form has several rules about manipulation of these statements. As it happens, it is robust enough to do the same, but into disjunctive normal form, which in this case happens to be:

(b and c) or (a and c)

Which does actually accomplish what the SAT solver set out to do.