[OT] On certificates of unsatisfiablity of linear equations over {0,1,-1}

[Georgi Guninski]

From our preprint [1] and mathoverflow question [2]:

When we encode 3SAT to this form we try to solve $M X=0$ where $M$
is the constraint matrix and $X$ is {0,1,-1} vector with last entry $1$
(for the constant coefficient of the inhomogeneous system).

For positive integer $w$, we add one more constraint $\sum x_i=w$

To solve the system compute $ke$ to be the basis of the LLL reduced
right kernel of $M$

In sage this is done with the commands `ke=M.right\_kernel(basis="LLL").basis()`
or `ke=M.right\_kernel\_matrix().LLL()`

$ke$ is a list of vectors $ke[i]$ of size $n+1$ and all solutions $Y$
of $ M Y=0$ are linear combinations of $ke[i]$.

Let $g=\gcd\{ke[j][n] : 0 \le j <|ke|\})$.
If $g \ne 1$ (usually $g$ is zero). then no linear combination can be
$1$ so return `No solution`.

For all but one $w$, we get `No solution`


>Q1 Has this unsatisfiability criteria been studied?

>Q2 What intuition explains that adding a single weight constraint
gives only one possibility for satisfiability in the reduction from 3SAT?



[1] On solving linear equations over {0, 1,
−1}](https://www.researchgate.net/publication/405231825_On_solving_linear_equations_over_0_1_-1#fullTextFileContent
[2] https://mathoverflow.net/q/511656/12481