علي الباشا 2

Date: 1 Apr 2004 10:30:59 -0800

Making use of a new type of model-theoretic tool -- the Boolean Sieve -- we have been able to construct a P-time algorithm for SAT, thus providing a resolution to one of the most famous, long-standing open problems of Theoretical Computer Science. A detailed, but accessible and informal, general overview of the Boolean Sieve method (more information can be found here by carrying out a Google groups search under "Boolean Sieve" and "Mathematician's Algorithm"). However, a brief description will be provided below of the method, some applications outside the specific context of SAT, as well as an overview of how it was applied to SAT. Opportunity providing, an abstract or possibly even an on-line copy of the submitted paper (just accepted for publication) will be made available at the above Web site.

What is a Boolean Sieve? Basically, it is a construct that is generated from a set of models, for an axiom-free theory ("free theory"), that are defined to filter out the possible logical relations between a set of statements which could be rendered in that theory. A possible application may be to seek out significant axiomatizations that may be applied to the set of operations and predicates in the underlying free theory. The term "filter" is more than appropriate given the nature of the formal machinery behind the method.

For instance, consider Group Theory. An interesting (but not well-known) fact is that groups can be defined by their inverse operation (division), just as well by multiplication. The underlying free theory is an algebraic sort with the following set of operations:

                            () |-> 1 (identity)
                        (a, b) |-> a/b (quotient)

So, it then becomes natural to ask: what are the logical relations between the possible statements that could be made over the underlying free theory. Such a situation is precisely the kind of circumstance where one would use the Boolean Sieve method.

What one does is write down a bunch of statements (ideally, including a set of statements that we already know from prior considerations would completely characterize a group), and then select a bunch of models for the free theory (which in the case at hand may or may not actually be groups). Each model should have the property that each statement has a truth value whose evaluation in that model can be done "efficiently".

The result is a set of raw data from which a profile can be assembled. The method of integrating all the basic facts is the Boolean Sieve, itself. The result of applying the Sieve is an efficient characterization, as a set of Horn clauses, of the Boolean lattice generated by the statements. >From there (for instance) one could read off the significant relations and possible axiomatizations, e.g.,

                   (a/c)/(b/c) = a/b; a/a = 1; a/1 = a

or for Abelien groups:

                   a-(b-c) = c-(b-a); a-(a-b) = b; 1-1 = 1.

More generally, a Boolean Sieve will allow us to filter out the possible relations between a set of statements. The Sieve is called Complete for that set, if all possible relations are constructed by the Sieve. What we've actually done is resolve a generalization of SAT (i.e., determine the validity of a Horn clause involving Boolean formulas over N-variables) by defining a process (that is N^3 in complexity) that generates a complete Boolean Sieve that is N^3 in size.

Why N^3? Well, this is where it gets interesting: the method for generating the complete Boolean Sieve is essentially a disguised version of the Earley parsing algorithm for context-free grammars! The significance and nature of this link remains a total mystery to us.

Currently, we are investigating extensions of the Boolean Sieve which will provide a basis for model-theoretic theorem proving methods -- or "Semantic Theorem Proving". As any expert mathematician will be able to relate, such an appropach has a far more direct bearing on the way mathematicians actually approach problems. They will take a stock set of examples, run a set of possible statements through the examples (often-times subconsciously) and "magically" arrive at a set of conjectures. We conjecture that the latent method behind this process is none other than the Boolean Sieve, itself. We even speculate that "mathematical intuition", itself, may be nothing more than the by-product of this subconscious process. Thus, for instance, one could develop a more honed "intuition" by having a larger stock of ready-made examples "under the belt", so to say.

Needless to say, these developments will go far beyond the specifics of the P = NP problem, as most anyone would have been able to anticipate regarding any method used to resolve this issue. Indeed, we strongly suspect that the very date of this announcement will long be remembered in the annals of history. Signed, Martin Michael Musatov:Eternal Prover of P=NP.