[BUG] Clause learning issues since 4.10.11

[Holt59]

The code below does not work since Choco 4.10.11 when clause learning are enabled.

The code contains two methods to define equivalent set of constraints in the functions tables and ifThen - In practice, I'm using both at it seems to improve propagation.

With Choco 4.10.10, I can run the model without any issue, using tables, ifThen or both, with and without clause learning.

With Choco 4.10.11, the model cannot be run with either set of constraints (or with both) when signed clause learning is enabled:

• with tables, I get

  Learn a weak clause (1/3)

• with ifThen, I get

  Weak explanation found. Try to backjump to :d_13: A2\0 [A1 = 1, A1 = 1, A2 = 1, E1 = 0, B_S-then-_V_3_E-C = 1]

• with both, I get

  Weak explanation found. Try to backjump to :d_13: B_S-then-1_V_2_E-B\0 [E10 = 9, A6 = 2, B_S-then-1_V_2_E-B = 1, E2 = 2]

NB: There are unused variables because I was trying to mimic a real model (this is an anonymized version), and I was comparing the .toString() outputs. These variables do not seem to have any effect on the bug but I kept them just in case.

---

package com.chocobug;

import java.io.IOException;
import java.io.PrintStream;
import java.lang.reflect.Field;
import java.nio.file.Files;
import java.nio.file.Paths;
import java.util.Arrays;
import java.util.List;
import java.util.stream.IntStream;
import java.util.stream.Stream;
import org.chocosolver.solver.Model;
import org.chocosolver.solver.Solution;
import org.chocosolver.solver.constraints.Constraint;
import org.chocosolver.solver.constraints.extension.Tuples;
import org.chocosolver.solver.constraints.extension.nary.PropCompactTable;
import org.chocosolver.solver.exception.ContradictionException;
import org.chocosolver.solver.variables.BoolVar;
import org.chocosolver.solver.variables.IntVar;
import org.chocosolver.solver.variables.Variable;

public class App {

    protected final static String[] MS =
            IntStream.range(0, 10).mapToObj(i -> "M" + (i + 1)).toArray(String[]::new);
    protected final static String[] AS =
            IntStream.range(0, 12).mapToObj(i -> "A" + (i + 1)).toArray(String[]::new);
    protected final static String[] ES =
            IntStream.range(0, 10).mapToObj(i -> "E" + (i + 1)).toArray(String[]::new);
    protected final static String[] SS =
            IntStream.range(0, 11).mapToObj(i -> "A" + (i + 1)).toArray(String[]::new);

    protected final static String RA_Name = "RA";
    protected final static String RI_Name = "RI";

    protected final static String CNU_Name = "CNU";
    protected final static String ANU_Name = "ANU";
    protected final static String LNU_Name = "LNU";

    protected final static String THEN_VAR_FMT = "B_S-then-%s_V_%s_E-%s";

    protected final static String[] PPS = new String[] { "A", "B", "C", "D" };

