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   * Based on the pseudo boolean algorithms described in:
20   * A fast pseudo-Boolean constraint solver Chai, D.; Kuehlmann, A.
21   * Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on
22   * Volume 24, Issue 3, March 2005 Page(s): 305 - 317
23   * 
24   * and 
25   * Heidi E. Dixon, 2004. Automating Pseudo-Boolean Inference within a DPLL 
26   * Framework. Ph.D. Dissertation, University of Oregon.
27   *******************************************************************************/
28  package org.sat4j.pb.core;
29  
30  import java.math.BigInteger;
31  
32  import org.sat4j.core.ConstrGroup;
33  import org.sat4j.core.Vec;
34  import org.sat4j.minisat.core.IOrder;
35  import org.sat4j.minisat.core.LearningStrategy;
36  import org.sat4j.minisat.core.RestartStrategy;
37  import org.sat4j.minisat.core.SearchParams;
38  import org.sat4j.minisat.core.Solver;
39  import org.sat4j.pb.IPBSolver;
40  import org.sat4j.pb.ObjectiveFunction;
41  import org.sat4j.pb.orders.IOrderObjective;
42  import org.sat4j.specs.ContradictionException;
43  import org.sat4j.specs.IConstr;
44  import org.sat4j.specs.IVec;
45  import org.sat4j.specs.IVecInt;
46  
47  public abstract class PBSolver extends Solver<PBDataStructureFactory> implements
48  		IPBSolver {
49  
50  	private ObjectiveFunction objf;
51  
52  	/**
53       * 
54       */
55  	private static final long serialVersionUID = 1L;
56  
57  	protected PBSolverStats stats;
58  
59  	public PBSolver(LearningStrategy<PBDataStructureFactory> learner,
60  			PBDataStructureFactory dsf, IOrder order, RestartStrategy restarter) {
61  		super(learner, dsf, order, restarter);
62  		stats = new PBSolverStats();
63  		initStats(stats);
64  	}
65  
66  	public PBSolver(LearningStrategy<PBDataStructureFactory> learner,
67  			PBDataStructureFactory dsf, SearchParams params, IOrder order,
68  			RestartStrategy restarter) {
69  		super(learner, dsf, params, order, restarter);
70  		stats = new PBSolverStats();
71  		initStats(stats);
72  	}
73  
74  	public IConstr addPseudoBoolean(IVecInt literals, IVec<BigInteger> coeffs,
75  			boolean moreThan, BigInteger degree) throws ContradictionException {
76  		IVecInt vlits = dimacs2internal(literals);
77  		assert vlits.size() == literals.size();
78  		assert literals.size() == coeffs.size();
79  		return addConstr(dsfactory.createPseudoBooleanConstraint(vlits, coeffs,
80  				moreThan, degree));
81  	}
82  
83  	public void setObjectiveFunction(ObjectiveFunction obj) {
84  		objf = obj;
85  		IOrder order = getOrder();
86  		if (order instanceof IOrderObjective) {
87  			((IOrderObjective) order).setObjectiveFunction(obj);
88  		}
89  	}
90  
91  	public ObjectiveFunction getObjectiveFunction() {
92  		return objf;
93  	}
94  
95  	public IConstr addAtMost(IVecInt literals, IVecInt coeffs, int degree)
96  			throws ContradictionException {
97  		// TODO use direct encoding to int/long
98  		IVec<BigInteger> bcoeffs = new Vec<BigInteger>(coeffs.size());
99  		for (int i = 0; i < coeffs.size(); i++) {
100 			bcoeffs.push(BigInteger.valueOf(coeffs.get(i)));
101 		}
102 		return addAtMost(literals, bcoeffs, BigInteger.valueOf(degree));
103 	}
104 
105 	public IConstr addAtMost(IVecInt literals, IVec<BigInteger> coeffs,
106 			BigInteger degree) throws ContradictionException {
107 		IVecInt vlits = dimacs2internal(literals);
108 		assert vlits.size() == literals.size();
109 		assert literals.size() == coeffs.size();
110 		return addConstr(dsfactory.createPseudoBooleanConstraint(vlits, coeffs,
111 				false, degree));
112 	}
113 
114 	public IConstr addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
115 			throws ContradictionException {
116 		// TODO use direct encoding to int/long
117 		IVec<BigInteger> bcoeffs = new Vec<BigInteger>(coeffs.size());
118 		for (int i = 0; i < coeffs.size(); i++) {
119 			bcoeffs.push(BigInteger.valueOf(coeffs.get(i)));
120 		}
121 		return addAtLeast(literals, bcoeffs, BigInteger.valueOf(degree));
122 	}
123 
124 	public IConstr addAtLeast(IVecInt literals, IVec<BigInteger> coeffs,
125 			BigInteger degree) throws ContradictionException {
126 		IVecInt vlits = dimacs2internal(literals);
127 		assert vlits.size() == literals.size();
128 		assert literals.size() == coeffs.size();
129 		return addConstr(dsfactory.createPseudoBooleanConstraint(vlits, coeffs,
130 				true, degree));
131 	}
132 
133 	public IConstr addExactly(IVecInt literals, IVecInt coeffs, int weight)
134 			throws ContradictionException {
135 		// TODO use direct encoding to int/long
136 		IVec<BigInteger> bcoeffs = new Vec<BigInteger>(coeffs.size());
137 		for (int i = 0; i < coeffs.size(); i++) {
138 			bcoeffs.push(BigInteger.valueOf(coeffs.get(i)));
139 		}
140 		return addExactly(literals, bcoeffs, BigInteger.valueOf(weight));
141 	}
142 
143 	public IConstr addExactly(IVecInt literals, IVec<BigInteger> coeffs,
144 			BigInteger weight) throws ContradictionException {
145 		IVecInt vlits = dimacs2internal(literals);
146 		assert vlits.size() == literals.size();
147 		assert literals.size() == coeffs.size();
148 		ConstrGroup group = new ConstrGroup(false);
149 		group.add(addConstr(dsfactory.createPseudoBooleanConstraint(vlits,
150 				coeffs, false, weight)));
151 		group.add(addConstr(dsfactory.createPseudoBooleanConstraint(vlits,
152 				coeffs, true, weight)));
153 		return group;
154 	}
155 }