[js8]

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.

[tgflynn]

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.

[js8]

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).

[tgflynn]

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 ?

[js8]

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.