Soundness bug in QF_LIA

[numairmansur]

Hi,
Z3 returns wrong answer on the following files.
1.smt2
2.smt2.zip
3.smt2.zip
4.smt2.zip
5.smt2.zip
6.smt2.zip
7.smt2.zip
8.smt2.zip
9.smt2.zip
10.smt2.zip

Every formula at each level in the assertion stack is satisfiable. But z3 would return unsat at some level. For example for file 1.smt2, i get:

sat
sat
sat
sat
sat
sat
unsat
sat
sat
sat
sat

CVC4 gives me:

sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat

OS:
NAME="Ubuntu"
VERSION="16.04.5 LTS (Xenial Xerus)"

$ git log -1
commit 321bad2
Author: Christoph M. Wintersteiger cwinter@microsoft.com
Date: Mon Jan 20 17:06:35 2020 +0000
Fix for implicit consts in FPA models. Fixes #2865.

[NikolajBjorner]

Are these the smallest repros possible?

[numairmansur]

I am sorry they actually aren't. I can run the minimiser and edit the PR with smaller files.

[numairmansur]

Here are some relatively small examples:

small1.smt2
small2.smt2
small3.smt2
small4.smt2

[NikolajBjorner]

@levnach The master branch creates a lia conflict with empty explanation. This seems to have been fixed in the levnach branch, or at least I don't easily repro.

[NikolajBjorner]

in the gomory cut code, the case where a non-basic variable has integer assignment there is no tracking of the explanations on the bounds of that variable. Seems it is necessary to add explanations, as sketched below.

 if (p.coeff().is_int()) {
                    // m_fj will be zero and no monomial will be added
                    if (at_lower(j)) {
                        m_ex.push_justification(column_lower_bound_constraint(j));            
                    }
                    if (at_upper(j)) {
                        m_ex.push_justification(column_upper_bound_constraint(j));
                    }
                    continue;
                }

[levnach]

Integrated to levnach fork.

[NikolajBjorner]

not really, it is #if 0'ed out at the moment. Can you check if just one bound is required and otherwise check correctness?

[levnach]

The Gomory cut is based on a precondition, as https://lara.epfl.ch/w/_media/projects:simplexdplltreport.pdf points out, that each non-basic variable is not free and has a value at its lower or upper bound. Therefore, at least one of the bound constraints needs to be provided; and the new code does it.
I also ran a performance test on QF_LIA: it did quite well.

[NikolajBjorner]

I am not sure about this being the real issue. The legacy solver also skips this case and integral columns shouldn't contribute to non-integrality of the base variables.

Running on small1.smt2 it looks like the offending row does not have the property that the basic variable is the sum of non-basic variables. This is an assumption for applying the cut.
What is a quick way to check this pre-condition (check that the row evaluates to 0).

[levnach]

lar_solver::row_is_correct(unsigned i), where i is the index of the row.

[NikolajBjorner]

Right, the rows are not correct and this is why gomory provides the wrong result. It assumes the rows are correct. I pushed a filter on incorrect rows, but a root cause understanding of whether this is legal would be useful.

[NikolajBjorner]

ad965ac

[levnach]

The row becomes incorrect during the "find_cube()" column shifting. Currently there is no indication in lar_solver that this has happened. I should track it and restore the tableau in this case.

[NikolajBjorner]

we should be good now.