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