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.tools;
29  
30  import org.sat4j.specs.ContradictionException;
31  import org.sat4j.specs.IOptimizationProblem;
32  import org.sat4j.specs.ISolver;
33  import org.sat4j.specs.IVecInt;
34  import org.sat4j.specs.TimeoutException;
35  
36  public class OptToSatAdapter extends SolverDecorator<ISolver> {
37  
38  	/**
39       * 
40       */
41  	private static final long serialVersionUID = 1L;
42  
43  	IOptimizationProblem problem;
44  
45  	boolean modelComputed = false;
46  	boolean optimalValueForced = false;
47  
48  	public OptToSatAdapter(IOptimizationProblem problem) {
49  		super((ISolver) problem);
50  		this.problem = problem;
51  	}
52  
53  	@Override
54  	public boolean isSatisfiable() throws TimeoutException {
55  		modelComputed = false;
56  		return problem.admitABetterSolution();
57  	}
58  
59  	@Override
60  	public void reset() {
61  		super.reset();
62  		optimalValueForced = false;
63  	}
64  
65  	@Override
66  	public boolean isSatisfiable(boolean global) throws TimeoutException {
67  		modelComputed = false;
68  		return problem.admitABetterSolution();
69  	}
70  
71  	@Override
72  	public boolean isSatisfiable(IVecInt assumps, boolean global)
73  			throws TimeoutException {
74  		throw new UnsupportedOperationException();
75  	}
76  
77  	@Override
78  	public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
79  		throw new UnsupportedOperationException();
80  	}
81  
82  	@Override
83  	public int[] model() {
84  		if (modelComputed)
85  			return problem.model();
86  
87  		try {
88  			assert problem.admitABetterSolution();
89  			do {
90  				problem.discardCurrentSolution();
91  			} while (problem.admitABetterSolution());
92  			if (!optimalValueForced) {
93  				try {
94  					problem.forceObjectiveValueTo(problem.getObjectiveValue());
95  				} catch (ContradictionException e1) {
96  					throw new IllegalStateException();
97  				}
98  				optimalValueForced = true;
99  			}
100 		} catch (TimeoutException e) {
101 			// solver timeout
102 		} catch (ContradictionException e) {
103 			// OK, optimal model found
104 			if (!optimalValueForced) {
105 				try {
106 					problem.forceObjectiveValueTo(problem.getObjectiveValue());
107 				} catch (ContradictionException e1) {
108 					throw new IllegalStateException();
109 				}
110 				optimalValueForced = true;
111 			}
112 		}
113 		modelComputed = true;
114 		return problem.model();
115 	}
116 
117 	@Override
118 	public boolean model(int var) {
119 		if (!modelComputed)
120 			model();
121 		return problem.model(var);
122 	}
123 
124 	@Override
125 	public String toString(String prefix) {
126 		return prefix + "Optimization to SAT adapter\n"
127 				+ super.toString(prefix);
128 	}
129 }