View Javadoc

1   /*
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le Berre
3    * 
4    * Based on the original minisat specification from:
5    * 
6    * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the
7    * Sixth International Conference on Theory and Applications of Satisfiability
8    * Testing, LNCS 2919, pp 502-518, 2003.
9    * 
10   * This library is free software; you can redistribute it and/or modify it under
11   * the terms of the GNU Lesser General Public License as published by the Free
12   * Software Foundation; either version 2.1 of the License, or (at your option)
13   * any later version.
14   * 
15   * This library is distributed in the hope that it will be useful, but WITHOUT
16   * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
17   * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
18   * details.
19   * 
20   * You should have received a copy of the GNU Lesser General Public License
21   * along with this library; if not, write to the Free Software Foundation, Inc.,
22   * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
23   * 
24   */
25  
26  package org.sat4j.opt;
27  
28  import java.math.BigInteger;
29  
30  import org.sat4j.core.Vec;
31  import org.sat4j.core.VecInt;
32  import org.sat4j.specs.ContradictionException;
33  import org.sat4j.specs.IOptimizationProblem;
34  import org.sat4j.specs.ISolver;
35  import org.sat4j.specs.IVec;
36  import org.sat4j.specs.IVecInt;
37  import org.sat4j.specs.TimeoutException;
38  import org.sat4j.tools.SolverDecorator;
39  
40  /**
41   * A decorator that computes minimal cost models.
42   * 
43   * Please make sure that newVar(howmany) is called first to setup the decorator.
44   * 
45   * @author daniel
46   *
47   */
48  public class MinCostDecorator extends SolverDecorator implements
49          IOptimizationProblem {
50  
51      /**
52       * 
53       */
54      private static final long serialVersionUID = 1L;
55  
56      private int[] costs;
57  
58      private int[] prevmodel;
59  
60      private final IVecInt vars = new VecInt();
61  
62      private final IVec<BigInteger> coeffs = new Vec<BigInteger>();
63  
64      public MinCostDecorator(ISolver solver) {
65          super(solver);
66      }
67  
68      /*
69       * (non-Javadoc)
70       * 
71       * @see org.sat4j.tools.SolverDecorator#newVar()
72       */
73      @Override
74      public int newVar() {
75          throw new UnsupportedOperationException();
76      }
77  
78      /**
79       * Setup the number of variables to use inside the solver.
80       * 
81       * It is mandatory to call that method before setting the cost of the
82       * variables.
83       * 
84       * @param howmany
85       *            the maximum number of variables in the solver.
86       */
87      @Override
88      public int newVar(int howmany) {
89          costs = new int[howmany + 1];
90          // Arrays.fill(costs, 1);
91          vars.clear();
92          coeffs.clear();
93          for (int i = 1; i <= howmany; i++) {
94              vars.push(i);
95              coeffs.push(BigInteger.ZERO);
96          }
97          // should the default cost be 1????
98          // here it is 0
99          return super.newVar(howmany);
100     }
101 
102     /**
103      * to know the cost of a given var.
104      * 
105      * @param var
106      *            a variable in dimacs format
107      * @return the cost of that variable when assigned to true
108      */
109     public int costOf(int var) {
110         return costs[var];
111     }
112 
113     /**
114      * to set the cost of a given var.
115      * 
116      * @param var
117      *            a variable in dimacs format
118      * @param cost
119      *            the cost of var when assigned to true
120      */
121     public void setCost(int var, int cost) {
122         costs[var] = cost;
123         coeffs.set(var - 1, BigInteger.valueOf(cost));
124     }
125 
126     public boolean admitABetterSolution() throws TimeoutException {
127         boolean result = super.isSatisfiable();
128         if (result)
129             prevmodel = super.model();
130         return result;
131     }
132 
133     public boolean hasNoObjectiveFunction() {
134         return false;
135     }
136 
137     public boolean nonOptimalMeansSatisfiable() {
138         return true;
139     }
140 
141     public Number calculateObjective() {
142         return calculateDegree(prevmodel);
143     }
144 
145     private int calculateDegree(int[] prevmodel2) {
146         int tmpcost = 0;
147         for (int i = 1; i < costs.length; i++) {
148             if (prevmodel2[i - 1] > 0) {
149                 tmpcost += costs[i];
150             }
151         }
152         return tmpcost;
153     }
154 
155     public void discard() throws ContradictionException {
156         super.addPseudoBoolean(vars, coeffs, false, BigInteger
157                 .valueOf(calculateDegree(prevmodel) - 1));
158     }
159 
160     @Override
161     public int[] model() {
162         // DLB findbugs ok
163         return prevmodel;
164     }
165 
166 }