001package org.clafer.compiler;
002
003import java.util.ArrayList;
004import java.util.HashSet;
005import java.util.List;
006import java.util.Map;
007import java.util.Map.Entry;
008import java.util.Set;
009import org.clafer.ast.AstConstraint;
010import org.clafer.collection.Either;
011import org.clafer.collection.Pair;
012import org.clafer.common.Check;
013import org.clafer.instance.InstanceModel;
014import org.clafer.ir.IrBoolVar;
015import solver.ResolutionPolicy;
016import solver.Solver;
017import solver.constraints.ICF;
018import solver.variables.BoolVar;
019import solver.variables.IntVar;
020import util.ESat;
021
022/**
023 * Either call {@link #minUnsat()} xor {@link #unsatCore()} at most once. If you
024 * need to invoke both, you need to two ClaferUnsat objects.
025 *
026 * @author jimmy
027 */
028public class ClaferUnsat {
029
030    private final Solver solver;
031    private final ClaferSolutionMap solutionMap;
032    private final Pair<AstConstraint, Either<Boolean, BoolVar>>[] softVars;
033    private final Either<Integer, IntVar> score;
034
035    ClaferUnsat(Solver solver, ClaferSolutionMap solutionMap) {
036        this.solver = Check.notNull(solver);
037        this.solutionMap = Check.notNull(solutionMap);
038        Map<AstConstraint, IrBoolVar> softVarsMap = solutionMap.getAstSolution().getSoftVarsMap();
039        @SuppressWarnings("unchecked")
040        Pair<AstConstraint, Either<Boolean, BoolVar>>[] soft = new Pair[softVarsMap.size()];
041        int i = 0;
042        for (Entry<AstConstraint, IrBoolVar> entry : softVarsMap.entrySet()) {
043            soft[i++] = new Pair<>(
044                    entry.getKey(),
045                    solutionMap.getIrSolution().getBoolVar(entry.getValue()));
046        }
047        assert i == soft.length;
048        this.softVars = soft;
049        this.score = solutionMap.getIrSolution().getIntVar(solutionMap.getAstSolution().getSumSoftVar());
050    }
051
052    public Solver getInternalSolver() {
053        return solver;
054    }
055
056    /**
057     * Compute the minimal set of constraints that need to be removed before the
058     * model is satisfiable. If the model is already satisfiable, then the set
059     * is empty. Guaranteed to be minimum.
060     *
061     * @return the Min-Unsat and the corresponding near-miss example or null if
062     * unknown
063     */
064    public Pair<Set<AstConstraint>, InstanceModel> minUnsat() {
065        if (ESat.TRUE.equals(maximize())) {
066            Set<AstConstraint> unsat = new HashSet<>();
067            for (Pair<AstConstraint, Either<Boolean, BoolVar>> softVar : softVars) {
068                Either<Boolean, BoolVar> var = softVar.getSnd();
069                if (var.isLeft()
070                        ? !var.getLeft().booleanValue()
071                        : var.getRight().instantiatedTo(0)) {
072                    unsat.add(softVar.getFst());
073                }
074            }
075            return new Pair<>(unsat, solutionMap.getInstance());
076        }
077        return null;
078    }
079
080    /**
081     * Compute a small set of constraints that are mutually unsatisfiable.
082     * Undefined behaviour if the model is satisfiable. This method is always
083     * slower to compute than {@link #minUnsat()}. Not guaranteed to be minimum.
084     *
085     * @return the Unsat-Core or null if unknown
086     */
087    public Set<AstConstraint> unsatCore() {
088        Set<AstConstraint> unsat = new HashSet<>();
089        switch (maximize()) {
090            case TRUE:
091                boolean changed;
092                do {
093                    changed = false;
094                    List<BoolVar> minUnsat = new ArrayList<>();
095                    for (Pair<AstConstraint, Either<Boolean, BoolVar>> softVar : softVars) {
096                        Either<Boolean, BoolVar> var = softVar.getSnd();
097                        if (var.isLeft()
098                                ? !var.getLeft().booleanValue()
099                                : var.getRight().instantiatedTo(0)) {
100                            changed |= unsat.add(softVar.getFst());
101                            if (var.isRight()) {
102                                minUnsat.add(var.getRight());
103                            }
104                        }
105                    }
106                    solver.getSearchLoop().reset();
107                    for (BoolVar var : minUnsat) {
108                        solver.postCut(ICF.arithm(var, "=", 1));
109                    }
110                } while (changed && ESat.TRUE.equals(maximize()));
111                return unsat;
112            default:
113                return null;
114        }
115    }
116
117    private ESat maximize() {
118        if (score.isLeft()) {
119            solver.findSolution();
120        } else {
121            solver.findOptimalSolution(ResolutionPolicy.MAXIMIZE, score.getRight());
122        }
123        return solver.isFeasible();
124    }
125}