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


It works but since there are assignments other than -1 and 1, how will you use the row echelon form to make any conclusions about the 1-in-3 SAT instance? 

Two cases: 


Case 1: The 1-in-3SAT formula is unsatisfiable but the reduced row echelon matrix is satisfiable (because of the possible assignments other than -1/1) 
Case 2: Both are satisfiable but assigning a 1 and -1 may bring you back to Case 1 


Therefore you will have to try an exponential number of assignments in worst case. Assigning random -1 and 1 values will force you to assign undesirable values during the end of elimination and you will have to backtrack. 

If you find an algorithm to find "only the solutions with -1 and 1" or count such solutions or prove there are 0 then it is NP-complete and even co-NP complete.