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.xplain;
29  
30  import java.util.ArrayList;
31  import java.util.Collections;
32  import java.util.List;
33  import java.util.Map;
34  
35  import org.sat4j.core.VecInt;
36  import org.sat4j.specs.IConstr;
37  import org.sat4j.specs.ISolver;
38  import org.sat4j.specs.IVecInt;
39  import org.sat4j.specs.TimeoutException;
40  
41  /**
42   * 
43   * @author daniel
44   * @since 2.1
45   */
46  public class ReplayXplainStrategy implements XplainStrategy {
47  
48  	private boolean computationCanceled;
49  
50  	/**
51  	 * @since 2.1
52  	 */
53  	public void cancelExplanationComputation() {
54  		computationCanceled = true;
55  	}
56  
57  	/**
58  	 * @since 2.1
59  	 */
60  	public IVecInt explain(ISolver solver, Map<Integer, IConstr> constrs,
61  			IVecInt assumps) throws TimeoutException {
62  		computationCanceled = false;
63  		IVecInt encodingAssumptions = new VecInt(constrs.size()
64  				+ assumps.size());
65  		List<Pair> pairs = new ArrayList<Pair>(constrs.size());
66  		IConstr constr;
67  		for (Map.Entry<Integer, IConstr> entry : constrs.entrySet()) {
68  			constr = entry.getValue();
69  			pairs.add(new Pair(entry.getKey(), constr));
70  		}
71  		Collections.sort(pairs);
72  
73  		assumps.copyTo(encodingAssumptions);
74  		// for (Integer p : constrsIds) {
75  		// encodingAssumptions.push(p);
76  		// }
77  		for (Pair p : pairs) {
78  			encodingAssumptions.push(p.key);
79  		}
80  
81  		boolean shouldContinue;
82  		int startingPoint = assumps.size();
83  		do {
84  			shouldContinue = false;
85  			int i = startingPoint;
86  			encodingAssumptions.set(i, -encodingAssumptions.get(i));
87  			assert encodingAssumptions.get(i) < 0;
88  			while (!computationCanceled
89  					&& solver.isSatisfiable(encodingAssumptions)) {
90  				i++;
91  				assert encodingAssumptions.get(i) > 0;
92  				encodingAssumptions.set(i, -encodingAssumptions.get(i));
93  			}
94  			if (!computationCanceled && i > startingPoint) {
95  				assert !solver.isSatisfiable(encodingAssumptions);
96  				if (i < encodingAssumptions.size()) {
97  					// latest constraint is for sure responsible for the
98  					// inconsistency.
99  					int tmp = encodingAssumptions.get(i);
100 					for (int j = i; j > startingPoint; j--) {
101 						encodingAssumptions.set(j, -encodingAssumptions
102 								.get(j - 1));
103 					}
104 					encodingAssumptions.set(startingPoint, tmp);
105 				}
106 				shouldContinue = true;
107 			}
108 			startingPoint++;
109 		} while (!computationCanceled && shouldContinue
110 				&& solver.isSatisfiable(encodingAssumptions));
111 		if (computationCanceled) {
112 			throw new TimeoutException();
113 		}
114 		IVecInt constrsKeys = new VecInt(startingPoint);
115 		for (int i = assumps.size(); i < startingPoint; i++) {
116 			constrsKeys.push(-encodingAssumptions.get(i));
117 		}
118 		return constrsKeys;
119 	}
120 }