A look at OverSAT X and a passing note about NP Completeness.

Here is a look at OverSAT X running in Windows 10.

The look is designed to be reminiscent of an old school computer. The CRT look is evocative of the 1970s and the look of the push buttons mimics those I have seen on mission control panels for the Apollo program of the 1960s. It's a homage to the era when the problem of satisfiability began to be first understood.

OverSAT X solves CNF files. It will either produce a decision string that satisfies all clauses or find that no such string can be created, with a proof of contradictions showing this is impossible, . At some point, it will also see when it must simply give up. Here, the user selects a CNF file from my collection. I downloaded mine from FSU (but the link is dead), SATLIB.org and also also the SAT Competition.

Once the file is loaded, a user may either single step through the SAT problem, or simply run it. Running the problem runs the solver on the background thread, as I wrote in a previous post.

If a solution exists, the OverSATX will eventually find it. Note though, in this screen shot, there is a bug. The particular CNF being solved had a symbol --1, and we treated that as -1 being a separate name than 1, which is, well, a mistake.

OverSATX works by attempting to build a non-conflicting string of variable assignments. For example, given a system (A or B) and (not A or not B), a decision string cannot contain both A and not A. The solution string could either be A not B, or B not A. If, during the building of this string, OverSATX detects a clause that cannot be satisfied because all of the possible choices would be in conflict with the existing string, the clause is said to be conflicted, and the existing string is the conflict string.

This conflict producing string is analyzed in an attempt to find a shorter string. It turns out that the shorter a conflict string is, the more bits are removed from the search space of the overall problem. However, any decision string that keeps a conflict is useful to have around. OverSAT X is also smart enough to replace larger strings with shorter ones that completely contain the space represented by the longer string. By accumulating conflicts and using new decision strings to avoid them, OverSAT X seeks to ever constrain the search space until it arrives at a solution.

It is interesting then, that the overall search space is constricted at each pass, always and relentlessly by some amount. But by how much?

At the moment, not enough. OverSAT X is a bit of a slow learner and there's holes in how it comes up with that conflict string and its processing of it is far from efficient.

But, as a rule, to formerly determine the performance of OverSAT X in Big O notation, then, we shall some day wish to know how many bits from the solution space are being removed by OverSAT X at each pass, and on average, above all, in the worst case. That hasn't been done yet, and characterizing the search space, and improving that contraction performance, is part of what this particular bit of madness is about.