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  package org.sat4j;
26  
27  import java.io.PrintWriter;
28  
29  import org.sat4j.specs.ContradictionException;
30  import org.sat4j.specs.IOptimizationProblem;
31  import org.sat4j.specs.IProblem;
32  import org.sat4j.specs.TimeoutException;
33  
34  /**
35   * This class is intended to be used by launchers to solve optimization
36   * problems, i.e. problems for which a loop is needed to find the optimal
37   * solution.
38   * 
39   * @author leberre
40   * 
41   */
42  @SuppressWarnings("PMD")
43  public abstract class AbstractOptimizationLauncher extends AbstractLauncher {
44  
45      private static final String CURRENT_OPTIMUM_VALUE_PREFIX = "o "; //$NON-NLS-1$
46  
47      @Override
48      protected void displayResult() {
49          if (solver == null)
50              return;
51          PrintWriter out = getLogWriter();
52          solver.printStat(out, COMMENT_PREFIX);
53          ExitCode exitCode = getExitCode();
54          out.println(ANSWER_PREFIX + exitCode);
55          if (exitCode == ExitCode.SATISFIABLE
56                  || exitCode == ExitCode.OPTIMUM_FOUND) {
57              out.print(SOLUTION_PREFIX);
58              getReader().decode(solver.model(), out);
59              out.println();
60              IOptimizationProblem optproblem = (IOptimizationProblem) solver;
61              if (!optproblem.hasNoObjectiveFunction()) {
62                  log("objective function=" + optproblem.calculateObjective()); //$NON-NLS-1$
63              }
64  
65          }
66          log("Total wall clock time (ms): " //$NON-NLS-1$
67                  + (System.currentTimeMillis() - getBeginTime()) / 1000.0);
68      }
69  
70      @Override
71      protected void solve(IProblem problem) throws TimeoutException {
72          boolean isSatisfiable = false;
73  
74          IOptimizationProblem optproblem = (IOptimizationProblem) problem;
75  
76          try {
77              while (optproblem.admitABetterSolution()) {
78                  if (!isSatisfiable) {
79                      if (optproblem.nonOptimalMeansSatisfiable()) {
80                          setExitCode(ExitCode.SATISFIABLE);
81                          if (optproblem.hasNoObjectiveFunction()) {
82                              return;
83                          }
84                          log("SATISFIABLE"); //$NON-NLS-1$
85                      }
86                      isSatisfiable = true;
87                      log("OPTIMIZING..."); //$NON-NLS-1$
88                  }
89                  log("Got one! Elapsed wall clock time (in seconds):" //$NON-NLS-1$
90                          + (System.currentTimeMillis() - getBeginTime())
91                          / 1000.0);
92                  getLogWriter().println(
93                          CURRENT_OPTIMUM_VALUE_PREFIX
94                                  + optproblem.calculateObjective());
95                  optproblem.discard();
96              }
97              if (isSatisfiable) {
98                  setExitCode(ExitCode.OPTIMUM_FOUND);
99              } else {
100                 setExitCode(ExitCode.UNSATISFIABLE);
101             }
102         } catch (ContradictionException ex) {
103             assert isSatisfiable;
104             setExitCode(ExitCode.OPTIMUM_FOUND);
105         }
106     }
107 
108 }