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.
صفحة مستخدمنقاشعدل هذه الصفحة+تاريخمراقبة
Solsticefanنقاشيتفضيلاتيقائمة مراقبتيمساهماتيخروج
الموسوعة
الصفحة الرئيسية
الأحداث الجارية
أحدث التغييرات
أحدث التغييرات الأساسية
بحث
إبحار
المواضيع
أبجدي
بوابات
مقالة عشوائية
المشاركة والمساعدة
اتصل بنا
بوابة المجتمع
مساعدة
الميدان
تبرع
صندوق الأدوات
ماذا يصل هنا
تغييرات ذات علاقة
مساهمات المستخدم
سجلات
الصفحات الخاصة
نسخة للطباعة
وصلة دائمة
آخر تعديل لهذه الصفحة في 09:54، 19 أبريل 2009. كل النصوص منشورة تحت
رخصة جنو للوثائق الحرة (اقرأ حقوق التأليف والنشر للحصول على التفاصيل).
ويكيبيديا® علامة مسجلة لمؤسسة ويكيميديا.
سياسة الخصوصية حول ويكيبيديا عدم مسؤولية
Hans
Except when it is proved that P!=NP.
- Tim
"Hans H�ttel" <hansh...@mac.com> schrieb im Newsbeitrag
news:hanshuttel-DE24D...@news.stofanet.dk...
> Did nobody notice the date in the original post?
> April 1 2004
Not according to what I have here.
From: Martin Michael Musatov <marty....@gmail.com>
Subject: I Just Proved [P=NP] and I get to announce it on Usenet.
Newsgroups: comp.theory
Date: the 26th of April 2009 at 10:35
Organization: http://groups.google.com
But you're right that the text is copied from an earlier post, namely:
Newsgroups: comp.theory
From: h...@alpha1.csd.uwm.edu (Mark William Hopkins)
Date: 1999/04/01
Subject: P = NP Proof Soon To Be Published
Evidently, Martin thought it was funny and missed the usual Apr. 1
tradition in his repost.
--
"Now I realize that he got away with all of that because sci.math is
not important, and the rest of the world doesn't pay attention.
Like, no one is worried about football players reading sci.math
postings!" -- James S. Harris on jock reading habits