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 addAtLeast(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(coeffs.size() - degree);
53  		coeffs.push(coef);
54  		IConstr constr = decorated().addPseudoBoolean(literals, coeffs, true,
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  	@Override
67  	public IConstr addAtMost(IVecInt literals, int degree)
68  			throws ContradictionException {
69  		IVec<BigInteger> coeffs = new Vec<BigInteger>();
70  		coeffs.growTo(literals.size(), BigInteger.ONE);
71  		int newvar = createNewVar(literals);
72  		literals.push(newvar);
73  		BigInteger coef = BigInteger.valueOf(degree - coeffs.size());
74  		coeffs.push(coef);
75  		IConstr constr = decorated().addPseudoBoolean(literals, coeffs, false,
76  				BigInteger.valueOf(degree));
77  		if (constr == null) {
78  			// constraint trivially satisfied
79  			discardLastestVar();
80  			// System.err.println(lits.toString()+"/"+coeffs+"/"+(moreThan?">=":"<=")+d);
81  		} else {
82  			constrs.put(newvar, constr);
83  		}
84  		return constr;
85  	}
86  
87  	public IConstr addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs,
88  			boolean moreThan, BigInteger d) throws ContradictionException {
89  		int newvar = createNewVar(lits);
90  		lits.push(newvar);
91  		if (moreThan && d.signum() >= 0) {
92  			coeffs.push(d);
93  		} else {
94  			BigInteger sum = BigInteger.ZERO;
95  			for (Iterator<BigInteger> ite = coeffs.iterator(); ite.hasNext();)
96  				sum = sum.add(ite.next());
97  			sum = sum.subtract(d);
98  			coeffs.push(sum.negate());
99  		}
100 		IConstr constr = decorated()
101 				.addPseudoBoolean(lits, coeffs, moreThan, d);
102 		if (constr == null) {
103 			// constraint trivially satisfied
104 			discardLastestVar();
105 			// System.err.println(lits.toString()+"/"+coeffs+"/"+(moreThan?">=":"<=")+d);
106 		} else {
107 			constrs.put(newvar, constr);
108 		}
109 		return constr;
110 	}
111 
112 	public void setObjectiveFunction(ObjectiveFunction obj) {
113 		decorated().setObjectiveFunction(obj);
114 	}
115 
116 	public ObjectiveFunction getObjectiveFunction() {
117 		return decorated().getObjectiveFunction();
118 	}
119 }