NonLinearReverting.java

NonLinearReverting.java

import org.chocosolver.solver.Model;
import org.chocosolver.solver.constraints.Constraint;
import org.chocosolver.solver.exception.ContradictionException;
import org.chocosolver.solver.variables.IntVar;

import java.util.List;

public class NonLinearReverting {
    public static void main(String[] args) throws ContradictionException {
        // the final output of both methods should be the same
        System.out.println(">> Expected");
        expected();

        System.out.println("\n-------------\n");

        System.out.println(">> Actual");
        actual();
    }

    public static void expected() throws ContradictionException {
        Model m = new Model();
        IntVar x = m.intVar("x", 0, 5);
        IntVar y = m.intVar("y", 0, 5);
        IntVar z = m.intVar("z", 0, 5);
        // background knowledge (static)
        m.arithm(x, "<", y).post();
        m.arithm(y, "<", z).post();

        // user inputs (dynamic)
        var y1 = m.arithm(y, "=", 1);
        propagateUserConstraint(m, y1);

        System.out.println(x);
        System.out.println(y);
        System.out.println(z);
    }

    public static void actual() throws ContradictionException {
        Model m = new Model();
        IntVar x = m.intVar("x", 0, 5);
        IntVar y = m.intVar("y", 0, 5);
        IntVar z = m.intVar("z", 0, 5);
        // background knowledge (static)
        var knowledgeBase = List.of(
                m.arithm(x, "<", y),
                m.arithm(y, "<", z)
        );
        knowledgeBase.forEach(Constraint::post);
        m.getEnvironment().worldPush();

        // user inputs (dynamic)
        Constraint x2 = m.arithm(x, "=", 2);
        propagateUserConstraint(m, x2);

        System.out.println(">>> After " + x2);
        System.out.println(x);
        System.out.println(y);
        System.out.println(z);

        Constraint y1 = m.arithm(y, "=", 1);
        try {
            propagateUserConstraint(m, y1);
            // creates a conflict. The user decides to remove the 'x2' constraint
        } catch (ContradictionException e) {
            System.out.println("err: failed to apply " + y1);
            System.out.println(e);
            // using QuickXplain (https://github.com/chocoteam/choco-solver/issues/509#issuecomment-335907477)
            var conflicts = QuickXplain.quickXPlain(knowledgeBase, List.of(x2, y1), m);
            System.out.println("conflicts = " + conflicts);
            System.out.println("\n>>> After failed " + y1);
            System.out.println(x);
            System.out.println(y);
            System.out.println(z);
            m.unpost(x2);
//            m.getSolver().reset();
            try {
                m.getSolver().propagate();
                System.out.println("\n>>> After unposting " + x2);
                System.out.println(x);
                System.out.println(y);
                System.out.println(z);
            } catch (ContradictionException contradictionException) {
                System.out.println("err: undoing " + x2 + " failed");
                System.out.println(contradictionException);
            }
        }
    }

    private static void propagateUserConstraint(Model m, Constraint constraint) throws ContradictionException {
        constraint.post();
        m.getSolver().propagate();
    }
}