    public static void tables(final Model m, final IntVar[] S, final IntVar[][] P) {
        final int[][][] values = new int[][][] {
                { { 1, 1, 0, 0, 1 }, { 1, 1, 1, 1, 1 }, { 1, 1, 2, 2, 1 },
                        { 1, 1, 3, 3, 1 }, { 1, 1, 4, 4, 1 }, { 1, 1, 5, 5, 1 },
                        { 1, 1, 6, 6, 1 }, { 1, 1, 7, 7, 1 }, { 1, 1, 8, 8, 1 },
                        { 1, 1, 9, 9, 1 }, { 1, 1, 10, 10, 1 }, { 2, 1, 0, 1, 0 },
                        { 2, 1, 1, 1, 1 }, { 2, 1, 2, 1, 2 }, { 2, 1, 3, 1, 3 },
                        { 2, 1, 4, 1, 4 }, { 2, 1, 5, 1, 5 }, { 2, 1, 6, 1, 6 },
                        { 2, 1, 7, 1, 7 }, { 2, 1, 8, 1, 8 }, { 2, 1, 9, 1, 9 },
                        { 2, 1, 10, 1, 10 }, { 3, 1, 1, 0, 0 }, { 3, 1, 1, 1, 1 },
                        { 3, 1, 1, 2, 2 }, { 3, 1, 1, 3, 3 }, { 3, 1, 1, 4, 4 },
                        { 3, 1, 1, 5, 5 }, { 3, 1, 1, 6, 6 }, { 3, 1, 1, 7, 7 },
                        { 3, 1, 1, 8, 8 }, { 3, 1, 1, 9, 9 }, { 3, 1, 1, 10, 10 } },
                { { 1, 2, 0, 0, 2 }, { 1, 2, 1, 1, 2 }, { 1, 2, 2, 2, 2 },
                        { 1, 2, 3, 3, 2 }, { 1, 2, 4, 4, 2 }, { 1, 2, 5, 5, 2 },
                        { 1, 2, 6, 6, 2 }, { 1, 2, 7, 7, 2 }, { 1, 2, 8, 8, 2 },
                        { 1, 2, 9, 9, 2 }, { 1, 2, 10, 10, 2 }, { 2, 2, 0, 2, 0 },
                        { 2, 2, 1, 2, 1 }, { 2, 2, 2, 2, 2 }, { 2, 2, 3, 2, 3 },
                        { 2, 2, 4, 2, 4 }, { 2, 2, 5, 2, 5 }, { 2, 2, 6, 2, 6 },
                        { 2, 2, 7, 2, 7 }, { 2, 2, 8, 2, 8 }, { 2, 2, 9, 2, 9 },
                        { 2, 2, 10, 2, 10 }, { 3, 2, 2, 0, 0 }, { 3, 2, 2, 1, 1 },
                        { 3, 2, 2, 2, 2 }, { 3, 2, 2, 3, 3 }, { 3, 2, 2, 4, 4 },
                        { 3, 2, 2, 5, 5 }, { 3, 2, 2, 6, 6 }, { 3, 2, 2, 7, 7 },
                        { 3, 2, 2, 8, 8 }, { 3, 2, 2, 9, 9 }, { 3, 2, 2, 10, 10 } },
                { { 1, 3, 0, 0, 3 }, { 1, 3, 1, 1, 3 }, { 1, 3, 2, 2, 3 },
                        { 1, 3, 3, 3, 3 }, { 1, 3, 4, 4, 3 }, { 1, 3, 5, 5, 3 },
                        { 1, 3, 6, 6, 3 }, { 1, 3, 7, 7, 3 }, { 1, 3, 8, 8, 3 },
                        { 1, 3, 9, 9, 3 }, { 1, 3, 10, 10, 3 }, { 2, 3, 0, 3, 0 },
                        { 2, 3, 1, 3, 1 }, { 2, 3, 2, 3, 2 }, { 2, 3, 3, 3, 3 },
                        { 2, 3, 4, 3, 4 }, { 2, 3, 5, 3, 5 }, { 2, 3, 6, 3, 6 },
                        { 2, 3, 7, 3, 7 }, { 2, 3, 8, 3, 8 }, { 2, 3, 9, 3, 9 },
                        { 2, 3, 10, 3, 10 }, { 3, 3, 3, 0, 0 }, { 3, 3, 3, 1, 1 },
                        { 3, 3, 3, 2, 2 }, { 3, 3, 3, 3, 3 }, { 3, 3, 3, 4, 4 },
                        { 3, 3, 3, 5, 5 }, { 3, 3, 3, 6, 6 }, { 3, 3, 3, 7, 7 },
                        { 3, 3, 3, 8, 8 }, { 3, 3, 3, 9, 9 }, { 3, 3, 3, 10, 10 } },
                { { 1, 4, 0, 0, 4 }, { 1, 4, 1, 1, 4 }, { 1, 4, 2, 2, 4 },
                        { 1, 4, 3, 3, 4 }, { 1, 4, 4, 4, 4 }, { 1, 4, 5, 5, 4 },
                        { 1, 4, 6, 6, 4 }, { 1, 4, 7, 7, 4 }, { 1, 4, 8, 8, 4 },
                        { 1, 4, 9, 9, 4 }, { 1, 4, 10, 10, 4 }, { 2, 4, 0, 4, 0 },
                        { 2, 4, 1, 4, 1 }, { 2, 4, 2, 4, 2 }, { 2, 4, 3, 4, 3 },
                        { 2, 4, 4, 4, 4 }, { 2, 4, 5, 4, 5 }, { 2, 4, 6, 4, 6 },
                        { 2, 4, 7, 4, 7 }, { 2, 4, 8, 4, 8 }, { 2, 4, 9, 4, 9 },
                        { 2, 4, 10, 4, 10 }, { 3, 4, 4, 0, 0 }, { 3, 4, 4, 1, 1 },
                        { 3, 4, 4, 2, 2 }, { 3, 4, 4, 3, 3 }, { 3, 4, 4, 4, 4 },
                        { 3, 4, 4, 5, 5 }, { 3, 4, 4, 6, 6 }, { 3, 4, 4, 7, 7 },
                        { 3, 4, 4, 8, 8 }, { 3, 4, 4, 9, 9 }, { 3, 4, 4, 10, 10 } },
                { { 1, 5, 0, 0, 5 }, { 1, 5, 1, 1, 5 }, { 1, 5, 2, 2, 5 },
                        { 1, 5, 3, 3, 5 }, { 1, 5, 4, 4, 5 }, { 1, 5, 5, 5, 5 },
                        { 1, 5, 6, 6, 5 }, { 1, 5, 7, 7, 5 }, { 1, 5, 8, 8, 5 },
                        { 1, 5, 9, 9, 5 }, { 1, 5, 10, 10, 5 }, { 2, 5, 0, 5, 0 },
                        { 2, 5, 1, 5, 1 }, { 2, 5, 2, 5, 2 }, { 2, 5, 3, 5, 3 },
                        { 2, 5, 4, 5, 4 }, { 2, 5, 5, 5, 5 }, { 2, 5, 6, 5, 6 },
                        { 2, 5, 7, 5, 7 }, { 2, 5, 8, 5, 8 }, { 2, 5, 9, 5, 9 },
                        { 2, 5, 10, 5, 10 }, { 3, 5, 5, 0, 0 }, { 3, 5, 5, 1, 1 },
                        { 3, 5, 5, 2, 2 }, { 3, 5, 5, 3, 3 }, { 3, 5, 5, 4, 4 },
                        { 3, 5, 5, 5, 5 }, { 3, 5, 5, 6, 6 }, { 3, 5, 5, 7, 7 },
                        { 3, 5, 5, 8, 8 }, { 3, 5, 5, 9, 9 }, { 3, 5, 5, 10, 10 } },
                { { 1, 6, 0, 0, 6 }, { 1, 6, 1, 1, 6 }, { 1, 6, 2, 2, 6 },
                        { 1, 6, 3, 3, 6 }, { 1, 6, 4, 4, 6 }, { 1, 6, 5, 5, 6 },
                        { 1, 6, 6, 6, 6 }, { 1, 6, 7, 7, 6 }, { 1, 6, 8, 8, 6 },
                        { 1, 6, 9, 9, 6 }, { 1, 6, 10, 10, 6 }, { 2, 6, 0, 6, 0 },
                        { 2, 6, 1, 6, 1 }, { 2, 6, 2, 6, 2 }, { 2, 6, 3, 6, 3 },
                        { 2, 6, 4, 6, 4 }, { 2, 6, 5, 6, 5 }, { 2, 6, 6, 6, 6 },
                        { 2, 6, 7, 6, 7 }, { 2, 6, 8, 6, 8 }, { 2, 6, 9, 6, 9 },
                        { 2, 6, 10, 6, 10 }, { 3, 6, 6, 0, 0 }, { 3, 6, 6, 1, 1 },
                        { 3, 6, 6, 2, 2 }, { 3, 6, 6, 3, 3 }, { 3, 6, 6, 4, 4 },
                        { 3, 6, 6, 5, 5 }, { 3, 6, 6, 6, 6 }, { 3, 6, 6, 7, 7 },
                        { 3, 6, 6, 8, 8 }, { 3, 6, 6, 9, 9 }, { 3, 6, 6, 10, 10 } },
                { { 1, 0, 0, 0, 0 }, { 2, 0, 0, 0, 0 }, { 3, 0, 0, 0, 0 },
                        { 3, 0, 0, 1, 1 }, { 3, 0, 0, 2, 2 }, { 3, 0, 0, 3, 3 },
                        { 3, 0, 0, 4, 4 }, { 3, 0, 0, 5, 5 }, { 3, 0, 0, 6, 6 },
                        { 3, 0, 0, 7, 7 }, { 3, 0, 0, 8, 8 }, { 3, 0, 0, 9, 9 },
                        { 3, 0, 0, 10, 10 } },
                { { 1, 7, 0, 0, 7 }, { 1, 7, 1, 1, 7 }, { 1, 7, 2, 2, 7 },
                        { 1, 7, 3, 3, 7 }, { 1, 7, 4, 4, 7 }, { 1, 7, 5, 5, 7 },
                        { 1, 7, 6, 6, 7 }, { 1, 7, 7, 7, 7 }, { 1, 7, 8, 8, 7 },
                        { 1, 7, 9, 9, 7 }, { 1, 7, 10, 10, 7 }, { 2, 7, 0, 7, 0 },
                        { 2, 7, 1, 7, 1 }, { 2, 7, 2, 7, 2 }, { 2, 7, 3, 7, 3 },
                        { 2, 7, 4, 7, 4 }, { 2, 7, 5, 7, 5 }, { 2, 7, 6, 7, 6 },
                        { 2, 7, 7, 7, 7 }, { 2, 7, 8, 7, 8 }, { 2, 7, 9, 7, 9 },
                        { 2, 7, 10, 7, 10 }, { 3, 7, 7, 0, 0 }, { 3, 7, 7, 1, 1 },
                        { 3, 7, 7, 2, 2 }, { 3, 7, 7, 3, 3 }, { 3, 7, 7, 4, 4 },
                        { 3, 7, 7, 5, 5 }, { 3, 7, 7, 6, 6 }, { 3, 7, 7, 7, 7 },
                        { 3, 7, 7, 8, 8 }, { 3, 7, 7, 9, 9 }, { 3, 7, 7, 10, 10 } },
                { { 1, 8, 0, 0, 8 }, { 1, 8, 1, 1, 8 }, { 1, 8, 2, 2, 8 },
                        { 1, 8, 3, 3, 8 }, { 1, 8, 4, 4, 8 }, { 1, 8, 5, 5, 8 },
                        { 1, 8, 6, 6, 8 }, { 1, 8, 7, 7, 8 }, { 1, 8, 8, 8, 8 },
                        { 1, 8, 9, 9, 8 }, { 1, 8, 10, 10, 8 }, { 2, 8, 0, 8, 0 },
                        { 2, 8, 1, 8, 1 }, { 2, 8, 2, 8, 2 }, { 2, 8, 3, 8, 3 },
                        { 2, 8, 4, 8, 4 }, { 2, 8, 5, 8, 5 }, { 2, 8, 6, 8, 6 },
                        { 2, 8, 7, 8, 7 }, { 2, 8, 8, 8, 8 }, { 2, 8, 9, 8, 9 },
                        { 2, 8, 10, 8, 10 }, { 3, 8, 8, 0, 0 }, { 3, 8, 8, 1, 1 },
                        { 3, 8, 8, 2, 2 }, { 3, 8, 8, 3, 3 }, { 3, 8, 8, 4, 4 },
                        { 3, 8, 8, 5, 5 }, { 3, 8, 8, 6, 6 }, { 3, 8, 8, 7, 7 },
                        { 3, 8, 8, 8, 8 }, { 3, 8, 8, 9, 9 }, { 3, 8, 8, 10, 10 } },
                { { 1, 9, 0, 0, 9 }, { 1, 9, 1, 1, 9 }, { 1, 9, 2, 2, 9 },
                        { 1, 9, 3, 3, 9 }, { 1, 9, 4, 4, 9 }, { 1, 9, 5, 5, 9 },
                        { 1, 9, 6, 6, 9 }, { 1, 9, 7, 7, 9 }, { 1, 9, 8, 8, 9 },
                        { 1, 9, 9, 9, 9 }, { 1, 9, 10, 10, 9 }, { 2, 9, 0, 9, 0 },
                        { 2, 9, 1, 9, 1 }, { 2, 9, 2, 9, 2 }, { 2, 9, 3, 9, 3 },
                        { 2, 9, 4, 9, 4 }, { 2, 9, 5, 9, 5 }, { 2, 9, 6, 9, 6 },
                        { 2, 9, 7, 9, 7 }, { 2, 9, 8, 9, 8 }, { 2, 9, 9, 9, 9 },
                        { 2, 9, 10, 9, 10 }, { 3, 9, 9, 0, 0 }, { 3, 9, 9, 1, 1 },
                        { 3, 9, 9, 2, 2 }, { 3, 9, 9, 3, 3 }, { 3, 9, 9, 4, 4 },
                        { 3, 9, 9, 5, 5 }, { 3, 9, 9, 6, 6 }, { 3, 9, 9, 7, 7 },
                        { 3, 9, 9, 8, 8 }, { 3, 9, 9, 9, 9 }, { 3, 9, 9, 10, 10 } },
                { { 1, 10, 0, 0, 10 }, { 1, 10, 1, 1, 10 }, { 1, 10, 2, 2, 10 },
                        { 1, 10, 3, 3, 10 }, { 1, 10, 4, 4, 10 }, { 1, 10, 5, 5, 10 },
                        { 1, 10, 6, 6, 10 }, { 1, 10, 7, 7, 10 }, { 1, 10, 8, 8, 10 },
                        { 1, 10, 9, 9, 10 }, { 1, 10, 10, 10, 10 }, { 2, 10, 0, 10, 0 },
                        { 2, 10, 1, 10, 1 }, { 2, 10, 2, 10, 2 }, { 2, 10, 3, 10, 3 },
                        { 2, 10, 4, 10, 4 }, { 2, 10, 5, 10, 5 }, { 2, 10, 6, 10, 6 },
                        { 2, 10, 7, 10, 7 }, { 2, 10, 8, 10, 8 }, { 2, 10, 9, 10, 9 },
                        { 2, 10, 10, 10, 10 }, { 3, 10, 10, 0, 0 }, { 3, 10, 10, 1, 1 },
                        { 3, 10, 10, 2, 2 }, { 3, 10, 10, 3, 3 }, { 3, 10, 10, 4, 4 },
                        { 3, 10, 10, 5, 5 }, { 3, 10, 10, 6, 6 }, { 3, 10, 10, 7, 7 },
                        { 3, 10, 10, 8, 8 }, { 3, 10, 10, 9, 9 },
                        { 3, 10, 10, 10, 10 } } };

        assert values.length == P.length;

        for (int i = 0; i < S.length; ++i) {
            final Tuples a = new Tuples();
            for (int j = 0; j < values[i].length; ++j) {
                a.add(values[i][j]);
            }
            final IntVar[] v = Stream.concat(Stream.of(S[i]), Arrays.stream(P[i]))
                    .toArray(IntVar[]::new);
            m.table(v, a, "CT+").post();
        }
    }

