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  		System.out.flush();
66  		PrintWriter out = getLogWriter();
67  		out.flush();
68  		solver.printStat(out, COMMENT_PREFIX);
69  		solver.printInfos(out, COMMENT_PREFIX);
70  		ExitCode exitCode = getExitCode();
71  		out.println(ANSWER_PREFIX + exitCode);
72  		if (exitCode == ExitCode.SATISFIABLE
73  				|| exitCode == ExitCode.OPTIMUM_FOUND) {
74  			out.print(SOLUTION_PREFIX);
75  			getReader().decode(solver.model(), out);
76  			out.println();
77  			IOptimizationProblem optproblem = (IOptimizationProblem) solver;
78  			if (!optproblem.hasNoObjectiveFunction()) {
79  				log("objective function=" + optproblem.getObjectiveValue()); //$NON-NLS-1$
80  			}
81  		}
82  	}
83  
84  	@Override
85  	protected void solve(IProblem problem) throws TimeoutException {
86  		boolean isSatisfiable = false;
87  
88  		IOptimizationProblem optproblem = (IOptimizationProblem) problem;
89  
90  		try {
91  			while (optproblem.admitABetterSolution()) {
92  				if (!isSatisfiable) {
93  					if (optproblem.nonOptimalMeansSatisfiable()) {
94  						setExitCode(ExitCode.SATISFIABLE);
95  						if (optproblem.hasNoObjectiveFunction()) {
96  							return;
97  						}
98  						log("SATISFIABLE"); //$NON-NLS-1$
99  					}
100 					isSatisfiable = true;
101 					log("OPTIMIZING..."); //$NON-NLS-1$
102 				}
103 				log("Got one! Elapsed wall clock time (in seconds):" //$NON-NLS-1$
104 						+ (System.currentTimeMillis() - getBeginTime())
105 						/ 1000.0);
106 				getLogWriter().println(
107 						CURRENT_OPTIMUM_VALUE_PREFIX
108 								+ optproblem.getObjectiveValue());
109 				optproblem.discardCurrentSolution();
110 			}
111 			if (isSatisfiable) {
112 				setExitCode(ExitCode.OPTIMUM_FOUND);
113 			} else {
114 				setExitCode(ExitCode.UNSATISFIABLE);
115 			}
116 		} catch (ContradictionException ex) {
117 			assert isSatisfiable;
118 			setExitCode(ExitCode.OPTIMUM_FOUND);
119 		}
120 	}
121 
122 }