Introduction

In order to limit any expectations up front, let me say that this tool is not a proof of P vs. NP (I really do not wish to participate in that discussion). It is also not meant to be a lightning fast SAT solver, although SAT problems can be solved with it (some even faster than with a variable based decision algorithm).

It is primarily an educational tool to provide some hints as to why some problems are hard and some are easy. (It sure educated me and it finally became fun after all).

If you have some experience in SAT problems, you may wish to decide beforehand, whether there is anything new here, or whether it is just a re-iteration of well-known facts.

So, in order to help make that decision, I am providing an abstract, as if this article was meant for publication in a mathematical journal:

• An algorithmic data structure, the |sm|, is constructed based on the mapping of arbitrary x-SAT problems, x = (1, 2, 3, ..), to an independent set problem, with additional constraints.
• The |sm| is shown to be a dynamic representation of all possible solutions to a SAT problem that differs from the well-known truth table. Its space requirement is O(n^2) which is better than that of a truth table O(2^n).
• An algorithm is presented, which operates on the set of all possible solutions instead of just a single possible solution. The worst case running time of the balancing algorithm (|rua|_) is shown to be O(P).
• The algorithm delivers a method to trivially solve 2-SAT problems. All possible solutions can be generated based on sound decisions without the need to perform a guessing search.
• A clause based decision algorithm is presented, which is shown to have an upper bound of ceil(k/2)^m. This eliminates the need to use variables to show exponential complexity.
• It is shown, that operating on the full set of possible solutions eliminates the need to distinguish between variables and clauses at all. Variables are shown to be a special case (size 2) of general disjunctive clauses of size k, k = (1, 2, 3, ..). Therefore, variable based decision algorithms are shown to be a special case of the |sm|.

Although the proofs only require very basic propositional logic, the fact that the |sm| is a true superset of variable based algorithms means, that the |sm| cannot be proved in terms of the existing results of research on variable based decison algorithms.

As I do not have enough time to start that venture, my research is presented in the current form instead of an official publication, in the hope that it will at least incite some interest in my son.

Since I first wrote this in 2013, I have nevertheless started it and it is available as Structural Logic.

The terminology was purposefully chosen to differ as much as possible from the terminology of existing variable based decision algorithms. I found this helpful to trick my own prejudice which lead me time and again astray by mistaking necessarily similar concepts as identical.

If you are a professional and have to be careful about wasting your time, you may still find amusement in the fact, that iff the |sm| is proved correct, variable based decision algorithms can be interpreted as forcing a necessarily satisfiable 2-SAT sub-problem into a 1-SAT problem in the hope that the resulting consequences in the k-SAT sub-problem, k >= 3, can somehow be detected more easily. The information that the k-SAT sub-problem provides from the very beginning is then gradually detected to enhance the decisions[#]_.

If you are a student and have more time at hand, feel free to prove any part of the |sm| as an exercise. If you can prove it correct, you will help advance knowledge in a very prestigious part of the field. Although you will not really be concerned about P vs. NP, it still generates lots of hype, if you do not point out the irrelevance of this topic too hard. It would be nice, if you gave me feedback either way.

Just a hint from my personal experience: It may be necessary to express the concepts in commonly accepted terminology to find somebody willing to listen, but it will make it hard to explain the subtle differences without explaining the entire concept. The key argument is, that working on the entire set of solutions to begin with is indeed quite different from working on (varying) single element subsets at a time.

If you are a skilled hacker, you are probably already used to not being understood by lesser minds. So you need not concern yourself with boring proofs of self-evident facts. You can jump right in and write highly optimized versions of the satoku algorithms (e.g., `satoku-mode`_ needs a complete rewrite -- as a matter of fact, everything I produced needs a rewrite). If you rather think that people should be deserving of knowledge and work for it, go ahead and write non-GUI tools that only a selected few can understand, have a look at my collection of cryptic adhoc command line tools (to be included soon) and create a satoku tookit.

If you are a hacker mastermind, help yourself to a conspiracy theory along the lines of "mathematicians (financed by the clan of your choice) conspiring to hide the true nature of boolean satisfiability problems to make encryption seem safe". I am willing to pose as a tragic hero who was tricked into believing that there was a substantial difference between 1,2,3-SAT, so that n-complexity (input = variables) would make any sense at all. The tragedy would be that this made me stare at the obvious for almost 10 years, not realizing that m-complexity (input = clauses) was the key to the whole problem. You can insistently repeat that ceil(k/2)^m trivially shows, that not only are 1-SAT problems trivial, but also that 2-SAT problems are trivial (1^m is very trivial indeed). Vehemently explain that the only way to hide this, is by pulling a hideous "Wizard of OZ" charade of "Do not look behind the curtain (of n-complexity)!"

If you do not find yourself in any of these categories, you can just enjoy a fun game and make a donation if you like it (just kidding :)).

Copyright

Copyright (C) 2013, Wolfgang Scherer, <Wolfgang.Scherer@gmx.de>. See the document source for conditions of use under the GNU Free Documentation License.