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;
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 }