    public static void ifThen(final Model m, final IntVar[] S, final IntVar[][] P) {
        for (int i = 0; i < S.length; ++i) {
            {
                final BoolVar ifVar = m.intEqView(S[i], 1);
                final BoolVar thenVar = m.boolVar(
                        String.format(THEN_VAR_FMT, SS[i].substring(2), 1, PPS[0]));
                m.reifyXeqY(P[i][0], P[i][3], thenVar);
                ifVar.imp(thenVar).post();
            }
            {
                final BoolVar ifVar = m.intEqView(S[i], 1);
                final BoolVar thenVar = m.boolVar(
                        String.format(THEN_VAR_FMT, SS[i].substring(2), 1, PPS[1]));
                m.reifyXeqY(P[i][1], P[i][2], thenVar);
                ifVar.imp(thenVar).post();
            }
            {
                final BoolVar ifVar = m.intEqView(S[i], 2);
                final BoolVar thenVar = m.boolVar(
                        String.format(THEN_VAR_FMT, SS[i].substring(2), 2, PPS[0]));
                m.reifyXeqY(P[i][0], P[i][2], thenVar);
                ifVar.imp(thenVar).post();
            }
            {
                final BoolVar ifVar = m.intEqView(S[i], 2);
                final BoolVar thenVar = m.boolVar(
                        String.format(THEN_VAR_FMT, SS[i].substring(2), 2, PPS[1]));
                m.reifyXeqY(P[i][1], P[i][3], thenVar);
                ifVar.imp(thenVar).post();
            }
            {
                final BoolVar ifVar = m.intEqView(S[i], 3);
                final BoolVar thenVar = m.boolVar(
                        String.format(THEN_VAR_FMT, SS[i].substring(2), 3, PPS[0]));
                m.reifyXeqY(P[i][0], P[i][1], thenVar);
                ifVar.imp(thenVar).post();
            }
            {
                final BoolVar ifVar = m.intEqView(S[i], 3);
                final BoolVar thenVar = m.boolVar(
                        String.format(THEN_VAR_FMT, SS[i].substring(2), 3, PPS[2]));
                m.reifyXeqY(P[i][2], P[i][3], thenVar);
                ifVar.imp(thenVar).post();
            }
        }
    }

