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.opt;
29  
30  import org.sat4j.core.VecInt;
31  import org.sat4j.specs.ContradictionException;
32  import org.sat4j.specs.IConstr;
33  import org.sat4j.specs.IOptimizationProblem;
34  import org.sat4j.specs.ISolver;
35  import org.sat4j.specs.IVecInt;
36  import org.sat4j.specs.TimeoutException;
37  import org.sat4j.tools.SolverDecorator;
38  
39  /**
40   * Computes a solution with the smallest number of satisfied literals.
41   * 
42   * Please make sure that newVar(howmany) is called first to setup the decorator.
43   * 
44   * @author leberre
45   */
46  public final class MinOneDecorator extends SolverDecorator<ISolver> implements
47  		IOptimizationProblem {
48  
49  	/**
50       * 
51       */
52  	private static final long serialVersionUID = 1L;
53  
54  	private int[] prevmodel;
55  
56  	public MinOneDecorator(ISolver solver) {
57  		super(solver);
58  	}
59  
60  	public boolean admitABetterSolution() throws TimeoutException {
61  		return admitABetterSolution(VecInt.EMPTY);
62  	}
63  
64  	/**
65  	 * @since 2.1
66  	 */
67  	public boolean admitABetterSolution(IVecInt assumps)
68  			throws TimeoutException {
69  		boolean result = isSatisfiable(assumps, true);
70  		if (result) {
71  			prevmodel = super.model();
72  			calculateObjectiveValue();
73  		}
74  		return result;
75  	}
76  
77  	public boolean hasNoObjectiveFunction() {
78  		return false;
79  	}
80  
81  	public boolean nonOptimalMeansSatisfiable() {
82  		return true;
83  	}
84  
85  	private int counter;
86  
87  	public Number calculateObjective() {
88  		calculateObjectiveValue();
89  		return counter;
90  	}
91  
92  	private void calculateObjectiveValue() {
93  		counter = 0;
94  		for (int p : prevmodel) {
95  			if (p > 0) {
96  				counter++;
97  			}
98  		}
99  	}
100 
101 	private final IVecInt literals = new VecInt();
102 
103 	private IConstr previousConstr;
104 
105 	/**
106 	 * @since 2.1
107 	 */
108 	public void discardCurrentSolution() throws ContradictionException {
109 		if (literals.isEmpty()) {
110 			for (int i = 1; i <= nVars(); i++) {
111 				literals.push(i);
112 			}
113 		}
114 		if (previousConstr != null) {
115 			super.removeConstr(previousConstr);
116 		}
117 		previousConstr = addAtMost(literals, counter - 1);
118 	}
119 
120 	@Override
121 	public int[] model() {
122 		// DLB findbugs ok
123 		return prevmodel;
124 	}
125 
126 	@Override
127 	public void reset() {
128 		literals.clear();
129 		previousConstr = null;
130 		super.reset();
131 	}
132 
133 	/**
134 	 * @since 2.1
135 	 */
136 	public Number getObjectiveValue() {
137 		return counter;
138 	}
139 
140 	public void discard() throws ContradictionException {
141 		discardCurrentSolution();
142 	}
143 
144 	/**
145 	 * @since 2.1
146 	 */
147 	public void forceObjectiveValueTo(Number forcedValue)
148 			throws ContradictionException {
149 		addAtMost(literals, forcedValue.intValue());
150 
151 	}
152 }