View Javadoc

1   /*******************************************************************************
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
3    *
4    * All rights reserved. This program and the accompanying materials
5    * are made available under the terms of the Eclipse Public License v1.0
6    * which accompanies this distribution, and is available at
7    * http://www.eclipse.org/legal/epl-v10.html
8    *
9    * Alternatively, the contents of this file may be used under the terms of
10   * either the GNU Lesser General Public License Version 2.1 or later (the
11   * "LGPL"), in which case the provisions of the LGPL are applicable instead
12   * of those above. If you wish to allow use of your version of this file only
13   * under the terms of the LGPL, and not to allow others to use your version of
14   * this file under the terms of the EPL, indicate your decision by deleting
15   * the provisions above and replace them with the notice and other provisions
16   * required by the LGPL. If you do not delete the provisions above, a recipient
17   * may use your version of this file under the terms of the EPL or the LGPL.
18   *******************************************************************************/
19  
20  package org.sat4j.pb.tools;
21  
22  import java.math.BigInteger;
23  import java.util.Iterator;
24  
25  import org.sat4j.core.Vec;
26  import org.sat4j.pb.IPBSolver;
27  import org.sat4j.pb.ObjectiveFunction;
28  import org.sat4j.specs.ContradictionException;
29  import org.sat4j.specs.IConstr;
30  import org.sat4j.specs.IVec;
31  import org.sat4j.specs.IVecInt;
32  import org.sat4j.tools.xplain.Xplain;
33  
34  public class XplainPB extends Xplain<IPBSolver> implements IPBSolver {
35  
36  	/**
37  	 * 
38  	 */
39  	private static final long serialVersionUID = 1L;
40  
41  	public XplainPB(IPBSolver solver) {
42  		super(solver);
43  	}
44  
45  	@Override
46  	public IConstr addAtMost(IVecInt literals, int degree)
47  			throws ContradictionException {
48  		IVec<BigInteger> coeffs = new Vec<BigInteger>();
49  		coeffs.growTo(literals.size(), BigInteger.ONE);
50  		int newvar = createNewVar(literals);
51  		literals.push(newvar);
52  		BigInteger coef = BigInteger.valueOf(degree - coeffs.size());
53  		coeffs.push(coef);
54  		IConstr constr = decorated().addPseudoBoolean(literals, coeffs, false,
55  				BigInteger.valueOf(degree));
56  		if (constr == null) {
57  			// constraint trivially satisfied
58  			discardLastestVar();
59  			// System.err.println(lits.toString()+"/"+coeffs+"/"+(moreThan?">=":"<=")+d);
60  		} else {
61  			constrs.put(newvar, constr);
62  		}
63  		return constr;
64  	}
65  
66  	public IConstr addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs,
67  			boolean moreThan, BigInteger d) throws ContradictionException {
68  		int newvar = createNewVar(lits);
69  		lits.push(newvar);
70  		if (moreThan && d.signum() >= 0) {
71  			coeffs.push(d);
72  		} else {
73  			BigInteger sum = BigInteger.ZERO;
74  			for (Iterator<BigInteger> ite = coeffs.iterator(); ite.hasNext();)
75  				sum = sum.add(ite.next());
76  			sum = sum.subtract(d);
77  			coeffs.push(sum.negate());
78  		}
79  		IConstr constr = decorated()
80  				.addPseudoBoolean(lits, coeffs, moreThan, d);
81  		if (constr == null) {
82  			// constraint trivially satisfied
83  			discardLastestVar();
84  			// System.err.println(lits.toString()+"/"+coeffs+"/"+(moreThan?">=":"<=")+d);
85  		} else {
86  			constrs.put(newvar, constr);
87  		}
88  		return constr;
89  	}
90  
91  	public void setObjectiveFunction(ObjectiveFunction obj) {
92  		decorated().setObjectiveFunction(obj);
93  	}
94  
95  	public ObjectiveFunction getObjectiveFunction() {
96  		return decorated().getObjectiveFunction();
97  	}
98  }