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 pseudo boolean algorithms described in:
20   * A fast pseudo-Boolean constraint solver Chai, D.; Kuehlmann, A.
21   * Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on
22   * Volume 24, Issue 3, March 2005 Page(s): 305 - 317
23   * 
24   * and 
25   * Heidi E. Dixon, 2004. Automating Pseudo-Boolean Inference within a DPLL 
26   * Framework. Ph.D. Dissertation, University of Oregon.
27   *******************************************************************************/
28  package org.sat4j.pb;
29  
30  import org.sat4j.core.VecInt;
31  import org.sat4j.specs.ContradictionException;
32  import org.sat4j.specs.IOptimizationProblem;
33  import org.sat4j.specs.IVecInt;
34  import org.sat4j.specs.TimeoutException;
35  
36  /**
37   * Utility class to use optimization solvers instead of simple SAT solvers in
38   * code meant for SAT solvers.
39   * 
40   * @author daniel
41   */
42  public class OptToPBSATAdapter extends PBSolverDecorator {
43  
44  	/**
45       * 
46       */
47  	private static final long serialVersionUID = 1L;
48  
49  	IOptimizationProblem problem;
50  
51  	boolean modelComputed = false;
52  
53  	private IVecInt assumps = new VecInt();
54  	
55  	public OptToPBSATAdapter(IOptimizationProblem problem) {
56  		super((IPBSolver) problem);
57  		this.problem = problem;
58  	}
59  
60  	@Override
61  	public boolean isSatisfiable() throws TimeoutException {
62  		modelComputed = false;
63  		assumps.clear();
64          if (problem.hasNoObjectiveFunction()) {
65      		return modelComputed = problem.isSatisfiable();
66      	}
67  		return problem.admitABetterSolution();
68  	}
69  
70  	@Override
71  	public boolean isSatisfiable(boolean global) throws TimeoutException {
72  		return isSatisfiable();
73  	}
74  
75  	@Override
76  	public boolean isSatisfiable(IVecInt assumps, boolean global)
77  			throws TimeoutException {
78  		return isSatisfiable(assumps);
79  	}
80  
81  	@Override
82  	public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
83  		modelComputed = false;
84  		this.assumps.clear();
85  		assumps.copyTo(this.assumps);
86      	if (problem.hasNoObjectiveFunction()) {
87      		return modelComputed = problem.isSatisfiable(assumps);
88      	}
89  		return problem.admitABetterSolution(assumps);
90  	}
91  
92  	@Override
93  	public int[] model() {
94  		if (modelComputed)
95  			return problem.model();
96  		try {
97  			assert problem.admitABetterSolution(assumps);
98              assert !problem.hasNoObjectiveFunction();
99   			do {
100 				problem.discardCurrentSolution();
101 			} while (problem.admitABetterSolution(assumps));
102 		} catch (TimeoutException e) {
103 			// solver timeout
104 		} catch (ContradictionException e) {
105 			// OK, optimal model found
106 		}
107 		modelComputed = true;
108 		return problem.model();
109 	}
110 
111 	@Override
112 	public boolean model(int var) {
113 		if (!modelComputed)
114 			model();
115 		return problem.model(var);
116 	}
117 
118 	@Override
119 	public String toString(String prefix) {
120 		return prefix + "Optimization to Pseudo Boolean adapter\n"
121 				+ super.toString(prefix);
122 	}
123 }