1 /*******************************************************************************
2 * SAT4J: a SATisfiability library for Java Copyright (C) 2004, 2012 Artois University and CNRS
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 original MiniSat specification from:
20 *
21 * An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
22 * Sixth International Conference on Theory and Applications of Satisfiability
23 * Testing, LNCS 2919, pp 502-518, 2003.
24 *
25 * See www.minisat.se for the original solver in C++.
26 *
27 * Contributors:
28 * CRIL - initial API and implementation
29 *******************************************************************************/
30 package org.sat4j.pb;
31
32 import java.io.Serializable;
33 import java.math.BigInteger;
34
35 import org.sat4j.core.ReadOnlyVec;
36 import org.sat4j.core.ReadOnlyVecInt;
37 import org.sat4j.specs.ISolver;
38 import org.sat4j.specs.IVec;
39 import org.sat4j.specs.IVecInt;
40 import org.sat4j.specs.RandomAccessModel;
41
42 /**
43 * Abstraction for an Objective Function for Pseudo Boolean Optimization.
44 *
45 * May be generalized in the future to deal with other optimization functions.
46 *
47 * @author leberre
48 *
49 */
50 public class ObjectiveFunction implements Serializable {
51
52 /**
53 *
54 */
55 private static final long serialVersionUID = 1L;
56
57 // contains the coeffs of the objective function for each variable
58 private final IVec<BigInteger> coeffs;
59
60 private final IVecInt vars;
61
62 private BigInteger correction = BigInteger.ZERO;
63
64 public ObjectiveFunction(IVecInt vars, IVec<BigInteger> coeffs) {
65 this.vars = new ReadOnlyVecInt(vars);
66 this.coeffs = new ReadOnlyVec<BigInteger>(coeffs);
67 }
68
69 /**
70 * Compute the degree of the objective function using a full model.
71 *
72 * @param lazyModel
73 * a solver that recently answered true to isSatisfiable()
74 * @return the value of the objective function for the last model found be
75 * the solver.
76 */
77 public BigInteger calculateDegree(RandomAccessModel lazyModel) {
78 BigInteger tempDegree = BigInteger.ZERO;
79 for (int i = 0; i < this.vars.size(); i++) {
80 BigInteger coeff = this.coeffs.get(i);
81 if (varInModel(this.vars.get(i), lazyModel)) {
82 tempDegree = tempDegree.add(coeff);
83 } else if (coeff.signum() < 0
84 && !varInModel(-this.vars.get(i), lazyModel)) {
85 // the variable does not appear in the model: it can be assigned
86 // either way
87 tempDegree = tempDegree.add(coeff);
88 }
89 }
90 return tempDegree;
91 }
92
93 /**
94 * Compute the degree of the objective function using a prime implicant. It
95 * is expected that the method IProblem.primeImplicant() has been called
96 * before calling that method.
97 *
98 * @param solver
99 * a solver which recently answered true to isSatisfiable and on
100 * which the method primeImplicant() has been called.
101 * @return
102 * @see org.sat4j.specs.IProblem#primeImplicant()
103 */
104 public BigInteger calculateDegreeImplicant(ISolver solver) {
105 BigInteger tempDegree = BigInteger.ZERO;
106 for (int i = 0; i < this.vars.size(); i++) {
107 BigInteger coeff = this.coeffs.get(i);
108 if (solver.primeImplicant(this.vars.get(i))) {
109 tempDegree = tempDegree.add(coeff);
110 } else if (coeff.signum() < 0
111 && !solver.primeImplicant(-this.vars.get(i))) {
112 // the variable does not appear in the model: it can be assigned
113 // either way
114 tempDegree = tempDegree.add(coeff);
115 }
116 }
117 return tempDegree;
118 }
119
120 private boolean varInModel(int var, RandomAccessModel lazyModel) {
121 if (var > 0) {
122 return lazyModel.model(var);
123 }
124 return !lazyModel.model(-var);
125 }
126
127 public IVec<BigInteger> getCoeffs() {
128 return this.coeffs;
129 }
130
131 public IVecInt getVars() {
132 return this.vars;
133 }
134
135 public void setCorrection(BigInteger correction) {
136 this.correction = correction;
137 }
138
139 public BigInteger getCorrection() {
140 return this.correction;
141 }
142
143 @Override
144 public String toString() {
145 StringBuffer stb = new StringBuffer();
146 IVecInt lits = getVars();
147 IVec<BigInteger> coefs = getCoeffs();
148 BigInteger coef;
149 int lit;
150 for (int i = 0; i < lits.size(); i++) {
151 coef = coefs.get(i);
152 lit = lits.get(i);
153 if (lit < 0) {
154 lit = -lit;
155 coef = coef.negate();
156 }
157 stb.append((coef.signum() < 0 ? "" : "+") + coef + " x" + lit + " ");
158 }
159 return stb.toString();
160 }
161
162 public BigInteger minValue() {
163 BigInteger tempDegree = BigInteger.ZERO;
164 for (int i = 0; i < this.vars.size(); i++) {
165 BigInteger coeff = this.coeffs.get(i);
166 if (coeff.signum() < 0) {
167 tempDegree = tempDegree.add(coeff);
168 }
169 }
170 return tempDegree;
171 }
172
173 @Override
174 public int hashCode() {
175 return this.coeffs.hashCode() / 3 + this.vars.hashCode() / 3
176 + this.correction.hashCode() / 3;
177 }
178
179 @Override
180 public boolean equals(Object obj) {
181 if (obj instanceof ObjectiveFunction) {
182 ObjectiveFunction of = (ObjectiveFunction) obj;
183 return of.correction.equals(this.correction)
184 && of.coeffs.equals(this.coeffs)
185 && of.vars.equals(this.vars);
186 }
187 return false;
188 }
189 }