P = NP Proof Soon To Be Published
David-Olivier Azulay
Mark William Hopkins (hu...@alpha1.csd.uwm.edu) wrote:
: 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 is provided at
: <http://www.csd.uwm.edu/~hunk/pnp.html>. 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.
--
David-Olivier Azulay
http://azathoth.esil.univ-mrs.fr/~azulay/
Hope Rover's hub-caps aren't stolen overnight.
Arthur C. Clarke (science fiction writer, to the Pathfinder mission)