Talk:Boolean satisfiability problem/Archive 1
 | This is an archive of past discussions about Boolean satisfiability problem. Do not edit the contents of this page. If you wish to start a new discussion or revive an old one, please do so on the current talk page. |
| Archive 1 |
DO NOT EDIT OR POST REPLIES TO THIS PAGE. THIS PAGE IS AN ARCHIVE.
This archive page covers approximately the dates between the page creation and 18/10/2005.
Post replies to the main talk page, copying or summarizing the section you are replying to if necessary.
Please add new archivals to Talk:Boolean satisfiability problem/Archive02. (See Wikipedia:How to archive a talk page.) Thank you. Paolo Liberatore (Talk) 13:41, 19 October 2005 (UTC)
I understood that DNF boolean satisfiability is in P. This article seems to say it's NP-Complete. Since I'm not 100% sure of this, I'm not going to edit the article, but maybe someone else knows the definitive answer?
- Strange, you are right. It is easy to see that it is in P; a formula in DNF is satisfiable iff there is a clause without a contradiction. And that can be checked in linear time. What is also strange is the claim that the proof of NP-completeness is rather simple. As an instructor I have taught that proof myself, and even I don't think it's easy. :-) I'm a bit time-pressed at the moment, but I will put this on my to-do list. -- Jan Hidders 17:26 Dec 6, 2002 (UTC)
3-sat vs 2-sat
3-sat is NPC and 2-sat is not, why is it so?
It becomes a little strange because it means that it is not possible in polynomial time to convert from 3-sat to 2-sat in general.
This seems to be a little mystery to me.
- There are formulas you can express in 3SAT that are not expressible in 2SAT. So it is not even possible in exponential time or, for that matter, in any time. Take for example the formula f = (X1 or X2 or X3). How would you express that with a conjunction of clauses with just 2 variables? The proof that this is not possible is fairly simple. -- Jan Hidders 20:36, 9 Jun 2004 (UTC)
- The intuition is that 2CNF formulas merely express a conjunction of implications (because A or B is the same as (not A) implies B.) The constraints you can express with 3CNF formulas are potentially much more complex. An example of this is that it's impossible to express the negation of the pigeonhole principle for k holes using 2CNF, because it requires exponential resolution steps to show that it's unsatisfiable, and I believe that any 2CNF formula can be show unsatisfiable in a polynomial resolution steps (since only more terms with two literals can be generated, and there's only 4n2 possible such terms). The surprising thing, though, is that the pigeonhole principle formulas have O(n2) terms, and all but O(n) of them do in fact have two literals. Deco 7 July 2005 06:29 (UTC)
Proof of NP-completeness
I cut a section giving a "proof" that SAT is NP-complete, which I give below. I cut this section because it isn't really a proof, hardly even an outline, and because it uses concepts not developed in this article, such as Boolean circuit. It looks to me as though the author of this material was following the presentation in Christos Papadimitriou's book Complexity Theory, which presents a way to encode problems in NP as Boolean circuits first and then proves Cook's theorem as a corollary. I think that in Wikipedia it is better to give a direct proof, so I gave one in the Cook's theorem article. Gdr 20:53, 2004 Jul 21 (UTC)
Proof of NP-completeness
We give here a sketch of the proof of NP-completeness. To prove that SAT is NP-complete we must show that
- SAT is in NP, and
- all other NP problems can be reduced to it in polynomial time.
First, notice that it is easy to verify a YES answer: simply plug in a given set of variable values and see if they make the expression true. Therefore the problem is in NP.
Next, consider an arbitrary problem X that is in NP. By definition, there must be an algorithm for checking certificates for YES answers to X in polynomial time. Given such an algorithm it is possible to construct a polynomial-time algorithm that, given the size of the certificate, constructs a boolean circuit that is polynomially large in the certificate size and decides whether its input is a binary encoding of a valid certificate or not. This circuit can then be transformed by another polynomial-time algorithm into an equivalent boolean formula that is still polynomially large in the certificate size. It then holds that this formula is satisfiable iff there is a valid certificate, which means that we have reduced the original problem to SAT.
- I believe you are engaging in a circular proof. You're indirectly using Cook's theorem, aren't you? You can't use a theorem's result to prove the same result... Rbarreira 7 July 2005 02:51 (UTC)
- Agreed. We really have to give a reduction from an arbitrary NP problem somewhere, although it would've been fine to follow Papadimitriou's route and add a proof to the article on boolean circuits (whichever is simpler). Deco 7 July 2005 06:20 (UTC)
Classes of algorithms for SAT
There are two classes of high-performance algorithms for solving instances of SAT in practice:
- Well actually, there is also Stalmarck's procedure, which is very different from DPLL and from the stochastic methods. It should be mentioned, too. --zeno 10:54, 8 Apr 2005 (UTC)
“P = NP” Proved! (Solution Algorithm for 3-SAT)
The following proof of P=NP, submitted by an anonomous editor, should be presumed wrong because it has not been published in a peer-reviewed scientific journal. Other editors have commented that the proof appears wrong, but it is not their duty to prove it, as encyclopedias are not places for original research: see WP:NOR. Do not post other proofs about P=NP here unless they have already been published in peer-reviewed scientific journals.
The equivalence of the P and the NP computational complexity classes is proved by presenting a very simple procedure for the practical solution of the NP-complete Boolean satisfiability 3-SAT decision problem. Using some kind of a Gödel prime natural numbers coding plan, polynomial-time algorithms are established for finding the respective assignment solutions to every group of input clauses with the same variables and for determining from them the valid assignment solutions to the 3-SAT problem.
Theorem 1: Let C be a clause and P be a variable. Then (C Ú P) Ù (C Ú ~P) = C.
For a given 3-SAT problem with n variables P1, P2, P3, . . ., Pn:
- The input clause(s) that include the same k (1 £ k £ 3) variable(s) could be grouped together — the maximum count of these groups is the number nCk of combinations of n distinct objects taken k-at-a-time. For each group, there are at most 2k possible length-k input clauses. All 2k possible length-k clauses cannot be specified as input clauses at the same time because this would lead to a self-contradiction.
- There could only be at most n possible input clause(s) that use only 1 variable since no variable Pj (1 £ j £ n) can appear in one length-1 input clause as “Pj” and as “~Pj” in another length-1 input clause because this would bring about a self-contradiction — Pj Ù ~Pj — and, indubitably, one of them is not satisfiable by any truth-value assignment to Pj so there is no assignment solution to the 3-SAT decision problem. The length-1 input clause(s), if any, already fixes the truth-value(s) of their respective variable(s) in the assignment solution. Hence, they could actually be dispensed with in any 3-SAT decision problem and the number of variables reduced.
- By Theorem 1, any length-2 input clause — Pi Ú Pj — could always be replaced by 2 length-3 clauses — Pi Ú Pj Ú Pk and Pi Ú Pj Ú ~Pk. These replacements (as well as the replacements of one length-1 input clause by four length-3 input clauses) only involve polynomial-time computations. Hence, it suffices to just work with 3-SAT decision problems with input clauses having exactly 3 distinct variables.
Definition: The assignment solution <P1, P2, P3, . . ., Pn> is the term-wise falsification of the clause Pi1 Ú Pi2 Ú Pi3 Ú . . . Ú Pin if and only if for all natural number j, 1 £ j £ n: Pj = “True” if Pij = “~Pj” (Pj is negated in the clause);
= “False” if Pij = “Pj” (Pj is not negated in the clause).
- For example, the assignment solution <True, False, False> is the term-wise falsification of the clause ~P1 Ú P2 Ú P3. The clause evaluates to False upon the substitution of the assignment solution’s truth-values — that is, the former is not satisfied by the latter.
Theorem 2: For any natural number n ³ 1, every valid assignment solution to an n-CNF-SAT problem (that is, a CNF-SAT problem whose input clauses use exactly n variables) is simply the term-wise falsification of a clause that was not specified among its input clauses.
Proof: First, we observe that, for n variables, there are at most 2n possible clauses Ci = Pi1 Ú Pi2 Ú Pi3 Ú . . . Ú Pin , 1 £ i £ 2n that could be set up and there are the same maximum number 2n of possible assignment solutions <P1, P2, P3, . . ., Pn> to the n-CNF-SAT decision problem.
Next, we emphasize that each assignment solution <P1, P2, P3, . . ., Pn> satisfies all the 2n possible clauses except for one clause— its term-wise falsified clause. This is easily deduced from the following facts:
- The truth-value of P1 satisfies half (that is, 2n-1) of all the 2n possible clauses;
- The truth-value of P2 satisfies half (that is, 2n-2) of all the 2n-1 possible clauses not satisfied by P1;
- The truth-value of P3 satisfies half (that is, 2n-3) of all the 2n-2 possible clauses not satisfied by P1 and P2;
. . .
- The truth-value of Pn-1 satisfies half (that is, 2) of all the 22 = 4 possible clauses not satisfied by P1, P2, P3, . . ., and Pn-2;
- The truth-value of Pn satisfies half (that is, 1) of all the 21 = 2 possible clauses not satisfied by P1, P2, P3, . . ., and Pn-1; and
- The sole possible clause not satisfied by the assignment solution <P1, P2, P3, . . ., Pn> is simply its term-wise falsified clause.
Therefore, for every possible clause that was not specified in the input, we could obtain a valid assignment solution <P1, P2, P3, . . , Pn> — which is just the term-wise falsification of that unused clause in the CNF formula.
A simple computer program implementation of the above algorithm for finding a valid assignment solution <P1, P2, P3, . . , Pn> to an n-CNF-SAT decision problem might proceed as follows:
- For each n-CNF-SAT (n = 1, 2, 3, . . .) decision problem, the 2n possible clauses are assigned code numbers using the prime natural numbers and the all-clause-codes-product n-ACCP is evaluated.
- The standard clause code assignment tables are:
Variables Clause Code
--------- --------------- --—–
n = 1 Pi 2
~Pi 3
n = 2 Pi Ú Pj 5
Pi Ú ~Pj 7
~Pi Ú Pj 11
~Pi Ú ~Pj 13
n = 3 Pi Ú Pj Ú Pk 17
Pi Ú Pj Ú ~Pk 19
Pi Ú ~Pj Ú Pk 23 Pi Ú ~Pj Ú ~Pk 29 ~Pi Ú Pj Ú Pk 31 ~Pi Ú Pj Ú ~Pk 37 ~Pi Ú ~Pj Ú Pk 41 ~Pi Ú ~Pj Ú ~Pk 43
- For very large n, the n-ACCP could be an extremely large number. It is stressed that the use of the prime natural numbers for clause code is just to ensure simple prime factorization of the clause codes product. Hence, we could also use character-type string clause codes instead of prime numbers, string concatenation instead of number multiplication, string deletion instead of number division, and in-string comparison for divisibility test.
- The input-clause-codes-product ICCP is computed by multiplying the prime number clause codes of all the given input clauses.
- The constant all-clause-codes-product n-ACCP is divided by the input-clause-codes-product ICCP and the distinct prime factors of the quotient are delineated (for a 3-SAT problem, the prime factorization here merely involves tests for divisibility by the first 21 + 22 + 23 = 14 prime natural numbers) — the latter identifies all the possible clauses that were excluded or not specified as input clauses.
- Each valid assignment solution is readily obtained from the term-wise falsification of each excluded clause.
Suppose a given 3-CNF-SAT problem has the following input clauses:
- C1 = P1 Ú P2 Ú P3 [17]
- C2 = P1 Ú ~P2 Ú P3 [23]
- C3 = ~P1 Ú P2 Ú P3 [31]
- C4 = ~P1 Ú P2 Ú ~P3 [37]
- C5 = ~P1 Ú ~P2 Ú P3 [41]
Then, the input-clause codes-product ICCP = 17 • 23 • 31 • 37 • 41. Therefore,
3-ACCP 17 • 19 • 23 • 29 • 31 • 37 • 41 • 43
------– = ---------------------------------------
ICCP 17 • 23 • 31 • 37 • 41
= 19 • 29 • 43
— so the excluded clauses and their respective assignment solutions are:
Code Excluded Clause Assignment Solution
———— ----------------- ----------------------
19 P1 Ú P2 Ú ~P3 < False, False, True >
29 P1 Ú ~P2 Ú ~P3 < False, True, True >
43 ~P1 Ú ~P2 Ú ~P3 < True, True, True >
Definition: The assignment solution <Pa, Pb, . . ., Pk> to a k-CNF-SAT problem is a sub-solution of the assignment solution <P1, P2, P3, . . ., Pn> to its parent n-CNF-SAT decision problem if and only if {Pa, Pb, Pc, . . ., Pk} Í {P1, P2, P3, . . ., Pn}.
Theorem 3: Every valid assignment solution <P1, P2, P3, . . ., Pn> to a 3-SAT decision problem is simply a consistent (that is, it is not self-contradictory variable-truth-value-wise) union of one valid group-assignment-solution <Pa>, <Pa, Pb>, or <Pa, Pb, Pc> from every group of input clause(s) which involve the same 1, 2 or 3 variable(s).
The number theory concepts of divisibility and greatest common divisor of 2 or more natural numbers a, b, c, . . ., n —
a|b if and only if b = aq for some natural number q;
d = gcd(a,b) if and only if d|a, d|b and (c|a Ù c|b) ® (c|d);
gcd(a,b,c,...,n) = gcd(gcd((gcd(a,b),c),...),n)
— could be promptly invoked to easily establish the formation, from the valid group-assignment-solutions to the groups of input clause(s) which involves the same 1, 2 or 3 variable(s), of appropriate sub-solutions to a valid assignment solution to a 3-SAT decision problem.
- Let P1T, P1F, P2T, P2F, . . ., PnT, PnF be the respective prime natural number literal code to every one of the 2n possible truth-values of the n variables of a 3-SAT decision problem.
- For each valid group-assignment-solution of every group, let us form a product of prime number literal codes by multiplying the actual prime number literal code(s) of all the variable(s) used in the group-solution and the 2 possible prime natural number literal codes of all the other unused variables in the said group-solution.
- The computations of products of prime number literal codes is not compulsory — it is proffered simply to make straightforward the determination of divisibility and the greatest common divisor among the group-assignment-solutions — that is, just to avoid the cumbersome conditionals of verifying the existence of 1 or 2 common variable(s) between two group-assignment-solutions of 2 different groups of input clause(s) with the same 1, 2 or 3 variable(s) before evaluating their divisibility status.
- An alternate way to compute the product of prime number literal codes for each group-assignment-solution is to keep the constant all-literal-codes-product — n-ALCP = P1T•P1F•P2T•P2F•P3T•P3F• . . .•PnT•PnF — and then dividing it by the prime number literal code(s) of each variable in the excluded clause — that is, by PjF if Pj is negated, and by PjT if Pj is not negated, in the excluded clause.
- For the groups of length-k (1 £ k £ 3) input clauses, this entails 2n – k factors for the product of prime number literal codes — for very large n, this could be an extremely large number. It is reemphasized that the use of prime natural numbers for literal codes is just to ensure simple prime factorization of the literal codes product. Therefore, we could also use character-type string literal codes instead of numeric-type prime numbers, string concatenation instead of number multiplication, string deletion instead of number division, as well as in-string comparison for divisibility test.
- As already noted earlier, for a 3-SAT problem with n variables, there are at most nC1 = n!/1!(n-1)! = n groups of single variable clauses with a maximum of 21 – 1 = 1 group-assignment-solution per group, and a maximum of nC2 = n!/2!(n-2)! = n(n-1)/2 groups of input clauses having the same 2 variables with at most 22 – 1 = 3 group-assignment-solutions per group, and at most nC3 = n!/3!(n-3)! = n(n-1)(n-2)/6 groups of input clauses having the same 3 variables with at most 23 – 1 = 7 group-assignment-solutions per group.
- In hindsight, the number of possible combinations of 1 group-assignment-solution from each group is of the order 7 raised to the exponent n3 — that is, to find all valid assignment solutions to a 3-SAT problem from its group-assignment-solutions would appear to involve exponential time computations. However, our simple algorithm straightforwardly constructs all of the possible assignment solutions to a 3-SAT problem — that is, it does not back up to try other combinations of group-assignment-solutions — and, at the ending of the verily deterministic polynomial-time procedure, categorically concludes that either there is no valid assignment solution to the parent 3-SAT decision problem or it definitely identifies all of them. Moreover, our algorithm stops forthrightly — that is, it does not have to continue the process — when it determines fatal inconsistencies between all the valid group-assignment-solutions of 2 groups of input clauses.
- Following Theorem 3, we could readily ascertain that no valid assignment solution to the 3-SAT decision problem could come up if all the group-assignment-solution(s) to some group of input clause(s) with the same 1, 2 or 3 variable(s) are inconsistent with all group-assignment-solution(s) to at least one of the other group of input clause(s) with which the former group shares 1 or 2 variable(s). Hence, to establish that a 3-SAT decision problem has no valid assignment solution, it is sufficient to look at a group of input clause(s) (for ease, one takes the group with the least number of group-assignment-solutions) and to check that none of the latter’s group-assignment-solutions divides at least 1 of the group-assignment-solutions of a different group of input clause(s) with which the former group has a common 1 or 2 variable(s).
- Using the products of prime number literal codes, the procedure is highly simplified because we could take advantage of the fact that the greatest common divisor of some set of natural numbers divides every natural-number-element of the given set and if their greatest common divisor consists of exactly n prime natural number factors — representing 1 prime number literal code for the actual truth-value of each variable — then we have also found a valid assignment solution to the parent 3-SAT problem.
- Because there are at most O(n3) of group-assignment-solutions, then there are only a maximum of O(n3) evaluations of greatest common divisors — therefore, our algorithm certainly involves only polynomial-time computations. As a matter of fact, because there are at most 2n - 1 factors in the product of prime number literal codes (which is the starting greatest common divisor) and considering a realistic reduction of 1 prime number factor for each computation of greatest common divisors between groups, then it would take only O(n–1) calculations of greatest common divisors until a greatest common divisor with exactly n prime number factors is attained.
- Beginning from a group A of input clauses having the same 1, 2 or 3 variables with the least number g of valid group-assignment-solutions, its products of prime number literal codes are set up as initial greatest common divisors gcd1a (1 £ a £ g).
- For each product of prime number literal codes PPNLC2b from the second group B of input clauses with the least number g, or next least number h, of group-assignment-solutions, its greatest common divisor gcd2b (1 £ b £ g|h) with every gcd1a is evaluated — this only involves g2 or g ´ h computations. Because we had intentionally used prime natural numbers for literal codes, it is easier to compute the greatest common divisors gcdab(gcd1a,PPNLC2b) by simultaneous divisibility tests by the first 2n prime numbers of both gcd1a and PPNLC2b instead of, say, Euclid’s algorithm. If, for some j < n, both PjT and PjF do not divide both gcd1a and PPNLC2b, then we already know that this particular gcdab is inconsistent so we do not have to continue with the divisibility tests for the rest of the prime number literal codes for this instance of gcdab and it is simply discarded.
- If no gcdab has at least 1 of the 2 prime number literal codes for each variable dividing it, then the 2 groups have inconsistent group-assignment-solutions so, by Theorem 3, no combination of their group-assignment-solutions could both be sub-solutions of the same valid assignment solution to the parent 3-SAT decision problem. Our decision algorithm stops here with the definite conclusion that the original 3-SAT problem has no valid assignment solution.
- All the gcdab that are inconsistent greatest common divisors are discarded. For every gcdab with at least 1 of the 2 prime number literal codes for each variable as factors, its greatest common divisors gcdabc with every product of prime number literal codes PPNLC3c from the next group C of input clauses with the least or next least number of group-solutions are computed.
- Unless a fatal inconsistency ensued for some group G of input clauses — that is, if there is no gcdabc...g with at least 1 of the 2 prime number literal codes for each variable as factors — the immediately preceding steps are repeated for all the z groups of input clauses. Once a greatest common divisor gcdabc...g with exactly n prime number literal codes factors had been reached, then it is better to simply test for divisibility by gcdabc...g the products of prime number literal codes of the succeeding groups.
- In the end, every gcdabc...z with exactly n prime number factors — that is, P1X • P2X • P3X • . . . • PnX (X Î {“T”,“F”}), one for each truth-value of every variable Pj (1 £ j £ n) — decoded for their actual truth-values, absolutely provides a valid assignment solution <P1, P2, P3, . . ., Pn> to the original 3-SAT decision problem.
- We reiterate that our simple algorithm is truly deterministic and verily involves only polynomial-time computations — since we invoked prime number clause and literal codes, our calculations of greatest common divisors and prime number factorization are straightforward divisibility tests of the first 2n prime numbers.
- Moreover, our simple algorithm not only decides the satisfiability of the input clauses of a given 3-SAT problem, it returns all the valid assignment solutions.
We can now summarize our simple polynomial-time algorithm [implemented as a relational database management system (RDBMS) application program that uses the standard Structured Query Language] for deciding a given 3-SAT problem as follows:
- The following prime number literal code assignments are labeled to the possible truth-values of each variable Pj, 1 £ j £ n:
Pj = “True” assign the (2j – 1)th prime number as PjT; and
= “False” assign the (2j)th prime number as PjF.
Thus: P1T = 2, P1F = 3, P2T = 5, P2F = 7, P3T = 11, P3F = 13, etc.
- The 3-SAT problem input clauses are entered into a database table Input_Clauses_Table with two fields:
- Group_ID — a character-type data field of comma-delimited name(s) of the variable(s) involved in the particular input clause [this is an index field]; and
- Clause_Code — a numeric-type data field of the standard prime number clause code for the form of the particular input clause.
- With just one SQL SELECT command on the Input_Clauses_Table records — following the simple polynomial-time algorithm presented earlier to find all of the respective valid group-assignment-solutions <Pa> or <Pa, Pb> or <Pa, Pb, Pc> to each group of the-same-1|2|3-variable(s) input clause(s) of the given 3-SAT decision problem with n variables — a Group_Assignment_Solutions_Table database table is readily created with the following fields in addition to Group_ID:
- Group_Solution — a numeric-type data field of the product of the prime number literal code of the actual truth-value of each variable in the term-wise-falsification of each excluded clause of every group of input clause(s) with the same 1, 2 or 3 variable(s);
- Product_of_Prime_Number_Literal_Codes — a numeric-type data field of product of the actual prime number literal code(s) of all the variable(s) in the value of the Group_Solution field and the 2 possible prime number literal codes of all the other unused variables in the Group_Solution field value.
- The group(s) in the Group_Assignment_Solutions_Table with only 1 valid group-assignment-solution record already have fixed assigned truth-value(s) for the variable(s) in their respective Group_ID field value(s) so they can be used to purge the inconsistent-to-them records from Group_Assignment_Solutions_Table. Hence, every record in Group_Assignment_Solutions_Table whose value for its Product_of_Prime_Number_Literal_Codes field is not divisible by the value of the Group_Solution field of sole-record group(s) in the Group_Assignment_Solutions_Table are to be deleted. If the purged Group_Assignment_Solutions_Table contains new sole-record group(s), then the deletion of inconsistent-to-them records continue for the new single-record group(s).
- For every record of the first group with the same Group_ID in the database table Group_Assignment_Solutions_Table, a respective Possible_3_SAT_Assignment_Solution_Table_Number database table is created with the following field in addition to Group_ID and Product_of_Prime_Number_Literal_Codes:
- Current_Greatest_Common_Divisor — a numeric-type data field for the recurrently computed greatest common divisor.
- The Possible_3_SAT_Assignment_Solution_Table_Number table correspondingly records the possible sub-solutions that made up a valid assignment solution to the parent 3-SAT decision problem — if this information is not desired, then this table could be dispensed with.
- Each Possible_3_SAT_Assignment_Solution_Table_Number has a respective initial record corresponding to the record(s) of the first group in the database table Group_Assignment_Solutions_Table with the Product_of_Prime_Number_Literal_Codes field’s value also assigned at first as the Current_Greatest_Common_Divisor field’s value.
- A database table Greatest_Common_Divisors_Table is also created with this field in addition to Current_Greatest_Common_Divisor:
- Possible_3_SAT_Assignment_Solution_Table_Reference — a character-type data field for the actual name of the table Possible_3_SAT_Assignment_Solution_Table_Number that involves the Current_Greatest_Common_Divisor field value. [If Possible_3_SAT_Assignment_Solution_Table_Number database tables are dispensed with, then so must this field be.]
- The database table Greatest_Common_Divisors_Table keeps track of the computed greatest common divisors that remain feasible to provide a valid assignment solution to the 3-SAT decision problem.
- Corresponding to each record of the first group in the database table Group_Assignment_Solutions_Table, or corresponding to every Possible_3_SAT_Assignment_Solution_Table_Number database table’s initial record, a matching related record in the database table Greatest_Common_Divisors_Table is also initially inputted.
- For each Product_of_Prime_Number_Literal_Codes field’s value, of every record in the second group of group-assignment-solutions in the Group_Assignment_Solutions_Table, their greatest common divisors with the Current_Greatest_Common_Divisor field’s value of all the records in the Greatest_Common_Divisors_Table are evaluated. If there is no fatal inconsistencies, then the process is repeated for each succeeding group of group-assignment-solutions in the Group_Assignment_Solutions_Table.
- If the procedure is completed for all the groups of group-assignment-solutions in the Group_Assignment_Solutions_Table without any fatal inconsistency, then every Current_Greatest_Common_Divisor field’s value of each record that remained in the database table Greatest_Common_Divisors_Table provides, after its appropriate decoding, a valid assignment solution to the 3-SAT decision problem.
BenCawaling@Yahoo.com [12 July 2005]
- Your text is all screwed up. Maybe it would be a better idea to publish a pdf with this. Have you implemented tried implementing this algorithm? Do you trust it? Rbarreira 17:06, 13 July 2005 (UTC)
- There are several problems with this argument, and I thank you for not adding it immediately to the article. Here are a few of its problems:
- Next, we emphasize that each assignment solution <P1, P2, P3, . . ., Pn> satisfies all the 2n possible clauses except for one clause— its term-wise falsified clause.
- This is true, but only in reference to the universe of all clauses of length n, where n is the number of variables, of which there are 2n. The clauses in the input are usually much shorter, and if you were to extend them all to n variables, there would be exponentially many clauses. This amounts to enumerating all assignments which fail to satisfy.
- Therefore, for every possible clause that was not specified in the input, we could obtain a valid assignment solution <P1, P2, P3, . . , Pn> — which is just the term-wise falsification of that unused clause in the CNF formula. [...] Each valid assignment solution is readily obtained from the term-wise falsification of each excluded clause.
- That's not true at all - many of the "unused"/"excluded" clauses are implied by the input clauses. A good example is the formula for the pigeonhole problem, where an exponential number of clauses not in the input are implied by the clauses in the input. The algorithm would be trivial if it sufficed to locate a clause not given in the input.
- The prime-based encoding seems like it might be a good idea, although I didn't look at it too closely (I stopped at the above part), but I don't think this algorithm can be saved. Deco 17:37, 13 July 2005 (UTC)
- Yes, thank you for not adding it immediately to the article. Some major problems:
- It is very hard to understand the algorithm in terms of SQL.
- Every "theorem" is trivial, and well-known, for example, Theorem 1 follows from the definition of the resolution proof system, it is better just add links to papers/books where there are proved.
- The algorithm uses exponential amount of memory for the product of all assignments for variables. So it is not polynomial time algorithm.
- It is very easy to test any algorithm with help of benchmarks from SatLib ;) --Aristk 13:15, 14 July 2005 (UTC)
- The prime based encoding is merely a (tortured) representation that permits use of division, multiplication & gcd in place of boolean operations, *increasing* the complexity of a solution. That leaves only the last 2 sentences as relevant to the "method", which doesn't work. The iterative process described, if implemented so that it generates a correct answer in the "gcd" table requires 2^n operations and just as many rows in the table. In other words, exactly what the method was supposed to avoid. This is obviously a crank proof. The original author is no where to be found, and it seems to me he tried it with 7 variables (a-g), which because of the representation structure, just happens to iterate to a correct solution. I vote that it be deleted.
Jok2000 23:06, 11 October 2005 (UTC)
- The proof of P=NP, regardless of correctness, has not been published anywhere else. If correct, it should be first published in a computer science journal, not in an encyclopedia (see WP:NOR). Even the talk page is in this case an inappropriate place for it. However, deleting is may be confusing because old versions of the pages are always accessible. I added a box at beginning of the proof saying that this proof has not been endorsed by anyone else beside the (anonymous) author, that some editors think it is flakey, and that this is not the place for publishing original reaseach to begin with. Paolo Liberatore (Talk) 11:23, 12 October 2005 (UTC)