View Javadoc

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