    public static void main(String[] args) throws ContradictionException, IOException {
        final Model model = new Model("DUM");

        final IntVar[] M = IntStream.range(0, MS.length)
                .mapToObj(i -> model.intVar(MS[i], i + 1, i + 1))
                .toArray(IntVar[]::new);

        final IntVar[] A = Arrays.stream(AS).map(s -> model.intVar(s, 0, MS.length))
                .toArray(IntVar[]::new);
        final IntVar[] L =
                new IntVar[] { model.intVar("L_Load", 0), model.intVar("L_Load", 0) };

        final IntVar[] E = Arrays.stream(ES).map(s -> model.intVar(s, 0, MS.length))
                .toArray(IntVar[]::new);
        final IntVar[] S = Arrays.stream(SS).map(s -> model.intVar(s, 1, 3))
                .toArray(IntVar[]::new);

        final int[] SI = new int[] { 1, 2, 2, 1, 1, 2, 3, 3, 3, 3, 2 };
        assert SI.length == S.length;

        // @formatter:off
        final IntVar[][] P = new IntVar[][] {
            { M[0], E[0], A[0], A[1] },
            { M[1], E[1], A[9], E[2] },
            { M[2], E[2], A[8], E[3] },
            { M[3], E[3], A[5], E[4] },
            { M[4], E[4], A[4], E[0] },
            { M[5], E[5], A[10], E[1] },
            { L[0], L[1], A[7], E[6] },
            { M[6], E[6], A[6], E[7] },
            { M[7], E[7], A[3], E[8] },
            { M[8], E[8], A[2], E[9] },
            { M[9], E[9], A[11], E[5] }
        };
        // @formatter:on

        final IntVar RA = model.intVar(RA_Name, 0, 0);
        final IntVar RI = model.intVar(RI_Name, -1, -1);

        final BoolVar[] A0 = Arrays.stream(A).map(a -> model.intEqView(a, 0))
                .toArray(BoolVar[]::new);

        tables(model, S, P);
        // ifThen(model, S, P);

        final IntVar MNU = model.intVar(CNU_Name, 0, 10);
        model.count(0, M, MNU).post();
        final IntVar ANU = model.intVar(ANU_Name, 0, 12);
        model.count(0, A, ANU).post();
        final IntVar LNU = model.intVar(LNU_Name, 0, 2);
        model.count(0, L, LNU).post();

        model.arithm(model.intOffsetView(ANU, -A.length), "+",
                model.intOffsetView(LNU, -L.length), "=",
                model.intOffsetView(MNU, -M.length)).post();

        for (int i = 0; i < S.length; ++i) {
            final IntVar CZ = model.intVar("S-Count-" + SS[i].substring(2), 0, 4);
            model.count(0, P[i], CZ).post();

            final BoolVar APZ = model.intEqView(CZ, 4);
            final BoolVar SPP = model.intEqView(S[i], SI[i]);
            APZ.imp(SPP).post();
        }

        model.getSolver().setLearningSignedClauses();

        // new PrintStream(Files.newOutputStream(Paths.get("./dum.txt"))).println(model);

        // model.getSolver().showDecisions(() -> "");

        final List<Solution> solutions = model.getSolver().findAllSolutions();
        System.out.println(solutions.size());

        model.getSolver().printStatistics();
    }
}