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