Gauss-Jordan Elimination seems to be incomplete

[j-danner]

While playing with XOR clauses and trying to use your Gauss-Jordan propagation implementation for XOR clauses in my own solver, I came across many examples, where the GJE seems to be incomplete. That is: For a given set of XOR clauses and given enqueued assignments, not all possible propagations are derived from the clauses right away.

Consider for instance the following minimal example, where no propagations are enqueued, and we merely give an inconsistent system of linear equations:

p cnf 6 4
x 1 2 3 5 0
x -1 2 4 6 0
x -3 6 0
x -4 5 0

This corresponds to the system of linear equations
$x_1 + x_2 + x_3 + x_5 +1$
$x_1+x_2+x_4+x_6$
$x_3+x_6$
$x_4+x_5$,
and the sum of these polynomials is $1$, so there is no solution.

Now, (the latest) cryptominisat (with and without options --autodisablegauss=0 and --minmatrixrows=0) requires between 4 and 7 decisions to terminate; whereas I would expect it to require 0 decisions, as GJE should already produce the conflict right away.

For my use case, I would very much like the implementation to be complete. I have played around with the configurations in conf.gaussconf, however did not succeed in substantially improving it. (The issue seems to be related to how binary XOR clauses are not put into matrices, but represented by two binary clauses.)

So my question/issue is rather simple: Is it intended behaviour that GJE is (seemingly) incomplete, or am I just using wrong configurations?

(If necessary, I can also produce more complex examples with incomplete propagation.)

[msoos]

Hi,

Nice observation! If you set --preproc 1 I have a feeling that will be fixed. Binary XORs are indeed not put into the matrix. And so we end up with this behaviour. If you run SCC & equivalent literal replacement, and then recompute the matrix and do GJE, it'll be done. As it is, without the preprocessing turned on, it does that later, as an inprocessing step, and so it takes some time. Preprocessing is not enabled, because it takes some time, and startup time can be a serious problem in some cases -- some people run solver.solve() literally 100000 times in a row. If each time the preprocessor runs, it'd take 10000 seconds. Without the preprocessor running, it takes like 10. So different use-cases require different trade-offs.

I hope the above helped. Let me know if it did, then we can close this issue I hope! Cheers,

Mate