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