Logo Search packages:      
Sourcecode: sat4j version File versions

MapPb.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.minisat.constraints.cnf.Lits;
import org.sat4j.minisat.core.VarActivityListener;
import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;

/**
 * @author parrain 
 * 
 */
00041 public class MapPb implements IDataStructurePB {

    /*
     * During the process of cutting planes, pseudo-boolean constraints are
     * coded with a HashMap <literal, coefficient> and a BigInteger for the
     * degree.
     */
    protected InternalMapPBStructure weightedLits;

    protected BigInteger degree;

    MapPb(PBConstr cpb) {
        weightedLits = new InternalMapPBStructure(cpb);
        degree = cpb.getDegree();
    }

    MapPb(int size) {
        weightedLits = new InternalMapPBStructure(size);
        degree = BigInteger.ZERO;
    }

    public boolean isCardinality(){
        for (int i = 0; i < size(); i++)
            if (!(weightedLits.getCoef(i).equals(BigInteger.ONE)))
                  return false;
        return true;
    }
    
    public BigInteger saturation() {
        assert degree.signum() > 0;
        BigInteger minimum = degree;
        for (int ind = 0; ind < size(); ind++) {
            assert weightedLits.getCoef(ind).signum() > 0;
            if (degree.compareTo(weightedLits.getCoef(ind)) < 0)
                changeCoef(ind, degree);
            assert weightedLits.getCoef(ind).signum() > 0;
            minimum = minimum.min(weightedLits.getCoef(ind));
        }
        // a clause has been learned
        if (minimum.equals(degree) && minimum.compareTo(BigInteger.ONE) > 0) {
            degree = BigInteger.ONE;
            for (int ind = 0; ind < size(); ind++)
                changeCoef(ind, BigInteger.ONE);
        }

        return degree;
    }

    public BigInteger cuttingPlane(PBConstr cpb, BigInteger deg,
            BigInteger[] reducedCoefs, VarActivityListener val) {
        return cuttingPlane(cpb, deg, reducedCoefs, BigInteger.ONE, val);
    }

    public BigInteger cuttingPlane(PBConstr cpb, BigInteger degreeCons,
            BigInteger[] reducedCoefs, BigInteger coefMult,
            VarActivityListener val) {
        degree = degree.add(degreeCons);
        assert degree.signum() > 0;

        if (reducedCoefs == null)
            for (int i = 0; i < cpb.size(); i++) {
                val.varBumpActivity(cpb.get(i));
                cuttingPlaneStep(cpb.get(i), multiplyCoefficient(
                        cpb.getCoef(i), coefMult));
            }
        else
            for (int i = 0; i < cpb.size(); i++) {
                val.varBumpActivity(cpb.get(i));
                cuttingPlaneStep(cpb.get(i), multiplyCoefficient(
                        reducedCoefs[i], coefMult));
            }

        return degree;
    }

    public BigInteger cuttingPlane(int[] lits, BigInteger[] reducedCoefs,
            BigInteger deg) {
        return cuttingPlane(lits, reducedCoefs, deg, BigInteger.ONE);
    }

    public BigInteger cuttingPlane(int lits[], BigInteger[] reducedCoefs,
            BigInteger degreeCons, BigInteger coefMult) {
        degree = degree.add(degreeCons);
        assert degree.signum() > 0;

        for (int i = 0; i < lits.length; i++)
            cuttingPlaneStep(lits[i], reducedCoefs[i].multiply(coefMult));

        return degree;
    }

    private void cuttingPlaneStep(final int lit, final BigInteger coef) {
        assert coef.signum() >= 0;
        int nlit = lit ^ 1;
        if (coef.signum() > 0) {
            if (weightedLits.containsKey(nlit)) {
                assert !weightedLits.containsKey(lit);
                assert weightedLits.get(nlit) != null;
                if (weightedLits.get(nlit).compareTo(coef) < 0) {
                    BigInteger tmp = weightedLits.get(nlit);
                    setCoef(lit, coef.subtract(tmp));
                    assert weightedLits.get(lit).signum() > 0;
                    degree = degree.subtract(tmp);
                    removeCoef(nlit);
                } else {
                    if (weightedLits.get(nlit).equals(coef)) {
                        degree = degree.subtract(coef);
                        removeCoef(nlit);
                    } else {
                        decreaseCoef(nlit, coef);
                        assert weightedLits.get(nlit).signum() > 0;
                        degree = degree.subtract(coef);
                    }
                }
            } else {
                assert (!weightedLits.containsKey(lit))
                        || (weightedLits.get(lit).signum() > 0);
                if (weightedLits.containsKey(lit))
                    increaseCoef(lit, coef);
                else 
                    setCoef(lit, coef);
                assert weightedLits.get(lit).signum() > 0;
            }
        }
        assert (!weightedLits.containsKey(nlit)) || (!weightedLits.containsKey(lit));
    }

    public void buildConstraintFromConflict(IVecInt resLits,
            IVec<BigInteger> resCoefs) {
        resLits.clear();
        resCoefs.clear();
        weightedLits.copyCoefs(resCoefs);
        weightedLits.copyLits(resLits);
    };

    public void buildConstraintFromMapPb(int[] resLits, BigInteger[] resCoefs) {
        // On recherche tous les litt?raux concern?s
        assert resLits.length == resCoefs.length;
        assert resLits.length == size();
        weightedLits.copyCoefs(resCoefs);
        weightedLits.copyLits(resLits);
    };

    public BigInteger getDegree() {
        return degree;
    }

    public int size() {
        return weightedLits.size();
    }

    /*
     * (non-Javadoc)
     * 
     * @see java.lang.Object#toString()
     */
    @Override
    public String toString() {
        StringBuffer stb = new StringBuffer();
        for (int ind = 0; ind < size(); ind++) {
            stb.append(weightedLits.getCoef(ind));
            stb.append(".");
            stb.append(Lits.toString(weightedLits.getLit(ind)));
            stb.append(" ");
        }
        return stb.toString() + " >= " + degree; //$NON-NLS-1$
    }

    private BigInteger multiplyCoefficient(BigInteger coef, BigInteger mult) {
        if (coef.equals(BigInteger.ONE))
            return mult;
        return coef.multiply(mult);
    }

    void increaseCoef(int lit, BigInteger incCoef) {
        weightedLits.put(lit, weightedLits.get(lit).add(incCoef));
    }

    void decreaseCoef(int lit, BigInteger decCoef) {
        weightedLits.put(lit, weightedLits.get(lit).subtract(decCoef));
    }

    void setCoef(int lit, BigInteger newValue) {
        weightedLits.put(lit, newValue);
    }

    void changeCoef(int indLit, BigInteger newValue) {
        weightedLits.changeCoef(indLit, newValue);
    }

    void removeCoef(int lit) {
        weightedLits.remove(lit);
    }

}

Generated by  Doxygen 1.6.0   Back to index