non linear constraints report incorrect results when conjuncts appear multiple times.
The following problem was reported for Sat4j 2.3.0.
In the file:
- #variable= 11 #constraint= 1 -1 x1 -2 x9 x4 -3 x10 x4 -4 x11 x4 +5 x8 x4 -6 x9 x4 -7 x10 x4 -8 x11 x4 +9 x8 x4 -10 x9 x4 -11 x10 x4 -12 x11 x4 +13 x8 x4 -14 x9 x4 -15 x10 x4 -16 x11 x4 +17 x8 x4 -18 x9 x4 -19 x10 x4 -20 x11 x4 +21 x8 x4 = 9;
the solver answers unsat, while there is a solution. x1 x4 x8 -x9 x10 -x11 for instance.
The problem comes from the constraint being build with conjuncts that appear several times.
Merging the conjuncts solves the problem:
- #variable= 11 #constraint= 1 -1 x1 -50 x9 x4 -55 x10 x4 -60 x11 x4 +65 x8 x4 = 9;
In competition settings, this case is not going to appear. However, it can happen when Sat4j is used in an application.
Thus we need to sort it out.