Well, this is somewhat heartbreaking for me. I haven't read the paper, but the result sounds very plausible to me.
I am also an amateur working on P=NP. Last week, I think I also proved that P=NP, but with a different method, and was about to seek publication.
My result seems very similar to his, yet very different. I can prove that class of SAT which is intersection of 2SAT and XORSAT is NP-complete by reduction to 3-SAT. Then I follow the approach in Melville's Krom 1967 paper on 2-SAT, and prove that certain polynomial-sized logic (that corresponds to the intersection) is refutable complete. So you can essentially generate all formulas in that logic and if you don't find contradiction, the instance is satisfiable.
I have also did some preliminary testing of my method, and was able to factor small integers with it. However, there was a bug.
So, to sum up, I am not surprised that P=NP with a constructive and efficient algorithm. Take it for what you want. The future is gonna be interesting (crypto DOOMSDAY).
I don't understand. You said that you thought you proved P=NP, but then it turned out you hadn't.
How does this help to support your belief that P=NP has been solved by someone else? Surely it wouldn't surprise you if it turns out they were as wrong as you were before?
PS: Also, reducing 2SAT to 3SAT doesn't help proving that P=NP. The opposite reduction would, if you were able to do the reduction in polynomial time. But maybe I misunderstood something about what you attempted.
I think I have a proof, it's just not yet published. Also, the original method I was attempting contained a bug, but I understand the theory better now.
So, I have some evidence, both experimental and theoretical, there is an efficient polynomial algorithm out there (and possibly many different methods).
Unfortunately, not 100% verified because despite what many smartypants are saying here, it's incredibly difficult to even have a conversation about a possibility of a relatively uncomplicated proof that P=NP. (I think Millenium prize is part of the problem, but that's another discussion).
And to clarify, I am reducing 3-SAT to 2XSAT, not 2-SAT. 2XSAT generalizes 2-SAT to arbitrary linear equations rather than literals (we can think of a literal as a linear equation on 1 variable).
I will happily send you (or anybody) the draft I have, so that you can critique it.
Nobody wants to read your draft about an algorithm that doesn't work. Your implementation is already giving you the critique that you need. If you get it to work and it's obviously polynomial time, you'll have something to talk about.
I don't think this is quite true. Most NP-hard problems are usually solvable in polynomial time, so your algorithm looking like it runs in polynomial time doesn't tell you much.
It really depends. If you have an unbounded loop that looks like it runs in polynomial time, you're in highly questionable territory. If you have a 5-deep nest of for-loops, that's what I call "obviously polynomial time" -- if such an algorithm solves every problem you throw at it, you have hope.
As <cat-over-keyboard> already mentioned, it's not always that simple. For example, my current approach (modeled after Krom, who doesn't even have a Wikipedia page - no wonder nobody reads him!) is a more systematic search for a polynomial algorithm - construct a polynomial sized-logic in which theories have models that are satisfying instances of SAT, and prove its refutable-completeness. This proves existence of a polynomial algorithm, because you can generate all formulas of theory (coming from SAT instance) in said logic, and if you don't find a contradiction, the instance is satisfiable. The algorithm is kinda implicit, non-deterministic, if you will (because you can generate all the formulas in any order or even generate just a subset).
Anyway, my main point is - people beware, practically solvable P=NP (even for hard instances) is a very real possibility.
Sure, but most complicated polynomial time algorithms don't work like this. You either have cases like AKS which are obviously polynomial but not obviously correct, or cases that are obviously correct but not obviously polynomial.
Algorithms which are obviously polynomial, and non-obviously correct are the only ones I'd entertain from a novice. It's not hard to mine for counterexamples, as long as the code runs.
I think this is exactly the unhelpful tactics that have prevented people figuring out the problem. I have both theoretically and practically verified the 2XSAT reduction, and I believe it's a step towards P=NP. But, it's being dismissed out of hand because I don't have a practical, fully polynomial, algorithm.
So I cannot publish that (I am well aware of the unfortunate situation that only a practical implementation will now convince people that P=NP).
Add to it, why should I? What if it's not that far from a full solution, and somebody else will get the prize?
I came to understand why Perelman refused the prize. Mathematics should be about collaborative understanding of the universe, not about people working in isolation until they have fully working superoprimized implementation that can crack Bitcoins.
I have both theoretically and practically verified the 2XSAT reduction, and I believe it's a step towards P=NP.
NP is generally thought to be harder than factoring, so I'm not sure that your reduction is a "reduction" in the sense that you've restated factoring in a (potentially-)harder-than-native problem space. Proving that factoring is polynomial would be a huge result indeed, but if your strategy requires you to prove P=NP along the way, you're focused on the wrong problem and I wouldn't expect you to get much traction.
If your reduction can solve factoring, what are the factors of 22112825529529666435281085255026230927612089502470015394413748319128822941402001986512729726569746599085900330031400051170742204560859276357953757185954298838958709229238491006703034124620545784566413664540684214361293017694020846391065875914794251435144458199?
I already said, I don't have an efficient algorithm. Once I will have, in my estimation, at best, it will be O(n^3) (n is number of variables), which still means a lot - to factor 16-bit integer, my (linear) 2XSAT reduction requires about 4000 variables, so the number of variables for a cryptographically-strong problem will be in millions. You need to have a very efficient parallel algorithm to deal with that, and that's very low on the list of priorities - first I need to understand how to actually make the algorithm efficient (so far I think I proved there is a polynomial bound - around O(n^8) or so, but I know for sure it's very inefficient, because I am doing it very naively).
There are other ways to improve the method, which (if indeed P=NP) are incredibly interesting - you can directly compose presolved general instances and specialize on them. Kinda like if you need to compute many solutions to linear equations, you only need to factor the matrix once.
Why don't you try testing your algorithm on some 1000 variable or so SAT instances ? There are thousands of such problems that have been created for the SAT competitions. If your code can solve all of them and is really P-time then I think there are many people who would be interested in looking at your algorithm, myself included.
That's what I am generally doing and planning to do, however right now, the theory had priority (there is still couple weak spots in my proof which I need to patch up). But I will return to testing once I will have a better idea what I want the algorithm to do (as I mentioned, a more naive version of the method that combined solving 2-SAT and XORSAT failed with a bug, which I think I now understand).
I think testing O(n^8) algorithm is pointless, so it needs more polishing (naive algorithm for 2-SAT (that follows from Krom) is O(n^3) or so, but the best methods are linear; so I feel there is a lot of room for improvement, but obviously my method is a little bit more complicated than 2-SAT, which it generalizes).
There's one thing I'd like to get some clarification on. You said in an earlier comment:
I am reducing to 2XSAT, which is a name for instances that are intersections of 2-SAT and XORSAT instances.
It seems to me that 2-SAT and XORSAT are distinct problems. I mean there is no problem instance that is simultaneously a 2-SAT problem and an XORSAT problem instance. So how can there be instances that are intersections of both ?
The 2XSAT has clauses that are from 2-SAT or XORSAT. So it's a generalization of both. The solutions (boolean variable assignments) must satisfy both 2-SAT and XORSAT part of the problem, hence the solutions of the 2XSAT instance is their intersection.
There are in fact problems that are both 2-SAT and XORSAT, but they seem to be rather trivial - those are linear equations that have up to 2 variables per equation. But that's not what I am talking about.
I understand why people are confused with my off-hand comments, but I didn't plan to explain my approach here in detail, and I typed the first couple of comments when I was at work on my phone, where being precise is tedious.
No, you misunderstand, the intersection is in the solution to the instance. The 2XSAT are problems that can contain both 2-SAT clauses (two literals per OR clause) and XORSAT clauses (linear equations). 2-SAT (as well as XORSAT) are just special cases of that. You can also think of it as 2-SAT, but confined into a linear subspace of Z_2^n.
That isn't the intersection of 2SAT and XORSAT, it's the union. Problems in the intersection would be solvable by either type of solver. I don't think it's "obvious" that your problem class should be polynomial; 2XSAT as you've described it (is it your own invention? I haven't found a reference) appears to be a strictly more powerful problem class.
It's not a union of those classes, it's a different class, and as you say, it's more powerful, because it can be projected (my reduction adds additional variables) into 3-SAT and SAT instance.
Yes, 2XSAT is the name I gave it, and I couldn't find it anywhere. The reduction is surprisingly simple, yet nobody mentions it. That's why I am warning people here - just based on this alone, I 80% believe that P=NP with a practical algorithm (which either way involves solving linear equations). And I wouldn't be surprised somebody coming up with the algorithm.
The reason why I say it's an intersection is because that's how the set of solutions of an instance looks like. That's what we need to figure out - how to characterize the sets of solutions described by SAT instance (i.e. sets of assignments to boolean variables that satisfy the instance).
However, it's not that easy, even if you characterize them as interesections of 2-SAT and XORSAT instances, set of solutions to 2-SAT is notoriously hard to characterize too, for example, #2SAT is not known. And polynomial algorithms for 2-SAT and XORSAT are doing very different things, and it's not at all obvious how to generalize them into a common algorithm that can do both.
As a mathematician, my advice to you is to build up some theory around this problem class. I find it entirely plausible that you can reduce 3sat to it. I'd encourage you to look for a reduction from 2XSAT to 3sat. Find some problems that are well-expressed in the language of 2XSAT. You might find something worthy of publication. From there you'll want to shop your results around at conferences. You may drum up some interest in your work, or even a collaborator. Just don't act confident that you've cracked a keystone problem in the field. You think you're on the right path, and that's exciting, but we've all been there and we've all met dozens of novices who were utterly convinced of their incorrect solution to this problem. It's a huge red flag that you're a waste of time.
As a grad student, I got perhaps hundreds of "dear professor" emails claiming proof of everything from squaring the circle to the BSD conjecture. Reflexively running from anybody making such claims is a necessary survival skill. Math is a field where the bullshit asymmetry principle[1] is particularly stark. Finding a flaw in a proof can take vastly more effort than is spent concocting it.
The opposite reduction from 2XSAT to SAT is obvious, it's just a special case.
I think professionals of every field have to deal with passionate amateurs of all levels. I understand why many people don't want to do it, but IMHO overemphasis on professionalism (culturally coming from enormous peer pressures) is hurting any field. The superprizes make it even worse.
Just don't act confident that you've cracked a keystone problem in the field.
I am not acting like that, but I also have to be honest that my goal is specific - to understand why we can or can't have a polynomial algorithm. I.e. I have a strategy already, what I need is a 2nd opinion about some specifics of it.
Honestly, I don't think you have the proof.
Proving p is euqal to np will have very big consequences, not only in computer science but also in logics for example.
I think this problem is far more complex than you think and it is not going to be solved by chance by an amateur. If it's going to be solved, there will be a deep math argument.
Mathematics should be about collaborative understanding of the universe
If you really think mathematics should be about collaboration and not competition, why do you worry about who gets the prize?
You should pick what's more important to you - if it's collaboration, why not publish the steps you've accomplished? If someone else uses it to achieve a full solution, you'll still have a claim to part of the credit towards the solution.
Because I am also a human. I think I could still use the money (if anything, very few people want to be principled idiots who refuse $1m), and if I spent several years determined to understand it, perhaps it's worth spending some more to understand it fully. As I explained, it creates an atmosphere that prevents collaboration - it's incredibly hard to find anyone to talk about the problem with. Anyway, I am writing about my approach here, and I am about to write about it more. Still, people dismiss it outright.
I haven't really studied it in detail, but my motivation is similar, I see SAT as a simplified version of the marginal problem, and I want to solve marginal problem (or at least approximate) because I am interested in representing knowledge intensionally.
I played with propagation a lot in the past, but I don't think local propagation (that resolves conditions of a bounded number of variables at a time, until everything stabilizes) can ever work, because it would contradict Razborov result on monotone circuits. I don't remember the exact argument, but I think it would imply a polynomial monotone circuit capable of resolving the instance. Also, XORSAT is not really amenable to this either, to solve arbitrary XORSAT instance you have to add together arbitrary number of linear equations, so the number of variables per equation can balloon up.
That's why more recently I focused on understanding what exactly is the role of XORSAT, and by serendipity, I stumbled upon the above-mentioned reduction (which I think is a really exciting result). XORSAT is great for testing different algorithms, because despite the fact we have a nice polynomial algorithm (Gaussian elimination), one can easily create arbitrary (and loopy) instances where propagation is difficult.
The way I see it, to avoid the problems with the bound, you need to preprocess the linear equations "inherent" in the instance by adding extra variables. The exact way to add variables depends on the instance, but it can be done by solving the linear equations. Propagation algorithms that go into the process blindly, without understanding the underlying linear structure, will mysteriously fail.
However, my current approach through logic, basically building up theorems about the instance, until it is decided, can be considered a generalization of the propagation approaches. The messages are true statements about variables, which are propagated by deduction rules of the logic. But this is done only after we have discerned the linear structure in the problem, which is addressed globally, as described above.
That jives with my intuition. I had forgotten about the connection between Gaussian elimination and xor sat. That does sound like a good direction to reason from.
How do you prevent an exponential increase in linear terms though?
I am still not sure about the exact role of Gaussian elimination. I thought that it will be somehow necessary, but it seems that if you only break linear equations to 3 variables per equation (by adding extra variables), you can get away without it. Although it certainly doesn't hurt to do it, I think for efficient algorithms, it will be required (and so the whole endeavor will be at least O(n^3)).
To prevent exponential increase in linear terms, I work within a sort of limited logic that only allows formulas that are ORs of (implications between) two linear equations of up to 2 variables. This logic accommodates both 2-SAT clauses and linear clauses of 3 variables, and seems to be able to emulate Gaussian elimination to some extent, but I am not yet completely sure how. Last week, I think I was able to generalize Krom's proof of refutable-completeness for 2-SAT logic (that has linear equations on 1 variable) to this logic, but I am in the process of double checking my result for gotchas like this.
There are other ideas how to control the linear terms, once you have the linear equations solved, it's easy to verify whether some variables are linearly dependent, because you have the basis, and modify the ordinary 2-SAT algorithm accordingly (2-SAT works by propagation via transitive dependency of literals, but if the 3 variables involved are linearly dependent, then you can derive lot more). These are mainly ideas how to make the polynomial algorithm even more efficient.
Comments
Well, this is somewhat heartbreaking for me. I haven't read the paper, but the result sounds very plausible to me.
I am also an amateur working on P=NP. Last week, I think I also proved that P=NP, but with a different method, and was about to seek publication.
My result seems very similar to his, yet very different. I can prove that class of SAT which is intersection of 2SAT and XORSAT is NP-complete by reduction to 3-SAT. Then I follow the approach in Melville's Krom 1967 paper on 2-SAT, and prove that certain polynomial-sized logic (that corresponds to the intersection) is refutable complete. So you can essentially generate all formulas in that logic and if you don't find contradiction, the instance is satisfiable.
I have also did some preliminary testing of my method, and was able to factor small integers with it. However, there was a bug.
So, to sum up, I am not surprised that P=NP with a constructive and efficient algorithm. Take it for what you want. The future is gonna be interesting (crypto DOOMSDAY).
I don't understand. You said that you thought you proved P=NP, but then it turned out you hadn't.
How does this help to support your belief that P=NP has been solved by someone else? Surely it wouldn't surprise you if it turns out they were as wrong as you were before?
PS: Also, reducing 2SAT to 3SAT doesn't help proving that P=NP. The opposite reduction would, if you were able to do the reduction in polynomial time. But maybe I misunderstood something about what you attempted.
I think I have a proof, it's just not yet published. Also, the original method I was attempting contained a bug, but I understand the theory better now.
So, I have some evidence, both experimental and theoretical, there is an efficient polynomial algorithm out there (and possibly many different methods).
Unfortunately, not 100% verified because despite what many smartypants are saying here, it's incredibly difficult to even have a conversation about a possibility of a relatively uncomplicated proof that P=NP. (I think Millenium prize is part of the problem, but that's another discussion).
And to clarify, I am reducing 3-SAT to 2XSAT, not 2-SAT. 2XSAT generalizes 2-SAT to arbitrary linear equations rather than literals (we can think of a literal as a linear equation on 1 variable).
I will happily send you (or anybody) the draft I have, so that you can critique it.
Nobody wants to read your draft about an algorithm that doesn't work. Your implementation is already giving you the critique that you need. If you get it to work and it's obviously polynomial time, you'll have something to talk about.
I don't think this is quite true. Most NP-hard problems are usually solvable in polynomial time, so your algorithm looking like it runs in polynomial time doesn't tell you much.
It really depends. If you have an unbounded loop that looks like it runs in polynomial time, you're in highly questionable territory. If you have a 5-deep nest of for-loops, that's what I call "obviously polynomial time" -- if such an algorithm solves every problem you throw at it, you have hope.
As <cat-over-keyboard> already mentioned, it's not always that simple. For example, my current approach (modeled after Krom, who doesn't even have a Wikipedia page - no wonder nobody reads him!) is a more systematic search for a polynomial algorithm - construct a polynomial sized-logic in which theories have models that are satisfying instances of SAT, and prove its refutable-completeness. This proves existence of a polynomial algorithm, because you can generate all formulas of theory (coming from SAT instance) in said logic, and if you don't find a contradiction, the instance is satisfiable. The algorithm is kinda implicit, non-deterministic, if you will (because you can generate all the formulas in any order or even generate just a subset).
Anyway, my main point is - people beware, practically solvable P=NP (even for hard instances) is a very real possibility.
Sure, but most complicated polynomial time algorithms don't work like this. You either have cases like AKS which are obviously polynomial but not obviously correct, or cases that are obviously correct but not obviously polynomial.
Algorithms which are obviously polynomial, and non-obviously correct are the only ones I'd entertain from a novice. It's not hard to mine for counterexamples, as long as the code runs.
I think this is exactly the unhelpful tactics that have prevented people figuring out the problem. I have both theoretically and practically verified the 2XSAT reduction, and I believe it's a step towards P=NP. But, it's being dismissed out of hand because I don't have a practical, fully polynomial, algorithm.
So I cannot publish that (I am well aware of the unfortunate situation that only a practical implementation will now convince people that P=NP).
Add to it, why should I? What if it's not that far from a full solution, and somebody else will get the prize?
I came to understand why Perelman refused the prize. Mathematics should be about collaborative understanding of the universe, not about people working in isolation until they have fully working superoprimized implementation that can crack Bitcoins.
NP is generally thought to be harder than factoring, so I'm not sure that your reduction is a "reduction" in the sense that you've restated factoring in a (potentially-)harder-than-native problem space. Proving that factoring is polynomial would be a huge result indeed, but if your strategy requires you to prove P=NP along the way, you're focused on the wrong problem and I wouldn't expect you to get much traction.
No, I am not reducing to factoring, I only tested some on it because it's a relatively easy way to get hard instances.
I am reducing to 2XSAT, which is a name for instances that are intersections of 2-SAT and XORSAT instances.
Both 2-SAT and XORSAT have polynomial algorithms, why is it hard to believe that their intersection has one too?
If your reduction can solve factoring, what are the factors of 22112825529529666435281085255026230927612089502470015394413748319128822941402001986512729726569746599085900330031400051170742204560859276357953757185954298838958709229238491006703034124620545784566413664540684214361293017694020846391065875914794251435144458199?
I already said, I don't have an efficient algorithm. Once I will have, in my estimation, at best, it will be O(n^3) (n is number of variables), which still means a lot - to factor 16-bit integer, my (linear) 2XSAT reduction requires about 4000 variables, so the number of variables for a cryptographically-strong problem will be in millions. You need to have a very efficient parallel algorithm to deal with that, and that's very low on the list of priorities - first I need to understand how to actually make the algorithm efficient (so far I think I proved there is a polynomial bound - around O(n^8) or so, but I know for sure it's very inefficient, because I am doing it very naively).
There are other ways to improve the method, which (if indeed P=NP) are incredibly interesting - you can directly compose presolved general instances and specialize on them. Kinda like if you need to compute many solutions to linear equations, you only need to factor the matrix once.
Why don't you try testing your algorithm on some 1000 variable or so SAT instances ? There are thousands of such problems that have been created for the SAT competitions. If your code can solve all of them and is really P-time then I think there are many people who would be interested in looking at your algorithm, myself included.
That's what I am generally doing and planning to do, however right now, the theory had priority (there is still couple weak spots in my proof which I need to patch up). But I will return to testing once I will have a better idea what I want the algorithm to do (as I mentioned, a more naive version of the method that combined solving 2-SAT and XORSAT failed with a bug, which I think I now understand).
I think testing O(n^8) algorithm is pointless, so it needs more polishing (naive algorithm for 2-SAT (that follows from Krom) is O(n^3) or so, but the best methods are linear; so I feel there is a lot of room for improvement, but obviously my method is a little bit more complicated than 2-SAT, which it generalizes).
There's one thing I'd like to get some clarification on. You said in an earlier comment:
It seems to me that 2-SAT and XORSAT are distinct problems. I mean there is no problem instance that is simultaneously a 2-SAT problem and an XORSAT problem instance. So how can there be instances that are intersections of both ?
The 2XSAT has clauses that are from 2-SAT or XORSAT. So it's a generalization of both. The solutions (boolean variable assignments) must satisfy both 2-SAT and XORSAT part of the problem, hence the solutions of the 2XSAT instance is their intersection.
There are in fact problems that are both 2-SAT and XORSAT, but they seem to be rather trivial - those are linear equations that have up to 2 variables per equation. But that's not what I am talking about.
I understand why people are confused with my off-hand comments, but I didn't plan to explain my approach here in detail, and I typed the first couple of comments when I was at work on my phone, where being precise is tedious.
The intersection of two sets is a subset of both sets. So that means you're reducing to 2SAT?
No, you misunderstand, the intersection is in the solution to the instance. The 2XSAT are problems that can contain both 2-SAT clauses (two literals per OR clause) and XORSAT clauses (linear equations). 2-SAT (as well as XORSAT) are just special cases of that. You can also think of it as 2-SAT, but confined into a linear subspace of Z_2^n.
That isn't the intersection of 2SAT and XORSAT, it's the union. Problems in the intersection would be solvable by either type of solver. I don't think it's "obvious" that your problem class should be polynomial; 2XSAT as you've described it (is it your own invention? I haven't found a reference) appears to be a strictly more powerful problem class.
It's not a union of those classes, it's a different class, and as you say, it's more powerful, because it can be projected (my reduction adds additional variables) into 3-SAT and SAT instance.
Yes, 2XSAT is the name I gave it, and I couldn't find it anywhere. The reduction is surprisingly simple, yet nobody mentions it. That's why I am warning people here - just based on this alone, I 80% believe that P=NP with a practical algorithm (which either way involves solving linear equations). And I wouldn't be surprised somebody coming up with the algorithm.
The reason why I say it's an intersection is because that's how the set of solutions of an instance looks like. That's what we need to figure out - how to characterize the sets of solutions described by SAT instance (i.e. sets of assignments to boolean variables that satisfy the instance).
However, it's not that easy, even if you characterize them as interesections of 2-SAT and XORSAT instances, set of solutions to 2-SAT is notoriously hard to characterize too, for example, #2SAT is not known. And polynomial algorithms for 2-SAT and XORSAT are doing very different things, and it's not at all obvious how to generalize them into a common algorithm that can do both.
As a mathematician, my advice to you is to build up some theory around this problem class. I find it entirely plausible that you can reduce 3sat to it. I'd encourage you to look for a reduction from 2XSAT to 3sat. Find some problems that are well-expressed in the language of 2XSAT. You might find something worthy of publication. From there you'll want to shop your results around at conferences. You may drum up some interest in your work, or even a collaborator. Just don't act confident that you've cracked a keystone problem in the field. You think you're on the right path, and that's exciting, but we've all been there and we've all met dozens of novices who were utterly convinced of their incorrect solution to this problem. It's a huge red flag that you're a waste of time.
As a grad student, I got perhaps hundreds of "dear professor" emails claiming proof of everything from squaring the circle to the BSD conjecture. Reflexively running from anybody making such claims is a necessary survival skill. Math is a field where the bullshit asymmetry principle[1] is particularly stark. Finding a flaw in a proof can take vastly more effort than is spent concocting it.
[1] https://en.m.wikipedia.org/wiki/Brandolini%27s_law
The opposite reduction from 2XSAT to SAT is obvious, it's just a special case.
I think professionals of every field have to deal with passionate amateurs of all levels. I understand why many people don't want to do it, but IMHO overemphasis on professionalism (culturally coming from enormous peer pressures) is hurting any field. The superprizes make it even worse.
I am not acting like that, but I also have to be honest that my goal is specific - to understand why we can or can't have a polynomial algorithm. I.e. I have a strategy already, what I need is a 2nd opinion about some specifics of it.
Honestly, I don't think you have the proof. Proving p is euqal to np will have very big consequences, not only in computer science but also in logics for example. I think this problem is far more complex than you think and it is not going to be solved by chance by an amateur. If it's going to be solved, there will be a deep math argument.
This is the entire question of P vs NP. I'd love to point you to a reference, but the question remains unresolved. Good hunting.
If you really think mathematics should be about collaboration and not competition, why do you worry about who gets the prize?
You should pick what's more important to you - if it's collaboration, why not publish the steps you've accomplished? If someone else uses it to achieve a full solution, you'll still have a claim to part of the credit towards the solution.
Because I am also a human. I think I could still use the money (if anything, very few people want to be principled idiots who refuse $1m), and if I spent several years determined to understand it, perhaps it's worth spending some more to understand it fully. As I explained, it creates an atmosphere that prevents collaboration - it's incredibly hard to find anyone to talk about the problem with. Anyway, I am writing about my approach here, and I am about to write about it more. Still, people dismiss it outright.
What's your take on survey propagation? I would think that any P=NP proof would take that into account or be similar.
I haven't really studied it in detail, but my motivation is similar, I see SAT as a simplified version of the marginal problem, and I want to solve marginal problem (or at least approximate) because I am interested in representing knowledge intensionally.
I played with propagation a lot in the past, but I don't think local propagation (that resolves conditions of a bounded number of variables at a time, until everything stabilizes) can ever work, because it would contradict Razborov result on monotone circuits. I don't remember the exact argument, but I think it would imply a polynomial monotone circuit capable of resolving the instance. Also, XORSAT is not really amenable to this either, to solve arbitrary XORSAT instance you have to add together arbitrary number of linear equations, so the number of variables per equation can balloon up.
That's why more recently I focused on understanding what exactly is the role of XORSAT, and by serendipity, I stumbled upon the above-mentioned reduction (which I think is a really exciting result). XORSAT is great for testing different algorithms, because despite the fact we have a nice polynomial algorithm (Gaussian elimination), one can easily create arbitrary (and loopy) instances where propagation is difficult.
The way I see it, to avoid the problems with the bound, you need to preprocess the linear equations "inherent" in the instance by adding extra variables. The exact way to add variables depends on the instance, but it can be done by solving the linear equations. Propagation algorithms that go into the process blindly, without understanding the underlying linear structure, will mysteriously fail.
However, my current approach through logic, basically building up theorems about the instance, until it is decided, can be considered a generalization of the propagation approaches. The messages are true statements about variables, which are propagated by deduction rules of the logic. But this is done only after we have discerned the linear structure in the problem, which is addressed globally, as described above.
That jives with my intuition. I had forgotten about the connection between Gaussian elimination and xor sat. That does sound like a good direction to reason from.
How do you prevent an exponential increase in linear terms though?
Good luck!
I am still not sure about the exact role of Gaussian elimination. I thought that it will be somehow necessary, but it seems that if you only break linear equations to 3 variables per equation (by adding extra variables), you can get away without it. Although it certainly doesn't hurt to do it, I think for efficient algorithms, it will be required (and so the whole endeavor will be at least O(n^3)).
To prevent exponential increase in linear terms, I work within a sort of limited logic that only allows formulas that are ORs of (implications between) two linear equations of up to 2 variables. This logic accommodates both 2-SAT clauses and linear clauses of 3 variables, and seems to be able to emulate Gaussian elimination to some extent, but I am not yet completely sure how. Last week, I think I was able to generalize Krom's proof of refutable-completeness for 2-SAT logic (that has linear equations on 1 variable) to this logic, but I am in the process of double checking my result for gotchas like this.
There are other ideas how to control the linear terms, once you have the linear equations solved, it's easy to verify whether some variables are linearly dependent, because you have the basis, and modify the ordinary 2-SAT algorithm accordingly (2-SAT works by propagation via transitive dependency of literals, but if the 3 variables involved are linearly dependent, then you can derive lot more). These are mainly ideas how to make the polynomial algorithm even more efficient.
And thanks for encouragement!