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.specs;
31  
32  /**
33   * Represents an optimization problem. The SAT solver will find suboptimal
34   * solutions of the problem until no more solutions are available. The latest
35   * solution found will be the optimal one.
36   * 
37   * Such kind of problem is supposed to be handled:
38   * 
39   * <pre>
40   * boolean isSatisfiable = false;
41   * 
42   * IOptimizationProblem optproblem = (IOptimizationProblem) problem;
43   * 
44   * try {
45   *     while (optproblem.admitABetterSolution()) {
46   *         if (!isSatisfiable) {
47   *             if (optproblem.nonOptimalMeansSatisfiable()) {
48   *                 setExitCode(ExitCode.SATISFIABLE);
49   *                 if (optproblem.hasNoObjectiveFunction()) {
50   *                     return;
51   *                 }
52   *                 log(&quot;SATISFIABLE&quot;); //$NON-NLS-1$
53   *             }
54   *             isSatisfiable = true;
55   *             log(&quot;OPTIMIZING...&quot;); //$NON-NLS-1$
56   *         }
57   *         log(&quot;Got one! Elapsed wall clock time (in seconds):&quot; //$NON-NLS-1$
58   *                 + (System.currentTimeMillis() - getBeginTime()) / 1000.0);
59   *         getLogWriter().println(
60   *                 CURRENT_OPTIMUM_VALUE_PREFIX + optproblem.getObjectiveValue());
61   *         optproblem.discardCurrentSolution();
62   *     }
63   *     if (isSatisfiable) {
64   *         setExitCode(ExitCode.OPTIMUM_FOUND);
65   *     } else {
66   *         setExitCode(ExitCode.UNSATISFIABLE);
67   *     }
68   * } catch (ContradictionException ex) {
69   *     assert isSatisfiable;
70   *     setExitCode(ExitCode.OPTIMUM_FOUND);
71   * }
72   * </pre>
73   * 
74   * @author leberre
75   * 
76   */
77  public interface IOptimizationProblem extends IProblem {
78  
79      /**
80       * Look for a solution of the optimization problem.
81       * 
82       * @return true if a better solution than current one can be found.
83       * @throws TimeoutException
84       *             if the solver cannot answer in reasonable time.
85       * @see ISolver#setTimeout(int)
86       */
87      boolean admitABetterSolution() throws TimeoutException;
88  
89      /**
90       * Look for a solution of the optimization problem when some literals are
91       * satisfied.
92       * 
93       * @param assumps
94       *            a set of literals in Dimacs format.
95       * @return true if a better solution than current one can be found.
96       * @throws TimeoutException
97       *             if the solver cannot answer in reasonable time.
98       * @see ISolver#setTimeout(int)
99       * @since 2.1
100      */
101     boolean admitABetterSolution(IVecInt assumps) throws TimeoutException;
102 
103     /**
104      * If the optimization problem has no objective function, then it is a
105      * simple decision problem.
106      * 
107      * @return true if the problem is a decision problem, false if the problem
108      *         is an optimization problem.
109      */
110     boolean hasNoObjectiveFunction();
111 
112     /**
113      * A suboptimal solution has different meaning depending of the optimization
114      * problem considered.
115      * 
116      * For instance, in the case of MAXSAT, a suboptimal solution does not mean
117      * that the problem is satisfiable, while in pseudo boolean optimization, it
118      * is true.
119      * 
120      * @return true if founding a suboptimal solution means that the problem is
121      *         satisfiable.
122      */
123     boolean nonOptimalMeansSatisfiable();
124 
125     /**
126      * Compute the value of the objective function for the current solution. A
127      * call to that method only makes sense if hasNoObjectiveFunction()==false.
128      * 
129      * DO NOT CALL THAT METHOD THAT WILL BE CALLED AUTOMATICALLY. USE
130      * getObjectiveValue() instead!
131      * 
132      * @return the value of the objective function.
133      * @see #getObjectiveValue()
134      */
135     @Deprecated
136     Number calculateObjective();
137 
138     /**
139      * Read only access to the value of the objective function for the current
140      * solution.
141      * 
142      * @return the value of the objective function for the current solution.
143      * @since 2.1
144      */
145     Number getObjectiveValue();
146 
147     /**
148      * Force the value of the objective function.
149      * 
150      * This is especially useful to iterate over optimal solutions.
151      * 
152      * @throws ContradictionException
153      * @since 2.1
154      */
155     void forceObjectiveValueTo(Number forcedValue)
156             throws ContradictionException;
157 
158     /**
159      * Discard the current solution in the optimization problem.
160      * 
161      * THE NAME WAS NOT NICE. STILL AVAILABLE TO AVOID BREAKING THE API. PLEASE
162      * USE THE LONGER discardCurrentSolution() instead.
163      * 
164      * @throws ContradictionException
165      *             if a trivial inconsistency is detected.
166      * @see #discardCurrentSolution()
167      */
168     @Deprecated
169     void discard() throws ContradictionException;
170 
171     /**
172      * Discard the current solution in the optimization problem.
173      * 
174      * @throws ContradictionException
175      *             if a trivial inconsistency is detected.
176      * @since 2.1
177      */
178     void discardCurrentSolution() throws ContradictionException;
179 
180     /**
181      * Allows to check afterwards if the solution provided by the solver is
182      * optimal or not.
183      * 
184      * @return
185      */
186     boolean isOptimal();
187 }