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  
20  package org.sat4j.pb;
21  
22  import static org.junit.Assert.assertEquals;
23  import static org.junit.Assert.assertFalse;
24  import static org.junit.Assert.assertTrue;
25  import static org.sat4j.pb.tools.WeightedObject.newWO;
26  
27  import java.util.ArrayList;
28  import java.util.Arrays;
29  import java.util.Iterator;
30  import java.util.List;
31  import java.util.Set;
32  
33  import org.junit.Before;
34  import org.junit.Test;
35  import org.sat4j.pb.tools.DependencyHelper;
36  import org.sat4j.pb.tools.StringNegator;
37  import org.sat4j.pb.tools.WeightedObject;
38  import org.sat4j.specs.ContradictionException;
39  import org.sat4j.specs.IVec;
40  import org.sat4j.specs.TimeoutException;
41  
42  public class TestDependencyHelper {
43  	private static final String profile = "profile";
44  	private static final String junit3 = "junit_3";
45  	private static final String junit4 = "junit_4";
46  
47  	private DependencyHelper<String, String> helper;
48  
49  	@Before
50  	public void setUp() {
51  		helper = new DependencyHelper<String, String>(SolverFactory
52  				.newEclipseP2());
53  		// helper = new
54  		// DependencyHelper<String,String>(SolverFactory.newDefault(),10);
55  	}
56  
57  	@Test
58  	public void testBasicRequirements() throws ContradictionException,
59  			TimeoutException {
60  		helper.implication("A").implies("B").and("C").and("D").named("I1");
61  		helper.implication("B").impliesNot("C").named("I2");
62  		helper.setTrue("A", "User selection");
63  		assertFalse(helper.hasASolution());
64  		// assertEquals("C",helper.getConflictingElement());
65  		Set<String> cause = helper.why();
66  		assertEquals(3, cause.size());
67  		Iterator<String> it = cause.iterator();
68  		assertEquals("I1", it.next());
69  		assertTrue(it.hasNext());
70  		assertEquals("I2", it.next());
71  		assertTrue(it.hasNext());
72  		assertEquals("User selection", it.next());
73  	}
74  
75  	@Test
76  	public void testBasicRequirementsDetailedExplanation()
77  			throws ContradictionException, TimeoutException {
78  		helper.implication("A").implies("B").named("I1b");
79  		helper.implication("A").implies("C").named("I1c");
80  		helper.implication("A").implies("D").named("I1d");
81  		helper.implication("B").impliesNot("C").named("I2");
82  		helper.setTrue("A", "User selection");
83  		assertFalse(helper.hasASolution());
84  		// assertEquals("C",helper.getConflictingElement());
85  		Set<String> cause = helper.why();
86  		assertEquals(4, cause.size());
87  		Iterator<String> it = cause.iterator();
88  		assertEquals("I1b", it.next());
89  		assertEquals("I1c", it.next());
90  		assertEquals("I2", it.next());
91  		assertEquals("User selection", it.next());
92  	}
93  
94  	@Test
95  	public void testDisjunctions() throws ContradictionException,
96  			TimeoutException {
97  		helper.implication("A").implies("B").and("C").and("D").named("I1");
98  		helper.implication("C").implies("C1", "C2", "C3").named("C versions");
99  		helper.atMost(1, "C1", "C2", "C3").named("Singleton on C");
100 		helper.setTrue("A", "User selection");
101 		assertTrue(helper.hasASolution());
102 		IVec<String> solution = helper.getSolution();
103 		assertTrue(solution.contains("A"));
104 		assertTrue(solution.contains("B"));
105 		assertTrue(solution.contains("C"));
106 		assertTrue(solution.contains("D"));
107 		if (solution.contains("C1")) {
108 			assertFalse(solution.contains("C2"));
109 			assertFalse(solution.contains("C3"));
110 		}
111 		if (solution.contains("C2")) {
112 			assertFalse(solution.contains("C1"));
113 			assertFalse(solution.contains("C3"));
114 		}
115 		if (solution.contains("C3")) {
116 			assertFalse(solution.contains("C1"));
117 			assertFalse(solution.contains("C2"));
118 		}
119 	}
120 
121 	@Test
122 	public void testDisjunctionExplanation() throws ContradictionException,
123 			TimeoutException {
124 		helper.implication("A").implies("B").and("C").and("D").named("I1");
125 		helper.implication("B").impliesNot("C1").named("I2");
126 		helper.implication("D").impliesNot("C2").named("I3");
127 		helper.implication("C").implies("C1", "C2").named("C versions");
128 		helper.atMost(1, "C1", "C2", "C3").named("Singleton on C");
129 		helper.setTrue("A", "User selection");
130 		assertFalse(helper.hasASolution());
131 		// assertTrue(helper.getConflictingElement().startsWith("C"));
132 		Set<String> cause = helper.why();
133 		assertEquals(5, cause.size());
134 		Iterator<String> it = cause.iterator();
135 		assertEquals("C versions", it.next());
136 		assertEquals("I1", it.next());
137 		assertEquals("I2", it.next());
138 		assertEquals("I3", it.next());
139 		assertEquals("User selection", it.next());
140 	}
141 
142 	@Test
143 	public void testExplanationForASolution() throws ContradictionException,
144 			TimeoutException {
145 		helper.implication("A").implies("B").and("C").and("D").named("I1");
146 		helper.implication("C").implies("C1", "C2", "C3").named("C versions");
147 		helper.atMost(1, "C1", "C2", "C3").named("Singleton on C");
148 		helper.setTrue("A", "User selection");
149 		assertTrue(helper.hasASolution());
150 		IVec<String> solution = helper.getSolution();
151 		assertTrue(solution.contains("A"));
152 		assertTrue(solution.contains("B"));
153 		assertTrue(solution.contains("C"));
154 		assertTrue(solution.contains("D"));
155 		Set<String> cause = helper.why("D");
156 		assertEquals(2, cause.size());
157 		Iterator<String> it = cause.iterator();
158 		assertEquals("I1", it.next());
159 		assertEquals("User selection", it.next());
160 	}
161 
162 	@Test
163 	public void testObjectiveFunction() throws ContradictionException,
164 			TimeoutException {
165 		helper.implication("A").implies("B").and("C").and("D").named("I1");
166 		helper.implication("C").implies("C1", "C2", "C3").named("C versions");
167 		helper.atMost(1, "C1", "C2", "C3").named("Singleton on C");
168 		helper.setTrue("A", "User selection");
169 		helper.setObjectiveFunction(newWO("C1", 4), newWO("C2", 2), newWO("C3",
170 				1));
171 		assertTrue(helper.hasASolution());
172 		IVec<String> solution = helper.getSolution();
173 		assertTrue(solution.contains("A"));
174 		assertTrue(solution.contains("B"));
175 		assertTrue(solution.contains("C"));
176 		assertTrue(solution.contains("C3"));
177 		assertFalse(solution.contains("C2"));
178 		assertFalse(solution.contains("C1"));
179 		assertTrue(solution.contains("D"));
180 	}
181 
182 	@Test
183 	public void testJunitExample() throws ContradictionException,
184 			TimeoutException {
185 		helper.implication(profile).implies(junit3).named("profile->junit_3");
186 		helper.implication(profile).implies(junit4).named("profile->junit_4");
187 		helper.setObjectiveFunction(WeightedObject.newWO(junit4, 1),
188 				WeightedObject.newWO(junit3, 2));
189 		helper.setTrue(profile, "profile must exist");
190 		assertTrue(helper.hasASolution());
191 		List<String> expected = new ArrayList<String>(Arrays.asList(profile,
192 				junit3, junit4));
193 		IVec<String> solution = helper.getSolution();
194 		for (Iterator<String> i = solution.iterator(); i.hasNext();) {
195 			String variable = i.next();
196 			assertTrue(variable + " was not part of the solution", expected
197 					.remove(variable));
198 		}
199 		assertTrue("solution contained too many variables: " + expected,
200 				expected.isEmpty());
201 	}
202 
203 	@Test
204 	public void testJunitSingletonObjectiveExample()
205 			throws ContradictionException, TimeoutException {
206 		helper.implication(profile).implies(junit3, junit4).named(
207 				"profile->junit");
208 		helper.atMost(1, junit4, junit3);
209 		helper.setObjectiveFunction(WeightedObject.newWO(junit4, 1),
210 				WeightedObject.newWO(junit3, 2));
211 		helper.setTrue(profile, "profile must exist");
212 		assertTrue(helper.hasASolution());
213 		List<String> expected = new ArrayList<String>(Arrays.asList(profile,
214 				junit4));
215 		IVec<String> solution = helper.getSolution();
216 		for (Iterator<String> i = solution.iterator(); i.hasNext();) {
217 			String variable = i.next();
218 			assertTrue(variable + " was not part of the solution", expected
219 					.remove(variable));
220 		}
221 		assertTrue("solution contained too many variables: " + expected,
222 				expected.isEmpty());
223 	}
224 
225 	@Test
226 	public void testEquivalency() throws ContradictionException,
227 			TimeoutException {
228 		helper.implication("A").implies("B").named("C1");
229 		helper.iff("C2", "B", "C");
230 		helper.setTrue("A", "C3");
231 		assertTrue(helper.hasASolution());
232 		helper.setFalse("C", "C4");
233 		assertFalse(helper.hasASolution());
234 	}
235 
236 	@Test
237 	public void testDisjunction() throws ContradictionException,
238 			TimeoutException {
239 		// A or B -> C or D
240 		helper.disjunction("A", "B").implies("C", "D").named("C1");
241 		// -> A or B ( equivalent to A or B )
242 		helper.implication().implies("A", "B").named("C2");
243 		helper.setFalse("C", "C3");
244 		assertTrue(helper.hasASolution());
245 		helper.setFalse("D", "C4");
246 		assertFalse(helper.hasASolution());
247 
248 	}
249 
250 	@Test
251 	public void testCathyExamples() throws ContradictionException,
252 			TimeoutException {
253 		helper.setNegator(StringNegator.instance);
254 		// A <=> B and C and D
255 		helper.and("C1", "A", "B", "C", "D");
256 		// not A or B implies E
257 		helper.implication("-A", "B").implies("E").named("C2");
258 		helper.setFalse("D", "InitState");
259 		helper.setTrue("B", "InitState");
260 		helper.setFalse("E", "InitState");
261 		helper.atMost(1, "A", "B", "C", "D", "E").named("C5");
262 		assertFalse(helper.hasASolution());
263 		assertEquals(3, helper.why().size());
264 	}
265 }