When does Gaussian elimination solve exact 1-in-3 SAT?


Terms:

A literal is a variable or its negation.

A clause is a set of literals.

An exact 3-in-1 clause is satisfied if an assignment of values to variables results in exactly 1 true literal and 2 false literals.

Exact 3-in-1 SAT is the problem, given a set of exact 3-in-1 clauses, is there as assignment of variables that satisfies all clauses?

Question:

This corresponds to a linear algebra problem, sort of:

Let true be 1 and false be -1.

For each variable v and its negation w, add the equations:

v + w = 0

(This is because 1 + (-1) = 0)

For each exact 3-in-1 clause (a b c), add the equations:

a + b + c = -1

(This is because two -1‘s and one 1 will add up to -1.)

It’s possible solving the equations results in a value other than 1 or -1. However if the solution to the system of equations is only 1 and -1, I suspect that’s a valid solution to the original exact 1-in-3 problem.

So, when does Gaussian elimination solve exact 1-in-3 SAT?

Here’s an example when it does:

These clauses:

(1 2 3) (2 3 -2) (2 3 -3)

Correspond to this matrix:

1, 0, 0, 1, 0, 0, 0 0, 1, 0, 0, 1, 0, 0 0, 0, 1, 0, 0, 1, 0 1, 1, 1, 0, 0, 0, -1 0, 1, 1, 0, 1, 0, -1 0, 1, 1, 0, 0, 1, -1 

Reduced row echelon:

1, 0, 0, 0, 0, 0, 1 0, 1, 0, 0, 0, 0, -1 0, 0, 1, 0, 0, 0, -1 0, 0, 0, 1, 0, 0, -1 0, 0, 0, 0, 1, 0, 1 0, 0, 0, 0, 0, 1, 1 

Therefore solution (via far-right column) is: (1 -2 -3)

Does this always work on larger matrices with 2*n rows and 2*n+1 columns where n is the number of variables? (I think it may need non-redundant (linearly independent?) rows.)