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.maxsat;
31  
32  import java.math.BigInteger;
33  
34  import org.sat4j.core.Vec;
35  import org.sat4j.core.VecInt;
36  import org.sat4j.pb.IPBSolver;
37  import org.sat4j.pb.PBSolverDecorator;
38  import org.sat4j.specs.ContradictionException;
39  import org.sat4j.specs.IConstr;
40  import org.sat4j.specs.IOptimizationProblem;
41  import org.sat4j.specs.IVec;
42  import org.sat4j.specs.IVecInt;
43  import org.sat4j.specs.TimeoutException;
44  
45  /**
46   * A decorator that computes minimal cost models. That problem is also known as
47   * binate covering problem.
48   * 
49   * Please make sure that newVar(howmany) is called first to setup the decorator.
50   * 
51   * @author daniel
52   * 
53   */
54  public class MinCostDecorator extends PBSolverDecorator implements
55          IOptimizationProblem {
56  
57      /**
58       * 
59       */
60      private static final long serialVersionUID = 1L;
61  
62      private int[] costs;
63  
64      private int[] prevmodel;
65  
66      private final IVecInt vars = new VecInt();
67  
68      private final IVec<BigInteger> coeffs = new Vec<BigInteger>();
69  
70      private int objectivevalue;
71  
72      private IConstr prevConstr;
73  
74      private boolean isSolutionOptimal;
75  
76      public MinCostDecorator(IPBSolver solver) {
77          super(solver);
78      }
79  
80      /*
81       * (non-Javadoc)
82       * 
83       * @see org.sat4j.tools.SolverDecorator#newVar()
84       */
85      @Override
86      public int newVar() {
87          throw new UnsupportedOperationException();
88      }
89  
90      /**
91       * Setup the number of variables to use inside the solver.
92       * 
93       * It is mandatory to call that method before setting the cost of the
94       * variables.
95       * 
96       * @param howmany
97       *            the maximum number of variables in the solver.
98       */
99      @Override
100     public int newVar(int howmany) {
101         this.costs = new int[howmany + 1];
102         // Arrays.fill(costs, 1);
103         this.vars.clear();
104         this.coeffs.clear();
105         for (int i = 1; i <= howmany; i++) {
106             this.vars.push(i);
107             this.coeffs.push(BigInteger.ZERO);
108         }
109         // should the default cost be 1????
110         // here it is 0
111         return super.newVar(howmany);
112     }
113 
114     /**
115      * to know the cost of a given var.
116      * 
117      * @param var
118      *            a variable in dimacs format
119      * @return the cost of that variable when assigned to true
120      */
121     public int costOf(int var) {
122         return this.costs[var];
123     }
124 
125     /**
126      * to set the cost of a given var.
127      * 
128      * @param var
129      *            a variable in dimacs format
130      * @param cost
131      *            the cost of var when assigned to true
132      */
133     public void setCost(int var, int cost) {
134         this.costs[var] = cost;
135         this.coeffs.set(var - 1, BigInteger.valueOf(cost));
136     }
137 
138     public boolean admitABetterSolution() throws TimeoutException {
139         return admitABetterSolution(VecInt.EMPTY);
140     }
141 
142     public boolean admitABetterSolution(IVecInt assumps)
143             throws TimeoutException {
144         this.isSolutionOptimal = false;
145         boolean result = super.isSatisfiable(assumps, true);
146         if (result) {
147             this.prevmodel = super.model();
148             calculateObjective();
149         } else {
150             this.isSolutionOptimal = true;
151         }
152         return result;
153     }
154 
155     public boolean hasNoObjectiveFunction() {
156         return false;
157     }
158 
159     public boolean nonOptimalMeansSatisfiable() {
160         return true;
161     }
162 
163     public Number calculateObjective() {
164         this.objectivevalue = calculateDegree(this.prevmodel);
165         return this.objectivevalue;
166     }
167 
168     private int calculateDegree(int[] prevmodel2) {
169         int tmpcost = 0;
170         for (int i = 1; i < this.costs.length; i++) {
171             if (prevmodel2[i - 1] > 0) {
172                 tmpcost += this.costs[i];
173             }
174         }
175         return tmpcost;
176     }
177 
178     public void discardCurrentSolution() throws ContradictionException {
179         if (this.prevConstr != null) {
180             super.removeSubsumedConstr(this.prevConstr);
181         }
182         try {
183             this.prevConstr = super.addPseudoBoolean(this.vars, this.coeffs,
184                     false, BigInteger.valueOf(this.objectivevalue - 1));
185         } catch (ContradictionException e) {
186             this.isSolutionOptimal = true;
187             throw e;
188         }
189     }
190 
191     @Override
192     public void reset() {
193         this.prevConstr = null;
194         super.reset();
195     }
196 
197     @Override
198     public int[] model() {
199         // DLB findbugs ok
200         return this.prevmodel;
201     }
202 
203     public Number getObjectiveValue() {
204         return this.objectivevalue;
205     }
206 
207     public void discard() throws ContradictionException {
208         discardCurrentSolution();
209     }
210 
211     public void forceObjectiveValueTo(Number forcedValue)
212             throws ContradictionException {
213         super.addPseudoBoolean(this.vars, this.coeffs, false,
214                 (BigInteger) forcedValue);
215     }
216 
217     public boolean isOptimal() {
218         return this.isSolutionOptimal;
219     }
220 
221     public void setTimeoutForFindingBetterSolution(int seconds) {
222         // TODO
223         throw new UnsupportedOperationException("No implemented yet");
224     }
225 }