Project Description
Oxsat is a Portable SAT Solver.

Oxsat is forward conflict avoidance SAT solver that can tell you when it cannot solve a problem, uses comparatively low memory does not need a heuristic, and outputs an unsatisfiability proof that is easy to verify. The latest incarnation is a command line that can run on both Windows and Linux.

The Windows GUI version was used to develop a lot of oversat but it is behind a bit. Honestly, the whole code tree is a mess.

Oxsat works by parsing a CNF file into a grammar of conflicts and implications. As Oxsat makes a guess, it attempts to reduce a string using the grammar until it reaches a conflicted state. At that point, Oxsat makes another guess. Instead of an implication graph, Oxsat keeps a solution string, that represents a unique list of literals that constitute a solution in progress. The solution string always grows, meaning that, once a literal is recorded in the string, it is never removed, although its value may be altered during the conflict resolution process.

Here, Oxsat solves the simple problem Quinn's CNF (from Rutgers). The language grammar deduced by Oxsat is on the left, the SAT problem the next column over, the current decision string runs top to bottom, and finally, any conflicts on the current step are shown. Often this is blank. Sometimes it is full. Oxsat will try to resolve conflict chains up to 16 literals long through brute force, but then, if that doesn't work, it bails. It is possible to make this resolution much more efficient and that will be done in future release.

oversat_quinn.png

In this example, Oxsat attempts to tackle another Rutgers dimacs example. This one is known to be unsolvable and Oxsat correctly determines it is unsolvable. In the conflicts column, you can see that Oxsat has identified a closed conflict chain consisting of a single literal. Each valuation of that chain yields a conflict, and therefor, because the conflicts are closed with respect to the conflict chain, the entire problem is unsatisfiable.

oversat_unsatisfiable.png

Finally, here's where Oxsat fails. We give it a SAT challenge problem of reasonable length and it quickly produces a conflict chain that is too long. Oxsat gives up! As a rule, we expect to improve the resolution time of the conflict chain while retaining the characteristic of a cleanly bounded estimation as to when the problem can be solved.

oversat_too_hard.png

There are three solution folders, oxsat, OverSAT, and OverSATb. OverSATb consists of older work and I would delete it if I could. OverSat is newer, and is a Windows SDK dialog based application. oxsat is a command line version for Windows and Linux.

oxsat is our entry to the SAT challenge for 2017.

The citations page actually doesn't give half the credit to all the universities I've googled about SAT and CNF, but Rutgers comes to mind for a good set of links to CNF formats and sample problems, and there's a guy in Japan that made a great slide show on CDCL, among others.

Citations

Last edited Feb 23 at 12:33 AM by tbandrowsky, version 22