XCSP3 parser: problems found by the unit tests of PyCSP3 (pow, mod, allDifferent-matrix with except, iff, nValues on expressions, ordered with lengths, lex-matrix with ge or gt, sum with notin) #1248

This issue gathers the problems found by the unit tests of PyCSP3 with the XCSP3 parser of Choco (choco-parsers-4.10.15-beta.jar, the version embedded in PyCSP3). The command is java -cp choco-parsers-4.10.15-beta.jar org.chocosolver.parser.xcsp.ChocoXCSP model.xml -a -f -flt.

1. pow is unsupported in some intensional constraints

<instance format="XCSP3" type="CSP">
  <variables>
    <var id="x"> -3..3 </var>
    <var id="y"> -30..30 </var>
  </variables>
  <constraints>
    <intension> eq(pow(x,3),y) </intension>
  </constraints>
</instance>

Observed:

java.lang.NullPointerException: Cannot invoke "org.chocosolver.solver.expression.discrete.arithmetic.ArExpression.eq(...)"
Exception in thread "main" java.lang.RuntimeException: UNSUPPORTED
s UNKNOWN

The same happens for eq(y,pow(x,2)) (with y in -3..9) and for eq(pow(x,z),y) (with z in 0..2), whereas eq(pow(x,2),add(y,3)) is solved.

Results of the other solvers:

with (ACE 2.6 and CHOCO (choco-parsers-4.10.15-beta), embedded in PyCSP3, and cosoco 2.6.1, from pip: the versions used by PyCSP3):

• ACE: java -jar ACE-2.6.jar model.xml -s=all -xe -xc=false
• CHOCO: java -cp choco-parsers-4.10.15-beta.jar org.chocosolver.parser.xcsp.ChocoXCSP model.xml -a -f -flt
• cosoco: cosoco model.xml -model=2 -nbsols=0

Tests of PyCSP3: test_arithmetic_operators[CHOCO-x ** 3 == y], test_arithmetic_operators_with_small_domains[CHOCO-x ** z == y], test_expr[CHOCO-expr("eq", y, expr("pow", x, 2))] in pycsp3/tests/test_constraints_intension.py.

2. mod loses the solutions where the dividend is negative and not a multiple of the divisor

<instance format="XCSP3" type="CSP">
  <variables>
    <var id="x"> -3..3 </var>
    <var id="y"> -3..3 </var>
  </variables>
  <constraints>
    <intension> eq(mod(x,3),y) </intension>
  </constraints>
</instance>

Observed: 5 solutions: (-3, 0), (0, 0), (1, 1), (2, 2), (3, 0).

Expected: according to Remark 7 of XCSP3-Core ("rounding towards 0", as in C or Java), 7 solutions: the ones above, and (-2, -2) and (-1, -1). No solution is found for x = -2 and x = -1 (with the rule "rounding towards negative infinity", (-2, 1) and (-1, 2) would be expected). Similarly, eq(y,mod(x,2)) has no solution for x = -3 and x = -1, whereas eq(div(x,2),y) is solved as expected.

Results of the other solvers:

with (ACE 2.6 and CHOCO (choco-parsers-4.10.15-beta), embedded in PyCSP3, and cosoco 2.6.1, from pip: the versions used by PyCSP3):

• ACE: java -jar ACE-2.6.jar model.xml -s=all -xe -xc=false
• CHOCO: java -cp choco-parsers-4.10.15-beta.jar org.chocosolver.parser.xcsp.ChocoXCSP model.xml -a -f -flt
• cosoco: cosoco model.xml -model=2 -nbsols=0

