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 package org.sat4j;
29
30 import static org.junit.Assert.assertEquals;
31 import static org.junit.Assert.assertFalse;
32 import static org.junit.Assert.assertTrue;
33
34 import java.util.Collection;
35
36 import org.junit.Test;
37 import org.sat4j.core.VecInt;
38 import org.sat4j.minisat.SolverFactory;
39 import org.sat4j.specs.ContradictionException;
40 import org.sat4j.specs.IConstr;
41 import org.sat4j.specs.ISolver;
42 import org.sat4j.specs.IVecInt;
43 import org.sat4j.specs.TimeoutException;
44 import org.sat4j.tools.xplain.Xplain;
45
46 public class TestQuickExplain {
47
48 @Test
49 public void testGlobalInconsistency() throws ContradictionException, TimeoutException {
50 Xplain<ISolver> solver = new Xplain<ISolver>(SolverFactory.newDefault());
51 solver.newVar(2);
52 IVecInt clause = new VecInt();
53 clause.push(1).push(2);
54 solver.addClause(clause);
55 clause.clear();
56 clause.push(1).push(-2);
57 solver.addClause(clause);
58 clause.clear();
59 clause.push(-1).push(2);
60 solver.addClause(clause);
61 clause.clear();
62 clause.push(-1).push(-2);
63 solver.addClause(clause);
64 clause.clear();
65 assertFalse(solver.isSatisfiable());
66 Collection<IConstr> explanation = solver.explain();
67 assertEquals(4,explanation.size());
68 }
69
70 @Test
71 public void testAlmostGlobalInconsistency() throws ContradictionException, TimeoutException {
72 Xplain<ISolver> solver = new Xplain<ISolver>(SolverFactory.newDefault());
73 solver.newVar(3);
74 IVecInt clause = new VecInt();
75 clause.push(1).push(2);
76 IConstr c1 = solver.addClause(clause);
77 clause.clear();
78 clause.push(1).push(-2);
79 IConstr c2 = solver.addClause(clause);
80 clause.clear();
81 clause.push(-1).push(2);
82 IConstr c3 = solver.addClause(clause);
83 clause.clear();
84 clause.push(-1).push(-2);
85 IConstr c4 = solver.addClause(clause);
86 clause.clear();
87 clause.push(1).push(3);
88 solver.addClause(clause);
89 clause.clear();
90 assertFalse(solver.isSatisfiable());
91 Collection<IConstr> explanation = solver.explain();
92 assertEquals(4,explanation.size());
93 assertTrue(explanation.contains(c1));
94 assertTrue(explanation.contains(c2));
95 assertTrue(explanation.contains(c3));
96 assertTrue(explanation.contains(c4));
97 }
98
99 @Test
100 public void testAlmostGlobalInconsistencyII() throws ContradictionException, TimeoutException {
101 Xplain<ISolver> solver = new Xplain<ISolver>(SolverFactory.newDefault());
102 solver.newVar(3);
103 IVecInt clause = new VecInt();
104 clause.push(1).push(2);
105 IConstr c1 = solver.addClause(clause);
106 clause.clear();
107 clause.push(1).push(-2);
108 IConstr c2 = solver.addClause(clause);
109 clause.clear();
110 clause.push(1).push(3);
111 solver.addClause(clause);
112 clause.clear();
113 clause.push(-1).push(2);
114 IConstr c4 = solver.addClause(clause);
115 clause.clear();
116 clause.push(-1).push(-2);
117 IConstr c5 = solver.addClause(clause);
118 clause.clear();
119 assertFalse(solver.isSatisfiable());
120 Collection<IConstr> explanation = solver.explain();
121 assertEquals(4,explanation.size());
122 assertTrue(explanation.contains(c1));
123 assertTrue(explanation.contains(c2));
124 assertTrue(explanation.contains(c4));
125 assertTrue(explanation.contains(c5));
126 }
127
128 @Test
129 public void testTheCaseOfTwoMUSes() throws ContradictionException, TimeoutException {
130 Xplain<ISolver> solver = new Xplain<ISolver>(SolverFactory.newDefault());
131 solver.newVar(4);
132 IVecInt clause = new VecInt();
133 clause.push(1).push(2);
134 IConstr c1 = solver.addClause(clause);
135 clause.clear();
136 clause.push(1).push(-2);
137 IConstr c2 = solver.addClause(clause);
138 clause.clear();
139 clause.push(-1).push(3);
140 solver.addClause(clause);
141 clause.clear();
142 clause.push(-1).push(-3);
143 solver.addClause(clause);
144 clause.clear();
145 clause.push(-1).push(4);
146 solver.addClause(clause);
147 clause.clear();
148 clause.push(-1).push(-4);
149 solver.addClause(clause);
150 clause.clear();
151 assertFalse(solver.isSatisfiable());
152 Collection<IConstr> explanation = solver.explain();
153 assertEquals(4,explanation.size());
154 assertTrue(explanation.contains(c1));
155 assertTrue(explanation.contains(c2));
156 }
157
158 @Test
159 public void testEclipseTestCase() throws ContradictionException, TimeoutException {
160 Xplain<ISolver> solver = new Xplain<ISolver>(SolverFactory.newDefault());
161 solver.newVar(3);
162 IVecInt clause = new VecInt();
163 clause.push(-1);
164 solver.addClause(clause);
165 clause.clear();
166 clause.push(-2).push(3);
167 solver.addClause(clause);
168 clause.clear();
169 clause.push(-2).push(1);
170 solver.addClause(clause);
171 clause.clear();
172 clause.push(2);
173 solver.addClause(clause);
174 clause.clear();
175 assertFalse(solver.isSatisfiable());
176 Collection<IConstr> explanation = solver.explain();
177 assertEquals(3,explanation.size());
178 }
179
180 @Test
181 public void testEclipseTestCase2() throws ContradictionException, TimeoutException {
182 Xplain<ISolver> solver = new Xplain<ISolver>(SolverFactory.newDefault());
183 solver.newVar(4);
184 IVecInt clause = new VecInt();
185 clause.push(-1).push(2);
186 solver.addClause(clause);
187 clause.clear();
188 clause.push(-1).push(3);
189 solver.addClause(clause);
190 clause.clear();
191 clause.push(-2).push(-3);
192 solver.addClause(clause);
193 clause.clear();
194 clause.push(-4).push(1);
195 solver.addClause(clause);
196 clause.clear();
197 IVecInt assump = new VecInt();
198 assump.push(4);
199 assertFalse(solver.isSatisfiable(assump));
200 Collection<IConstr> explanation = solver.explain();
201 assertEquals(4,explanation.size());
202 }
203 }