Logo Search packages:      
Sourcecode: sat4j version File versions

ConflictMap.java

/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions
* required by the LGPL. If you do not delete the provisions above, a recipient
* may use your version of this file under the terms of the EPL or the LGPL.
* 
* Based on the pseudo boolean algorithms described in:
* A fast pseudo-Boolean constraint solver Chai, D.; Kuehlmann, A.
* Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on
* Volume 24, Issue 3, March 2005 Page(s): 305 - 317
* 
* and 
* Heidi E. Dixon, 2004. Automating Pseudo-Boolean Inference within a DPLL 
* Framework. Ph.D. Dissertation, University of Oregon.
*******************************************************************************/
package org.sat4j.pb.constraints.pb;

import java.math.BigInteger;

import org.sat4j.core.VecInt;
import org.sat4j.minisat.constraints.cnf.Lits;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.VarActivityListener;
import org.sat4j.specs.IteratorInt;

/**
 * @author parrain TODO To change the template for this generated type comment
 *         go to Window - Preferences - Java - Code Style - Code Templates
 */
00042 public class ConflictMap extends MapPb implements IConflict {

    private final ILits voc;

    /**
     * to store the slack of the current resolvant
     */
00049     protected BigInteger currentSlack;

    protected int currentLevel;

    /**
     * allows to access directly to all variables belonging to a particular
     * level At index 0, unassigned literals are stored (usually level -1); so
     * there is always a step between index and levels.
     */
00058     protected VecInt[] byLevel;

    /**
     * constructs the data structure needed to perform cutting planes
     * 
     * @param cpb
     *                pseudo-boolean constraint which rosed the conflict
     * @param level
     *                current decision level
     * @return a conflict on which cutting plane can be performed.
     */
00069     public static IConflict createConflict(PBConstr cpb, int level) {
        return new ConflictMap(cpb, level);
    }

    ConflictMap(PBConstr cpb, int level) {
        super(cpb);
        this.voc = cpb.getVocabulary();
        this.currentLevel = level;
        initStructures();
    }

    private void initStructures() {
        currentSlack = BigInteger.ZERO;
        byLevel = new VecInt[levelToIndex(currentLevel) + 1];
        int ilit, litLevel, index;
        BigInteger tmp;
        for (int i = 0; i < size(); i++) {
            ilit = weightedLits.getLit(i);
            litLevel = voc.getLevel(ilit);
            // eventually add to slack
            tmp = weightedLits.getCoef(i);
            if ((tmp.signum() > 0)
                    && (((!voc.isFalsified(ilit)) || litLevel == currentLevel)))
                currentSlack = currentSlack.add(tmp);
            // add to byLevel structure
            index = levelToIndex(litLevel);
            if (byLevel[index] == null) {
                byLevel[index] = new VecInt();
            }
            byLevel[index].push(ilit);
        }
    }

    /**
     * convert level into an index in the byLevel structure
     * 
     * @param level
     * @return
     */
00108     private static final int levelToIndex(int level) {
        return level + 1;
    }

    /**
     * convert index in the byLevel structure into a level
     * 
     * @param indLevel
     * @return
     */
00118     private static final int indexToLevel(int indLevel) {
        return indLevel - 1;
    }

    /*
     * coefficient to be computed.
     * 
     */
    protected BigInteger coefMult = BigInteger.ZERO;

    protected BigInteger coefMultCons = BigInteger.ZERO;

    /**
     * computes a cutting plane with a pseudo-boolean constraint. this method
     * updates the current instance (of ConflictMap).
     * 
     * @param cpb
     *                constraint to compute with the cutting plane
     * @param litImplied
     *                literal that must be resolved by the cutting plane
     * @return an update of the degree of the current instance
     */
00140     public BigInteger resolve(PBConstr cpb, int litImplied,
            VarActivityListener val) {
        assert litImplied > 1;
        int nLitImplied = litImplied ^ 1;
        if (cpb == null || !weightedLits.containsKey(nLitImplied)) {
            // no resolution
            // undo operation should be anticipated
            int litLevel = levelToIndex(voc.getLevel(litImplied));
            int lit = 0;
            if (byLevel[litLevel] != null) {
                if (byLevel[litLevel].contains(litImplied)) {
                    lit = litImplied;
                    assert weightedLits.containsKey(litImplied);
                } else if (byLevel[litLevel].contains(nLitImplied)) {
                    lit = nLitImplied;
                    assert weightedLits.containsKey(nLitImplied);
                }
            }

            if (lit > 0) {
                byLevel[litLevel].remove(lit);
                if (byLevel[0] == null)
                    byLevel[0] = new VecInt();
                byLevel[0].push(lit);
            }
            return degree;
        }

        assert slackConflict().signum() <= 0;
        assert degree.signum() >= 0;

        // coefficients of the constraint must be copied in an other structure
        // in order to make reduction operations.
        BigInteger[] coefsCons = null;
        BigInteger degreeCons = cpb.getDegree();

        // search of the index of the implied literal
        int ind = 0;
        while (cpb.get(ind) != litImplied)
            ind++;

        assert cpb.get(ind) == litImplied;
        assert cpb.getCoef(ind) != BigInteger.ZERO;

        if (cpb.getCoef(ind).equals(BigInteger.ONE)) {
            // then we know that the resolvant will still be a conflict (cf.
            // Dixon's property)
            coefMultCons = weightedLits.get(nLitImplied);
            coefMult = BigInteger.ONE;
            // updating of the degree of the conflict
            degreeCons = degreeCons.multiply(coefMultCons);
        } else {
            if (weightedLits.get(nLitImplied).equals(BigInteger.ONE)) {
                // then we know that the resolvant will still be a conflict (cf.
                // Dixon's property)
                coefMult = cpb.getCoef(ind);
                coefMultCons = BigInteger.ONE;
                // updating of the degree of the conflict
                degree = degree.multiply(coefMult);
            } else {
                // pb-constraint has to be reduced
                // to obtain a conflictual result from the cutting plane
                WatchPb wpb = (WatchPb) cpb; // DLB Findbugs warning ok
                coefsCons = wpb.getCoefs();
                assert positiveCoefs(coefsCons);
                degreeCons = reduceUntilConflict(litImplied, ind, coefsCons,
                        wpb);
                // updating of the degree of the conflict
                degreeCons = degreeCons.multiply(coefMultCons);
                degree = degree.multiply(coefMult);
            }

            // coefficients of the conflict must be multiplied by coefMult
            if (!coefMult.equals(BigInteger.ONE))
                for (int i = 0; i < size(); i++) {
                    changeCoef(i, weightedLits.getCoef(i).multiply(coefMult));
                }
        }

        assert slackConflict().signum() <= 0;

        // cutting plane
        degree = cuttingPlane(cpb, degreeCons, coefsCons, coefMultCons, val);

        // neither litImplied nor nLitImplied is present in coefs structure
        assert !weightedLits.containsKey(litImplied);
        assert !weightedLits.containsKey(nLitImplied);
        // neither litImplied nor nLitImplied is present in byLevel structure
        assert getLevelByLevel(litImplied) == -1;
        assert getLevelByLevel(nLitImplied) == -1;
        assert degree.signum() > 0;
        assert slackConflict().signum() <= 0;

        // saturation
        degree = saturation();
        assert slackConflict().signum() <= 0;

        return degree;
    }

    protected BigInteger reduceUntilConflict(int litImplied, int ind,
            BigInteger[] reducedCoefs, WatchPb wpb) {
        BigInteger slackResolve = BigInteger.ONE.negate();
        BigInteger slackThis = BigInteger.ZERO;
        BigInteger slackIndex;
        BigInteger slackConflict = slackConflict();
        BigInteger ppcm;
        BigInteger reducedDegree = wpb.getDegree();
        BigInteger previousCoefLitImplied = BigInteger.ZERO;
        BigInteger tmp;
        BigInteger coefLitImplied = weightedLits.get(litImplied ^ 1);

        do {
            if (slackResolve.signum() >= 0) {
                assert slackThis.signum() > 0;
                tmp = reduceInConstraint(wpb, reducedCoefs, ind, reducedDegree);
                assert ((tmp.compareTo(reducedDegree) < 0) && (tmp
                        .compareTo(BigInteger.ONE) >= 0));
                reducedDegree = tmp;
            }
            // search of the multiplying coefficients
            assert weightedLits.get(litImplied ^ 1).signum() > 0;
            assert reducedCoefs[ind].signum() > 0;

            if (!reducedCoefs[ind].equals(previousCoefLitImplied)) {
                assert coefLitImplied.equals(weightedLits.get(litImplied ^ 1));
                ppcm = ppcm(reducedCoefs[ind], coefLitImplied);
                assert ppcm.signum() > 0;
                coefMult = ppcm.divide(coefLitImplied);
                coefMultCons = ppcm.divide(reducedCoefs[ind]);

                assert coefMultCons.signum() > 0;
                assert coefMult.signum() > 0;
                assert coefMult.multiply(coefLitImplied).equals(
                        coefMultCons.multiply(reducedCoefs[ind]));
                previousCoefLitImplied = reducedCoefs[ind];
            }

            // slacks computed for each constraint
            slackThis = wpb.slackConstraint(reducedCoefs, reducedDegree)
                    .multiply(coefMultCons);
            assert slackConflict.equals(slackConflict());
            slackIndex = slackConflict.multiply(coefMult);
            assert slackIndex.signum() <= 0;
            // estimate of the slack after the cutting plane
            slackResolve = slackThis.add(slackIndex);
        } while (slackResolve.signum() >= 0);
        assert coefMult.multiply(weightedLits.get(litImplied ^ 1)).equals(
                coefMultCons.multiply(reducedCoefs[ind]));
        return reducedDegree;

    }

    /**
     * computes the slack of the current instance
     */
00296     public BigInteger slackConflict() {
        BigInteger poss = BigInteger.ZERO;
        BigInteger tmp;
        // for each literal
        for (int i = 0; i < size(); i++) {
            tmp = weightedLits.getCoef(i);
            if (tmp.signum() != 0 && !voc.isFalsified(weightedLits.getLit(i)))
                poss = poss.add(tmp);
        }
        return poss.subtract(degree);
    }

    public boolean oldIsAssertive(int dl) {
        BigInteger tmp;
        int lit;
        BigInteger slack = computeSlack(dl).subtract(degree);
        if (slack.signum() < 0)
            return false;
        for (int i = 0; i < size(); i++) {
            tmp = weightedLits.getCoef(i);
            lit = weightedLits.getLit(i);
            if ((tmp.signum() > 0)
                    && (voc.isUnassigned(lit) || voc.getLevel(lit) >= dl)
                    && (slack.compareTo(tmp) < 0))
                return true;
        }
        return false;
    }

    // computes a slack with respect to a particular decision level
    private BigInteger computeSlack(int dl) {
        BigInteger slack = BigInteger.ZERO;
        int lit;
        BigInteger tmp;
        for (int i = 0; i < size(); i++) {
            tmp = weightedLits.getCoef(i);
            lit = weightedLits.getLit(i);
            if ((tmp.signum() > 0)
                    && (((!voc.isFalsified(lit)) || voc.getLevel(lit) >= dl)))
                slack = slack.add(tmp);
        }
        return slack;
    }

    /**
     * tests if the conflict is assertive (allows to imply a literal) at a
     * particular decision level
     * 
     * @param dl
     *                the decision level
     * @return true if the conflict is assertive at the decision level
     */
00348     public boolean isAssertive(int dl) {
        assert dl <= currentLevel;
        assert dl <= currentLevel;

        currentLevel = dl;
        // assert currentSlack.equals(computeSlack(dl));
        BigInteger slack = currentSlack.subtract(degree);
        if (slack.signum() < 0)
            return false;
        return isImplyingLiteral(slack);
    }

    // given the slack already computed, tests if a literal could be implied at
    // a particular level
    // uses the byLevel data structure to parse each literal by decision level
    private boolean isImplyingLiteral(BigInteger slack) {
        // unassigned literals are tried first
        int unassigned = levelToIndex(-1);
        if (byLevel[unassigned] != null) {
            for (IteratorInt iterator = byLevel[unassigned].iterator(); iterator
                    .hasNext();) {
                if (slack.compareTo(weightedLits.get(iterator.next())) < 0)
                    return true;
            }
        }
        // then we have to look at every literal at a decision level >=dl
        BigInteger tmp;
        int level = levelToIndex(currentLevel);
        if (byLevel[level] != null)
            for (IteratorInt iterator = byLevel[level].iterator(); iterator
                    .hasNext();) {
                tmp = weightedLits.get(iterator.next());
                if (tmp != null && slack.compareTo(tmp) < 0)
                    return true;
            }
        return false;
    }

    // given the slack already computed, tests if a literal could be implied at
    // a particular level
    // uses the coefs data structure (where coefficients are decreasing ordered)
    // to parse each literal
    private boolean isImplyingLiteralOrdered(int dl, BigInteger slack) {
        int ilit, litLevel;
        for (int i = 0; i < size(); i++) {
            ilit = weightedLits.getLit(i);
            litLevel = voc.getLevel(ilit);
            if ((litLevel >= dl || voc.isUnassigned(ilit))
                    && (slack.compareTo(weightedLits.getCoef(i)) < 0))
                return true;
        }
        return false;
    }

    /**
     * computes the least common factor of two integers (Plus Petit Commun
     * Multiple in french)
     * 
     * @param a
     *                first integer
     * @param b
     *                second integer
     * @return the least common factor
     */
00412     protected static BigInteger ppcm(BigInteger a, BigInteger b) {
        return a.divide(a.gcd(b)).multiply(b);
    }

    /**
     * constraint reduction : removes a literal of the constraint. The literal
     * should be either unassigned or satisfied. The literal can not be the
     * literal that should be resolved.
     * 
     * @param wpb
     *                the initial constraint to reduce
     * @param coefsBis
     *                the coefficients of the constraint wrt which the reduction
     *                will be proposed
     * @param indLitImplied
     *                index in wpb of the literal that should be resolved
     * @param degreeBis
     *                the degree of the constraint wrt which the reduction will
     *                be proposed
     * @return new degree of the reduced constraint
     */
00433     public BigInteger reduceInConstraint(WatchPb wpb,
            final BigInteger[] coefsBis, final int indLitImplied,
            final BigInteger degreeBis) {
        // logger.entering(this.getClass().getName(),"reduceInConstraint");
        assert degreeBis.compareTo(BigInteger.ONE) > 0;
        // search of an unassigned literal
        int lit = -1;
        for (int ind = 0; (ind < wpb.lits.length) && (lit == -1); ind++)
            if (coefsBis[ind].signum() != 0 && voc.isUnassigned(wpb.lits[ind])) {
                assert coefsBis[ind].compareTo(degreeBis) < 0;
                lit = ind;
            }

        // else, search of a satisfied literal
        if (lit == -1)
            for (int ind = 0; (ind < wpb.lits.length) && (lit == -1); ind++)
                if ((coefsBis[ind].signum() != 0)
                        && (voc.isSatisfied(wpb.lits[ind]))
                        && (ind != indLitImplied))
                    lit = ind;

        // a literal has been found
        assert lit != -1;

        assert lit != indLitImplied;
        // logger.finer("Found literal "+Lits.toString(lits[lit]));
        // reduction can be done
        BigInteger degUpdate = degreeBis.subtract(coefsBis[lit]);
        coefsBis[lit] = BigInteger.ZERO;

        // saturation of the constraint
        degUpdate = saturation(coefsBis, degUpdate);

        assert coefsBis[indLitImplied].signum() > 0;
        assert degreeBis.compareTo(degUpdate) > 0;
        return degUpdate;
    }

    static BigInteger saturation(BigInteger[] coefs, BigInteger degree) {
        assert degree.signum() > 0;
        BigInteger minimum = degree;
        for (int i = 0; i < coefs.length; i++) {
            if (coefs[i].signum() > 0)
                minimum = minimum.min(coefs[i]);
            coefs[i] = degree.min(coefs[i]);
        }
        if (minimum.equals(degree) && !degree.equals(BigInteger.ONE)) {
            // the result is a clause
            // there is no more possible reduction
            degree = BigInteger.ONE;
            for (int i = 0; i < coefs.length; i++)
                if (coefs[i].signum() > 0)
                    coefs[i] = degree;
        }
        return degree;
    }

    private static boolean positiveCoefs(final BigInteger[] coefsCons) {
        for (int i = 0; i < coefsCons.length; i++) {
            if (coefsCons[i].signum() <= 0)
                return false;
        }
        return true;
    }

    /**
     * computes the level for the backtrack : the highest decision level for
     * which the conflict is assertive.
     * 
     * @param maxLevel
     *                the lowest level for which the conflict is assertive
     * @return the highest level (smaller int) for which the constraint is
     *         assertive.
     */
00507     public int getBacktrackLevel(int maxLevel) {
        // we are looking for a level higher than maxLevel
        // where the constraint is still assertive
        VecInt lits;
        int level;
        int indStop = levelToIndex(maxLevel) - 1;
        int indStart = levelToIndex(0);
        BigInteger slack = computeSlack(0).subtract(degree);
        int previous = 0;
        for (int indLevel = indStart; indLevel <= indStop; indLevel++) {
            if (byLevel[indLevel] != null) {
                level = indexToLevel(indLevel);
                assert computeSlack(level).subtract(degree).equals(slack);
                if (isImplyingLiteralOrdered(level, slack)) {
                    break;
                }
                // updating the new slack
                lits = byLevel[indLevel];
                int lit;
                for (IteratorInt iterator = lits.iterator(); iterator.hasNext();) {
                    lit = iterator.next();
                    if (voc.isFalsified(lit)
                            && voc.getLevel(lit) == indexToLevel(indLevel))
                        slack = slack.subtract(weightedLits.get(lit));
                }
                if (!lits.isEmpty())
                    previous = level;
            }
        }
        assert previous == oldGetBacktrackLevel(maxLevel);
        return previous;
    }

    public int oldGetBacktrackLevel(int maxLevel) {
        int litLevel;
        int borneMax = maxLevel;
        assert oldIsAssertive(borneMax);
        int borneMin = -1;
        // borneMax is the highest level in the search tree where the constraint is assertive
        for (int i = 0; i < size() ; i++) {
            litLevel = voc.getLevel(weightedLits.getLit(i));
            if (litLevel < borneMax && litLevel > borneMin
                    && oldIsAssertive(litLevel))
                borneMax = litLevel;
        }
        // the level returned is the first level below borneMax
        // where there is a literal belonging to the constraint
        int retour = 0;
        for (int i = 0; i < size(); i++) {
            litLevel = voc.getLevel(weightedLits.getLit(i));
            if (litLevel > retour && litLevel < borneMax) {
                retour = litLevel;
            }
        }
        return retour;
    }

    public void updateSlack(int level) {
        int dl = levelToIndex(level);
        if (byLevel[dl] != null) {
            int lit;
            for (IteratorInt iterator = byLevel[dl].iterator(); iterator
                    .hasNext();) {
                lit = iterator.next();
                if (voc.isFalsified(lit))
                    currentSlack = currentSlack.add(weightedLits.get(lit));
            }
        }
    }

    @Override
    void increaseCoef(int lit, BigInteger incCoef) {
        if ((!voc.isFalsified(lit)) || voc.getLevel(lit) == currentLevel) {
            currentSlack = currentSlack.add(incCoef);
        }
        assert byLevel[levelToIndex(voc.getLevel(lit))].contains(lit);
        super.increaseCoef(lit, incCoef);
    }

    @Override
    void decreaseCoef(int lit, BigInteger decCoef) {
        if ((!voc.isFalsified(lit)) || voc.getLevel(lit) == currentLevel) {
            currentSlack = currentSlack.subtract(decCoef);
        }
        assert byLevel[levelToIndex(voc.getLevel(lit))].contains(lit);
        super.decreaseCoef(lit, decCoef);
    }

    @Override
    void setCoef(int lit, BigInteger newValue) {
        int litLevel = voc.getLevel(lit);
        if ((!voc.isFalsified(lit)) || litLevel == currentLevel) {
            if (weightedLits.containsKey(lit))
                currentSlack = currentSlack.subtract(weightedLits.get(lit));
            currentSlack = currentSlack.add(newValue);
        }
        int indLitLevel = levelToIndex(litLevel);
        if (!weightedLits.containsKey(lit)) {
            if (byLevel[indLitLevel] == null) {
                byLevel[indLitLevel] = new VecInt();
            }
            byLevel[indLitLevel].push(lit);

        }
        assert byLevel[indLitLevel] != null;
        assert byLevel[indLitLevel].contains(lit);
        super.setCoef(lit, newValue);
    }

    @Override
    void changeCoef(int indLit, BigInteger newValue) {
      int lit = weightedLits.getLit(indLit);
        int litLevel = voc.getLevel(lit);
        if ((!voc.isFalsified(lit)) || litLevel == currentLevel) {
            if (weightedLits.containsKey(lit))
                currentSlack = currentSlack.subtract(weightedLits.get(lit));
            currentSlack = currentSlack.add(newValue);
        }
        int indLitLevel = levelToIndex(litLevel);
        assert weightedLits.containsKey(lit);
        assert byLevel[indLitLevel] != null;
        assert byLevel[indLitLevel].contains(lit);
        super.changeCoef(indLit, newValue);
    }


    @Override
    void removeCoef(int lit) {
        int litLevel = voc.getLevel(lit);
        if ((!voc.isFalsified(lit)) || litLevel == currentLevel) {
            currentSlack = currentSlack.subtract(weightedLits.get(lit));
        }
        int indLitLevel = levelToIndex(litLevel);
        assert indLitLevel < byLevel.length;
        assert byLevel[indLitLevel] != null;
        assert byLevel[indLitLevel].contains(lit);
        byLevel[indLitLevel].remove(lit);
        super.removeCoef(lit);
    }
    
    
    private int getLevelByLevel(int lit) {
        for (int i = 0; i < byLevel.length; i++)
            if (byLevel[i] != null && byLevel[i].contains(lit))
                return i;
        return -1;
    }

    public boolean slackIsCorrect(int dl) {
        return currentSlack.equals(computeSlack(dl));
    }

    @Override
    public String toString() {
        int lit;
        StringBuffer stb = new StringBuffer();
        for (int i = 0; i < size(); i++) {
            lit = weightedLits.getLit(i);
            stb.append(weightedLits.getCoef(i));
            stb.append(".");
            stb.append(Lits.toString(lit));
            stb.append(" ");
            stb.append("[");
            stb.append(voc.valueToString(lit));
            stb.append("@");
            stb.append(voc.getLevel(lit));
            stb.append("]");
        }
        return stb.toString() + " >= " + degree; //$NON-NLS-1$
    }

}

Generated by  Doxygen 1.6.0   Back to index