cosoco finds the expected solutions; ACE fails on these instances (reported in xcsp3team/ACE#12).

Tests of PyCSP3: test_arithmetic_operators[CHOCO-x % 3 == y], test_expr[CHOCO-expr("eq", y, expr("mod", x, 2))] in pycsp3/tests/test_constraints_intension.py.

3. allDifferent-matrix with except: solutions are lost

<instance format="XCSP3" type="CSP">
  <variables>
    <array id="x" size="[3][3]"> 0..2 </array>
  </variables>
  <constraints>
    <allDifferent>
      <matrix> x[][] </matrix>
      <except> 0 </except>
    </allDifferent>
  </constraints>
</instance>

Observed: some of the expected solutions are not found (see the table below).

Expected: the assignments where the values different from 0, on each row and on each column, are all different.

Results of the three solvers:

with java -jar ACE-2.6.jar model.xml -s=all -xe -xc=false, java -cp choco-parsers-4.10.15-beta.jar org.chocosolver.parser.xcsp.ChocoXCSP model.xml -a -f -flt and cosoco model.xml -model=2 -nbsols=0 (ACE 2.6 and CHOCO, embedded in PyCSP3, and cosoco 2.6.1, from pip).

ACE finds all the expected solutions; cosoco also loses solutions (reported in xcsp3team/cosoco#78).

Tests of PyCSP3: test_alldifferent_matrix[CHOCO-excepting 0], test_alldifferent_matrix[CHOCO-excepting 0 and 2] in pycsp3/tests/test_constraints_global_alldifferent.py.

4. iff with more than two arguments is evaluated with associativity

<instance format="XCSP3" type="CSP">
  <variables>
    <var id="x"> -3..3 </var>
    <var id="y"> -3..3 </var>
    <var id="b"> 0 1 </var>
  </variables>
  <constraints>
    <intension> iff(gt(x,0),gt(y,0),b) </intension>
  </constraints>
</instance>

Observed: 49 solutions, whose combinations of (x > 0, y > 0, b) are (F, F, 1), (F, T, 0), (T, F, 0) and (T, T, 1): the predicate is evaluated as gt(x,0) ⇔ (gt(y,0) ⇔ b).

Expected: according to Table 4.1 of XCSP3-Core (x1 ⇔ ... ⇔ xr), all the arguments are equivalent, as for eq(x1,...,xr): 25 solutions, where x > 0, y > 0 and b are all true or all false, that is to say the combinations (F, F, 0) and (T, T, 1).

Results of the three solvers:

with java -jar ACE-2.6.jar model.xml -s=all -xe -xc=false, java -cp choco-parsers-4.10.15-beta.jar org.chocosolver.parser.xcsp.ChocoXCSP model.xml -a -f -flt and cosoco model.xml -model=2 -nbsols=0 (ACE 2.6 and CHOCO, embedded in PyCSP3, and cosoco 2.6.1, from pip).

ACE finds all the expected solutions; cosoco ignores the arguments after the second one (reported in xcsp3team/cosoco#74).

Tests of PyCSP3: test_xor_iff_imply[CHOCO-iff(x > 0, y > 0, b)] in pycsp3/tests/test_constraints_intension.py.

5. nValues on expressions: some solutions are found several times

<instance format="XCSP3" type="CSP">
  <variables>
    <array id="x" size="[3]"> 0..2 </array>
  </variables>
  <constraints>
    <nValues>
      <list> add(x[0],1) add(x[1],1) add(x[2],1) </list>
      <condition> (gt,1) </condition>
    </nValues>
  </constraints>
</instance>

Observed: d FOUND SOLUTIONS 30: all the expected solutions are found, but the 6 solutions where the three values are all different (such as 0 1 2) are each found twice.

Expected: the 24 assignments where x[0] + 1, x[1] + 1 and x[2] + 1 are not all equal, each one found once.

Solutions are also found several times with the condition (le,2), and when variables and expressions are mixed in the list, but not with the condition (eq,2), nor with two expressions, nor with variables only.

Results of the three solvers:

with java -jar ACE-2.6.jar model.xml -s=all -xe -xc=false, java -cp choco-parsers-4.10.15-beta.jar org.chocosolver.parser.xcsp.ChocoXCSP model.xml -a -f -flt and cosoco model.xml -model=2 -nbsols=0 (ACE 2.6 and CHOCO, embedded in PyCSP3, and cosoco 2.6.1, from pip). The solutions are counted without the last one, displayed again by CHOCO after s SATISFIABLE.

ACE finds all the expected solutions, each one once; cosoco does not handle nValues on expressions (s UNSUPPORTED).

Tests of PyCSP3: test_notallequal_on_expressions with CHOCO, for the 6 constraints on at least three integer expressions (such as NotAllEqual(x[0] + 1, x[1] + 1, x[2] + 1)), in pycsp3/tests/test_constraints_global_notallequal.py (xcsp3team/pycsp3#130).

6. ordered with lengths: solutions are lost

<instance format="XCSP3" type="CSP">
  <variables>
    <array id="x" size="[3]"> 0..2 </array>
  </variables>
  <constraints>
    <ordered>
      <list> x[] </list>
      <lengths> -1 -1 </lengths>
      <operator> ge </operator>
    </ordered>
  </constraints>
</instance>

Observed: s UNSATISFIABLE.

Expected: according to XCSP3-core (Semantics 9), ordered(X, L, ⊙) holds iff x[i] + l[i] ⊙ x[i+1] for each i: here, the 21 assignments such that x[0] + 1 >= x[1] and x[1] + 1 >= x[2].

Cause: XCSPParser.buildCtrOrdered() (with lengths given by integers or by variables) orders the whole sequence x[0], x[0] + l[0], x[1], x[1] + l[1], ..., x[n-1] with the operator, which adds the constraints x[i] ⊙ x[i] + l[i], not part of the semantics: they are false when l[i] > 0 with ge or gt, when l[i] < 0 with le or lt, and when l[i] = 0 with lt or gt.

Results of the three solvers (x of size 3 with domains 0..2, and y of size 2 with domains 0..1):

with java -jar ACE-2.6.jar model.xml -s=all -xe -xc=false, java -cp choco-parsers-4.10.15-beta.jar org.chocosolver.parser.xcsp.ChocoXCSP model.xml -a -f -flt and cosoco model.xml -model=2 -nbsols=0 (ACE 2.6 and CHOCO, embedded in PyCSP3, and cosoco 2.6.1, from pip).

Tests of PyCSP3: test_ordered_with_lengths and test_ordered_with_lengths_given_by_variables with CHOCO, for the lengths and the orderings on which the decomposition of CHOCO differs from the semantics (21 tests), in pycsp3/tests/test_constraints_global_increasing_decreasing.py (xcsp3team/pycsp3#135).

7. lex-matrix with ge or gt: wrong solutions

<instance format="XCSP3" type="CSP">
  <variables>
    <array id="x" size="[2][2]"> 0 1 </array>
  </variables>
  <constraints>
    <lex>
      <matrix> x[][] </matrix>
      <operator> ge </operator>
    </lex>
  </constraints>
</instance>

Observed: 4 of the 7 expected solutions, and 3 wrong solutions.

Expected: according to XCSP3-core (Semantics 35), the rows of the matrix are lexicographically ordered with >=, and so are its columns: the 7 assignments such that (x[0][0], x[0][1]) >=lex (x[1][0], x[1][1]) and (x[0][0], x[1][0]) >=lex (x[0][1], x[1][1]).

Cause: for GE and GT, XCSPParser.buildCtrLexMatrix() reverses the order of the rows (rmatrix), which is right for the rows, but then orders the columns of rmatrix, that is to say the columns read from bottom to top, instead of the reversed sequence of the columns of the matrix (ArrayUtils.reverse(ArrayUtils.transpose(matrix)), for instance). With LE and LT, the solutions are correct.

Results of the three solvers (x of the given size, with domains 0..1):

with java -jar ACE-2.6.jar model.xml -s=all -xe -xc=false, java -cp choco-parsers-4.10.15-beta.jar org.chocosolver.parser.xcsp.ChocoXCSP model.xml -a -f -flt and cosoco model.xml -model=2 -nbsols=0 (ACE 2.6 and CHOCO, embedded in PyCSP3, and cosoco 2.6.1, from pip).

Tests of PyCSP3: test_lex_matrix, test_lex_matrix_given_by_rows, test_lex_matrix_given_by_explicit_rows and test_lexdecreasing_example_with_matrix with CHOCO, for LexDecreasing() (with and without strict=True), in pycsp3/tests/test_constraints_global_lexincreasing_lexdecreasing.py (xcsp3team/pycsp3#141).

8. sum with notin: wrong solutions, found several times

<instance format="XCSP3" type="CSP">
  <variables>
    <array id="x" size="[4]"> 0..2 </array>
  </variables>
  <constraints>
    <sum>
      <list> x[] </list>
      <condition> (notin,2..4) </condition>
    </sum>
  </constraints>
</instance>

Observed: the 81 assignments (the 36 expected solutions, and 45 wrong ones, whose sum is in 2..4), displayed 198 times in all.

Expected: the 36 assignments whose sum is not in 2..4, each one once.

Cause: for NOTIN, XCSPParser.buildSum() creates a new variable resu whose domain is the set (or the interval) of the condition, and posts resu != sum (XCSPParser.java, lines 943-966): this says that some value of the set is different from the sum, instead of the sum being different from all the values of the set; besides, each value of resu gives the same solution again. With IN, the solutions are correct.

Results of the three solvers (x of size 4, with domains 0..2):

with java -jar ACE-2.6.jar model.xml -s=all -xe -xc=false, java -cp choco-parsers-4.10.15-beta.jar org.chocosolver.parser.xcsp.ChocoXCSP model.xml -a -f -flt and cosoco model.xml -model=2 -nbsols=0 (ACE 2.6 and CHOCO, embedded in PyCSP3, and cosoco 2.6.1, from pip).

Tests of PyCSP3: test_sum_conditions (not in range(2, 5), not in {1, 3, 5}, not in [1, 3, 5]), test_sum_with_the_parameter_condition (('notin', {1, 3})), test_sum_with_mini (not in range(2, 5), not in {1, 3}) and test_sum_with_an_empty_or_unreachable_condition (not in range(0, 9)) with CHOCO, in pycsp3/tests/test_constraints_global_sum.py (xcsp3team/pycsp3#156).

9. count with in or notin an interval: wrong solutions

<instance format="XCSP3" type="CSP">
  <variables>
    <var id="x0"> 0..2 </var>
    <var id="x1"> 0..2 </var>
    <var id="x2"> 0..2 </var>
  </variables>
  <constraints>
    <count>
      <list> x0 x1 x2 </list>
      <values> 1 </values>
      <condition> (in,1..2) </condition>
    </count>
  </constraints>
</instance>

Observed: the 27 assignments (the condition is ignored); with (notin,1..2), no solution.

Expected: the 18 assignments where 1 or 2 variables are 1 (and, with (notin,1..2), the 9 others).

Cause: XCSPParser.dealWithConditionIntvl(), used by condToVar() for count (and also for nValues) (XCSPParser.java, lines 1834-1845): for IN, the variable is created with model.intVar(Math.min(mi, min), Math.max(ma, max)), that is to say the union of the interval and of min..max (here 0..3), instead of their intersection; for NOTIN, model.notMember(r, min, max) is posted with the bounds min..max instead of the bounds mi..ma of the interval. With a set, the solutions are correct.

Results of the three solvers

with (ACE 2.6 and CHOCO (choco-parsers-4.10.15-beta), embedded in PyCSP3, and cosoco 2.6.1, from pip: the versions used by PyCSP3):

• ACE: java -jar ACE-2.6.jar model.xml -s=all -xe -xc=false
• CHOCO: java -cp choco-parsers-4.10.15-beta.jar org.chocosolver.parser.xcsp.ChocoXCSP model.xml -a -f -flt
• cosoco: cosoco model.xml -model=2 -nbsols=0

Tests

Tests of PyCSP3: test_count_conditions (in range(1, 3), not in range(1, 3)) and test_count_with_an_empty_or_unreachable_condition (in range(5, 9)) with CHOCO, in test_constraints_global_count.py (xcsp3team/pycsp3#169), whose model is, for instance,

x = VarArray(size=3, dom=range(3))

satisfy(
    Count(x, value=1) in range(1, 3)
)

10. element (member) with reifiedBy: the reification is ignored

<instance format="XCSP3" type="CSP">
  <variables>
    <var id="x0"> 0..2 </var>
    <var id="x1"> 0..2 </var>
    <var id="x2"> 0..2 </var>
    <var id="r"> 0 1 </var>
  </variables>
  <constraints>
    <element reifiedBy="r">
      <list> x0 x1 x2 </list>
      <value> 1 </value>
    </element>
  </constraints>
</instance>

Observed: the 38 assignments where a variable of the list is 1, with r = 0 as well as r = 1 (16 of them displayed twice), and none of the 8 assignments where no variable is 1 and r = 0: the attribute reifiedBy (full XCSP3, reification) seems to be ignored, the constraint element (member) being posted alone.

Expected: the 27 assignments where r = 1 iff a variable of the list is 1 (ACE is right), or else an explicit message saying that the case is not handled (as cosoco: s UNSUPPORTED).

Cause: the parser of CHOCO (XCSPParser) has no method buildCtrElement(..., XVarInteger reifiedBy); in the current version of XCSP3-Java-Tools, the default methods of XCallbacks2 would call unimplementedCase().

Results of the three solvers

with (ACE 2.6 and CHOCO (choco-parsers-4.10.15-beta), embedded in PyCSP3, and cosoco 2.6.1, from pip: the versions used by PyCSP3):

• ACE: java -jar ACE-2.6.jar model.xml -s=all -xe -xc=false
• CHOCO: java -cp choco-parsers-4.10.15-beta.jar org.chocosolver.parser.xcsp.ChocoXCSP model.xml -a -f -flt
• cosoco: cosoco model.xml -model=2 -nbsols=0

Tests

Tests of PyCSP3: test_exist_reified, test_exist_reified_on_integer_variables, test_exist_reified_by_a_negation, test_exist_by_element and test_exist_example_with_reified_by with CHOCO (14 tests), in test_constraints_global_count_shortcuts.py (xcsp3team/pycsp3#169), whose model is, for instance,

x = VarArray(size=3, dom=range(3))
r = Var(dom={0, 1})

satisfy(
    Exist(x, value=1, reified_by=r)
)

11. sum and count of expressions in(x,set(...)): wrong solutions

<instance format="XCSP3" type="CSP">
  <variables>
    <var id="x0"> 0..2 </var>
    <var id="x1"> 0..2 </var>
  </variables>
  <constraints>
    <sum>
      <list> in(x0,set(1,2)) in(x1,set(1,2)) </list>
      <condition> (le,1) </condition>
    </sum>
  </constraints>
</instance>

Observed: the 5 expected solutions, and wrong ones (some of them found twice): for example (2, 1), where the two expressions in(...)
are 1 (the sum is 2); with the coefficients 2 1, (1, 0) (the sum is 2); with in(x0,set(1,2)) x1 and (le,0), (2, 0). The value of
in(x0,set(1,2)) does not seem to be related to the value of x0.

Expected: the 5 assignments where at most one variable is 1 or 2.

Cause: not identified. The problem occurs when the expression in(x,set(...)) is converted into a variable, as for the lists of sum and count
(XCSPParser.vars(XNode[])); the same expression inside an intension is right, and so are notin and the equivalent disjunction or(eq(x0,1),eq(x0,2)).

Results of the three solvers

with (ACE 2.6 and CHOCO (choco-parsers-4.10.15-beta), embedded in PyCSP3, and cosoco 2.6.1, from pip: the versions used by PyCSP3):

• ACE: java -jar ACE-2.6.jar model.xml -s=all -xe -xc=false
• CHOCO: java -cp choco-parsers-4.10.15-beta.jar org.chocosolver.parser.xcsp.ChocoXCSP model.xml -a -f -flt
• cosoco: cosoco model.xml -model=2 -nbsols=0

Tests

Tests of PyCSP3: test_count_with_a_repeated_variable (Count(x[0], x[0], x[1], values=[1, 2]) <= 1, posted by PyCSP3 as a sum of
expressions in(...) with coefficients) with CHOCO, in test_constraints_global_count.py (xcsp3team/pycsp3#169), whose model is, for instance,

x = VarArray(size=2, dom=range(3))

satisfy(
    Count(x[0], x[0], x[1], values=[1, 2]) <= 1
)

This issue was found by the unit tests of PyCSP3: xcsp3team/pycsp3#66 (sections 1 to 4), xcsp3team/pycsp3#130 (section 5), xcsp3team/pycsp3#135 (section 6), xcsp3team/pycsp3#141 (section 7), xcsp3team/pycsp3#156 (section 8) and xcsp3team/pycsp3#169 (sections 9, 10 and 11)