1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30 package org.sat4j.tools.xplain;
31
32 import java.util.ArrayList;
33 import java.util.Collection;
34 import java.util.Collections;
35 import java.util.HashMap;
36 import java.util.List;
37 import java.util.Map;
38
39 import org.sat4j.core.VecInt;
40 import org.sat4j.specs.ContradictionException;
41 import org.sat4j.specs.IConstr;
42 import org.sat4j.specs.ISolver;
43 import org.sat4j.specs.IVecInt;
44 import org.sat4j.specs.IteratorInt;
45 import org.sat4j.specs.TimeoutException;
46 import org.sat4j.tools.SolverDecorator;
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62 public class Xplain<T extends ISolver> extends SolverDecorator<T> implements
63 Explainer {
64
65 protected Map<Integer, IConstr> constrs = new HashMap<Integer, IConstr>();
66
67 protected IVecInt assump;
68
69 private int lastCreatedVar;
70 private boolean pooledVarId = false;
71 private final IVecInt lastClause = new VecInt();
72 private IConstr lastConstr;
73 private final boolean skipDuplicatedEntries;
74
75 private MinimizationStrategy xplainStrategy = new DeletionStrategy();
76
77 public Xplain(T solver, boolean skipDuplicatedEntries) {
78 super(solver);
79 this.skipDuplicatedEntries = skipDuplicatedEntries;
80 }
81
82 public Xplain(T solver) {
83 this(solver, true);
84 }
85
86 @Override
87 public IConstr addClause(IVecInt literals) throws ContradictionException {
88 if (this.skipDuplicatedEntries) {
89 if (literals.equals(this.lastClause)) {
90
91 return null;
92 }
93 this.lastClause.clear();
94 literals.copyTo(this.lastClause);
95 }
96 int newvar = createNewVar(literals);
97 literals.push(newvar);
98 this.lastConstr = super.addClause(literals);
99 if (this.lastConstr == null) {
100 discardLastestVar();
101 } else {
102 this.constrs.put(newvar, this.lastConstr);
103 }
104 return this.lastConstr;
105 }
106
107
108
109
110
111
112
113 protected int createNewVar(IVecInt literals) {
114 for (IteratorInt it = literals.iterator(); it.hasNext();) {
115 if (Math.abs(it.next()) > nextFreeVarId(false)) {
116 throw new IllegalStateException(
117 "Please call newVar(int) before adding constraints!!!");
118 }
119 }
120 if (this.pooledVarId) {
121 this.pooledVarId = false;
122 return this.lastCreatedVar;
123 }
124 this.lastCreatedVar = nextFreeVarId(true);
125 return this.lastCreatedVar;
126 }
127
128 protected void discardLastestVar() {
129 this.pooledVarId = true;
130 }
131
132 @Override
133 public IConstr addExactly(IVecInt literals, int n)
134 throws ContradictionException {
135 throw new UnsupportedOperationException(
136 "Explanation requires Pseudo Boolean support. See XplainPB class instead.");
137 }
138
139 @Override
140 public IConstr addAtLeast(IVecInt literals, int degree)
141 throws ContradictionException {
142 throw new UnsupportedOperationException(
143 "Explanation requires Pseudo Boolean support. See XplainPB class instead.");
144 }
145
146 @Override
147 public IConstr addAtMost(IVecInt literals, int degree)
148 throws ContradictionException {
149 throw new UnsupportedOperationException(
150 "Explanation requires Pseudo Boolean support. See XplainPB class instead.");
151 }
152
153
154
155
156 private static final long serialVersionUID = 1L;
157
158
159
160
161
162
163 private IVecInt explanationKeys() throws TimeoutException {
164 assert !isSatisfiable(this.assump);
165 ISolver solver = decorated();
166 if (solver instanceof SolverDecorator<?>) {
167 solver = ((SolverDecorator<? extends ISolver>) solver).decorated();
168 }
169 return this.xplainStrategy.explain(solver, this.constrs, this.assump);
170 }
171
172 public int[] minimalExplanation() throws TimeoutException {
173 IVecInt keys = explanationKeys();
174 keys.sort();
175 List<Integer> allKeys = new ArrayList<Integer>(this.constrs.keySet());
176 Collections.sort(allKeys);
177 int[] model = new int[keys.size()];
178 int i = 0;
179 for (IteratorInt it = keys.iterator(); it.hasNext();) {
180 model[i++] = allKeys.indexOf(it.next()) + 1;
181 }
182 return model;
183 }
184
185
186
187
188
189
190 public Collection<IConstr> explain() throws TimeoutException {
191 IVecInt keys = explanationKeys();
192 Collection<IConstr> explanation = new ArrayList<IConstr>(keys.size());
193 for (IteratorInt it = keys.iterator(); it.hasNext();) {
194 explanation.add(this.constrs.get(it.next()));
195 }
196 return explanation;
197 }
198
199
200
201
202 public void cancelExplanation() {
203 this.xplainStrategy.cancelExplanationComputation();
204 }
205
206
207
208
209
210 public Collection<IConstr> getConstraints() {
211 return this.constrs.values();
212 }
213
214 @Override
215 public int[] findModel() throws TimeoutException {
216 this.assump = VecInt.EMPTY;
217 IVecInt extraVariables = new VecInt();
218 for (Integer p : this.constrs.keySet()) {
219 extraVariables.push(-p);
220 }
221 return super.findModel(extraVariables);
222 }
223
224 @Override
225 public int[] findModel(IVecInt assumps) throws TimeoutException {
226 this.assump = assumps;
227 IVecInt extraVariables = new VecInt();
228 assumps.copyTo(extraVariables);
229 for (Integer p : this.constrs.keySet()) {
230 extraVariables.push(-p);
231 }
232 return super.findModel(extraVariables);
233 }
234
235 @Override
236 public boolean isSatisfiable() throws TimeoutException {
237 this.assump = VecInt.EMPTY;
238 IVecInt extraVariables = new VecInt();
239 for (Integer p : this.constrs.keySet()) {
240 extraVariables.push(-p);
241 }
242 return super.isSatisfiable(extraVariables);
243 }
244
245 @Override
246 public boolean isSatisfiable(boolean global) throws TimeoutException {
247 this.assump = VecInt.EMPTY;
248 IVecInt extraVariables = new VecInt();
249 for (Integer p : this.constrs.keySet()) {
250 extraVariables.push(-p);
251 }
252 return super.isSatisfiable(extraVariables, global);
253 }
254
255 @Override
256 public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
257 this.assump = assumps;
258 IVecInt extraVariables = new VecInt();
259 assumps.copyTo(extraVariables);
260 for (Integer p : this.constrs.keySet()) {
261 extraVariables.push(-p);
262 }
263 return super.isSatisfiable(extraVariables);
264 }
265
266 @Override
267 public boolean isSatisfiable(IVecInt assumps, boolean global)
268 throws TimeoutException {
269 this.assump = assumps;
270 IVecInt extraVariables = new VecInt();
271 assumps.copyTo(extraVariables);
272 for (Integer p : this.constrs.keySet()) {
273 extraVariables.push(-p);
274 }
275 return super.isSatisfiable(extraVariables, global);
276 }
277
278 @Override
279 public int[] model() {
280 int[] fullmodel = super.modelWithInternalVariables();
281 if (fullmodel == null) {
282 return null;
283 }
284 int[] model = new int[fullmodel.length - this.constrs.size()];
285 int j = 0;
286 for (int element : fullmodel) {
287 if (this.constrs.get(Math.abs(element)) == null) {
288 model[j++] = element;
289 }
290 }
291 return model;
292 }
293
294 @Override
295 public String toString(String prefix) {
296 System.out.println(prefix + "Explanation (MUS) enabled solver");
297 System.out.println(prefix + this.xplainStrategy);
298 return super.toString(prefix);
299 }
300
301 public void setMinimizationStrategy(MinimizationStrategy strategy) {
302 this.xplainStrategy = strategy;
303 }
304
305 @Override
306 public boolean removeConstr(IConstr c) {
307 if (this.lastConstr == c) {
308 this.lastClause.clear();
309 this.lastConstr = null;
310 }
311 return super.removeConstr(c);
312 }
313
314 @Override
315 public boolean removeSubsumedConstr(IConstr c) {
316 if (this.lastConstr == c) {
317 this.lastClause.clear();
318 this.lastConstr = null;
319 }
320 return super.removeSubsumedConstr(c);
321 }
322
323 }