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.math.BigInteger;
33  
34  import org.sat4j.core.VecInt;
35  import org.sat4j.specs.ContradictionException;
36  import org.sat4j.specs.IConstr;
37  import org.sat4j.specs.IOptimizationProblem;
38  import org.sat4j.specs.IVecInt;
39  import org.sat4j.specs.TimeoutException;
40  
41  /**
42   * A decorator that computes minimal pseudo boolean models.
43   * 
44   * @author daniel
45   * 
46   */
47  public class PseudoOptDecorator extends PBSolverDecorator implements
48          IOptimizationProblem {
49  
50      /**
51       * 
52       */
53      private static final long serialVersionUID = 1L;
54  
55      private BigInteger objectiveValue;
56  
57      private int[] prevmodel;
58      private int[] prevmodelwithadditionalvars;
59  
60      private boolean[] prevfullmodel;
61  
62      private IConstr previousPBConstr;
63  
64      private boolean isSolutionOptimal;
65  
66      private final boolean nonOptimalMeansSatisfiable;
67  
68      private final boolean useAnImplicantForEvaluation;
69  
70      private int solverTimeout = Integer.MAX_VALUE;
71  
72      private int optimizationTimeout = -1;
73  
74      /**
75       * Create a PB decorator for which a non optimal solution means that the
76       * problem is satisfiable.
77       * 
78       * @param solver
79       *            a PB solver.
80       */
81      public PseudoOptDecorator(IPBSolver solver) {
82          this(solver, true);
83      }
84  
85      /**
86       * Create a PB decorator with a specific semantic of non optimal solution.
87       * 
88       * @param solver
89       *            a PB solver
90       * @param nonOptimalMeansSatisfiable
91       *            true if a suboptimal solution means that the problem is
92       *            satisfiable (e.g. as in the PB competition), else false (e.g.
93       *            as in the MAXSAT competition).
94       */
95      public PseudoOptDecorator(IPBSolver solver,
96              boolean nonOptimalMeansSatisfiable) {
97          this(solver, nonOptimalMeansSatisfiable, false);
98      }
99  
100     /**
101      * Create a PB decorator with a specific semantic of non optimal solution.
102      * 
103      * @param solver
104      *            a PB solver
105      * @param nonOptimalMeansSatisfiable
106      *            true if a suboptimal solution means that the problem is
107      *            satisfiable (e.g. as in the PB competition), else false (e.g.
108      *            as in the MAXSAT competition).
109      * @param useAnImplicantForEvaluation
110      *            uses an implicant (a prime implicant computed using
111      *            {@link #primeImplicant()}) instead of a plain model to
112      *            evaluate the objective function.
113      */
114     public PseudoOptDecorator(IPBSolver solver,
115             boolean nonOptimalMeansSatisfiable,
116             boolean useAnImplicantForEvaluation) {
117         super(solver);
118         this.nonOptimalMeansSatisfiable = nonOptimalMeansSatisfiable;
119         this.useAnImplicantForEvaluation = useAnImplicantForEvaluation;
120     }
121 
122     @Override
123     public boolean isSatisfiable() throws TimeoutException {
124         return isSatisfiable(VecInt.EMPTY);
125     }
126 
127     @Override
128     public boolean isSatisfiable(boolean global) throws TimeoutException {
129         return isSatisfiable(VecInt.EMPTY, global);
130     }
131 
132     @Override
133     public boolean isSatisfiable(IVecInt assumps, boolean global)
134             throws TimeoutException {
135         boolean result = super.isSatisfiable(assumps, true);
136         if (result) {
137             this.prevmodel = super.model();
138             this.prevmodelwithadditionalvars = super
139                     .modelWithInternalVariables();
140             this.prevfullmodel = new boolean[nVars()];
141             for (int i = 0; i < nVars(); i++) {
142                 this.prevfullmodel[i] = decorated().model(i + 1);
143             }
144             if (optimizationTimeout > 0) {
145                 super.expireTimeout();
146                 super.setTimeout(optimizationTimeout);
147             }
148 
149         } else {
150             if (this.previousPBConstr != null) {
151                 decorated().removeConstr(this.previousPBConstr);
152                 this.previousPBConstr = null;
153             }
154             super.setTimeout(solverTimeout);
155         }
156         return result;
157     }
158 
159     @Override
160     public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
161         return isSatisfiable(assumps, true);
162     }
163 
164     @Override
165     public void setObjectiveFunction(ObjectiveFunction objf) {
166         decorated().setObjectiveFunction(objf);
167     }
168 
169     public boolean admitABetterSolution() throws TimeoutException {
170         return admitABetterSolution(VecInt.EMPTY);
171     }
172 
173     public boolean admitABetterSolution(IVecInt assumps)
174             throws TimeoutException {
175         try {
176             this.isSolutionOptimal = false;
177             boolean result = super.isSatisfiable(assumps, true);
178             if (result) {
179                 if (this.useAnImplicantForEvaluation) {
180                     this.prevmodel = modelWithAdaptedNonPrimeLiterals();
181 
182                 } else {
183                     this.prevmodel = super.model();
184                 }
185                 this.prevmodelwithadditionalvars = super
186                         .modelWithInternalVariables();
187                 this.prevfullmodel = new boolean[nVars()];
188                 for (int i = 0; i < nVars(); i++) {
189                     this.prevfullmodel[i] = decorated().model(i + 1);
190                 }
191                 if (decorated().getObjectiveFunction() != null) {
192                     calculateObjective();
193                 }
194                 if (optimizationTimeout > 0) {
195                     super.expireTimeout();
196                     super.setTimeout(optimizationTimeout);
197                 }
198             } else {
199                 this.isSolutionOptimal = true;
200                 if (this.previousPBConstr != null) {
201                     decorated().removeConstr(this.previousPBConstr);
202                     this.previousPBConstr = null;
203                 }
204             }
205             return result;
206         } catch (TimeoutException te) {
207             if (this.previousPBConstr != null) {
208                 decorated().removeConstr(this.previousPBConstr);
209                 this.previousPBConstr = null;
210             }
211             throw te;
212         }
213     }
214 
215     private int[] modelWithAdaptedNonPrimeLiterals() {
216         // do not use model() because it might contain holes.
217         int[] completeModel = new int[nVars()];
218         int var;
219         for (int i = 0; i < nVars(); i++) {
220             var = i + 1;
221             completeModel[i] = super.model(var) ? var : -var;
222         }
223         primeImplicant();
224         ObjectiveFunction obj = getObjectiveFunction();
225         for (int i = 0; i < obj.getVars().size(); i++) {
226             int d = obj.getVars().get(i);
227             BigInteger coeff = obj.getCoeffs().get(i);
228             if (d <= nVars() && !primeImplicant(d) && !primeImplicant(-d)) {
229                 // the variable does not appear in the model: it can be assigned
230                 // either way
231                 assert Math.abs(completeModel[Math.abs(d) - 1]) == d;
232                 if (coeff.signum() * d < 0) {
233                     completeModel[Math.abs(d) - 1] = Math.abs(d);
234                 } else {
235                     completeModel[Math.abs(d) - 1] = -Math.abs(d);
236                 }
237             }
238         }
239         return completeModel;
240     }
241 
242     public boolean hasNoObjectiveFunction() {
243         return decorated().getObjectiveFunction() == null;
244     }
245 
246     public boolean nonOptimalMeansSatisfiable() {
247         return nonOptimalMeansSatisfiable;
248     }
249 
250     public Number calculateObjective() {
251         if (decorated().getObjectiveFunction() == null) {
252             throw new UnsupportedOperationException(
253                     "The problem does not contain an objective function");
254         }
255         if (this.useAnImplicantForEvaluation) {
256             this.objectiveValue = decorated().getObjectiveFunction()
257                     .calculateDegreeImplicant(decorated());
258         } else {
259             this.objectiveValue = decorated().getObjectiveFunction()
260                     .calculateDegree(decorated());
261         }
262         return getObjectiveValue();
263     }
264 
265     public void discardCurrentSolution() throws ContradictionException {
266         if (this.previousPBConstr != null) {
267             super.removeSubsumedConstr(this.previousPBConstr);
268         }
269         if (decorated().getObjectiveFunction() != null
270                 && this.objectiveValue != null) {
271             this.previousPBConstr = super.addPseudoBoolean(decorated()
272                     .getObjectiveFunction().getVars(), decorated()
273                     .getObjectiveFunction().getCoeffs(), false,
274                     this.objectiveValue.subtract(BigInteger.ONE));
275         }
276     }
277 
278     @Override
279     public void reset() {
280         this.previousPBConstr = null;
281         super.reset();
282     }
283 
284     @Override
285     public int[] model() {
286         // DLB findbugs ok
287         return this.prevmodel;
288     }
289 
290     @Override
291     public boolean model(int var) {
292         return this.prevfullmodel[var - 1];
293     }
294 
295     @Override
296     public String toString(String prefix) {
297         return prefix
298                 + "Pseudo Boolean Optimization by upper bound\n"
299                 + prefix
300                 + (useAnImplicantForEvaluation ? "using prime implicants for evaluating the objective function\n"
301                         : "") + super.toString(prefix);
302     }
303 
304     public Number getObjectiveValue() {
305         return this.objectiveValue.add(decorated().getObjectiveFunction()
306                 .getCorrection());
307     }
308 
309     public void discard() throws ContradictionException {
310         discardCurrentSolution();
311     }
312 
313     public void forceObjectiveValueTo(Number forcedValue)
314             throws ContradictionException {
315         super.addPseudoBoolean(decorated().getObjectiveFunction().getVars(),
316                 decorated().getObjectiveFunction().getCoeffs(), false,
317                 (BigInteger) forcedValue);
318     }
319 
320     public boolean isOptimal() {
321         return this.isSolutionOptimal;
322     }
323 
324     @Override
325     public int[] modelWithInternalVariables() {
326         return this.prevmodelwithadditionalvars;
327     }
328 
329     public void setTimeoutForFindingBetterSolution(int seconds) {
330         optimizationTimeout = seconds;
331     }
332 
333     @Override
334     public void setTimeout(int t) {
335         solverTimeout = t;
336         super.setTimeout(t);
337     }
338 }