View Javadoc

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 }