QuickXplain.java

QuickXplain.java

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

import java.util.ArrayList;
import java.util.Collection;
import java.util.HashSet;
import java.util.List;

//QuickXPlain Algorithm	"Ulrich Junker"
//--------------------
//QuickXPlain(B, C={c1,c2,…, cm})
//IF consistent(B∪C) return "No conflict";
//IF isEmpty(C) return Φ;
//ELSE return QX(B, B, C);

//func QX(B,Δ, C={c1,c2, …, cq}): conflictSet Δ
//IF (Δ != Φ AND inconsistent(B)) return Φ; /* pruning of C */
//IF (C = {cα}) return({cα}); /* conflict element cα detected */
//k=n/2;
//C1 <-- {c1, …, ck}; C2 <-- {ck+1, …, cq}; /* B still consistent */
//D2 <-- QX(B ∪ C1, C1, C2);
//D1 <-- QX(B ∪ D2, D2, C1);
//return (D2 ∪ D1)

class QuickXplain {
    private QuickXplain() {
        throw new AssertionError("forbidden to instantiate a utility class");
    }

    static Collection<Constraint> quickXPlain(Collection<Constraint> knowledgeBase,
                                              Collection<? extends Constraint> userConstraints,
                                              Model model) {
        var ac = new ArrayList<Constraint>(knowledgeBase.size() + userConstraints.size());
        ac.addAll(knowledgeBase);
        ac.addAll(userConstraints);
        //IF (is empty(C) or consistent(B ∪ C)) return Φ
        if (userConstraints.isEmpty() || isConsistent(ac, model)) {
            model.unpost(model.getCstrs());
            model.getSolver().reset();
            for (Constraint constraint : ac) {
                model.post(constraint);
            }
            try {
                model.getSolver().propagate();
            } catch (ContradictionException ignored) {
            }
            return List.of();
        } else { //ELSE return QX(B, B, C)
            var conflictSet = qx(knowledgeBase, knowledgeBase, new ArrayList<>(userConstraints), model);
            model.unpost(model.getCstrs());
            model.getSolver().reset();
            for (Constraint constraint : ac) {
                model.post(constraint);
            }
            try {
                model.getSolver().propagate();
            } catch (ContradictionException ignored) {
            }
            return conflictSet;
        }
    }

    // func QX(B,Δ, C={c1,c2, …, cq}): conflictSet Δ
    private static Collection<Constraint> qx(Collection<Constraint> b,
                                             Collection<Constraint> d,
                                             List<Constraint> c,
                                             Model model) {
        int cSize = c.size();
        // IF (Δ != Φ AND inconsistent(B)) return Φ;
        if (!d.isEmpty())
            if (!isConsistent(b, model)) {
                return List.of();
            }
        // if singleton(C) return C;
        if (cSize == 1) {
            return c;
        }
        int k = cSize / 2;  // k = q/2;
        // C1 = {c1..ck}; C2 = {ck+1..cq};
        List<Constraint> c1 = c.subList(0, k);
        List<Constraint> c2 = c.subList(k, cSize);
        // D2 = QX(B ∪ C1, C1, C2);  // D1 = QX(B ∪ D2, D2, C1);
        Collection<Constraint> d2 = qx(union(b, c1), c1, c2, model);
        Collection<Constraint> conflictSet = new HashSet<>(d2);
        Collection<Constraint> d1 = qx(union(b, d2), d2, c1, model);
        conflictSet.addAll(d1);
        return conflictSet;
    }

    // Check if set of constraint is consistent
    private static boolean isConsistent(Iterable<Constraint> constraints, Model model) {
        model.unpost(model.getCstrs());
        model.getSolver().reset();
        for (Constraint constr : constraints) {
            model.post(constr);
        }
        // let the solver check if the model is consistent
        return model.getSolver().solve();
    }

    //Calculate c1 ∪ c2
    private static List<Constraint> union(Collection<Constraint> c1, Collection<Constraint> c2) {
        var union = new ArrayList<Constraint>(c1.size() + c2.size());
        union.addAll(c1);
        union.addAll(c2);
        return union;
    }
}