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  
29  package org.sat4j;
30  
31  import static org.junit.Assert.assertEquals;
32  import static org.junit.Assert.assertFalse;
33  import static org.junit.Assert.assertTrue;
34  import static org.junit.Assert.fail;
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.ISolver;
41  import org.sat4j.specs.IVecInt;
42  import org.sat4j.specs.TimeoutException;
43  import org.sat4j.tools.Minimal4CardinalityModel;
44  import org.sat4j.tools.Minimal4InclusionModel;
45  import org.sat4j.tools.ModelIterator;
46  import org.sat4j.tools.SolutionCounter;
47  
48  /**
49   * @author leberre
50   * 
51   *         To change the template for this generated type comment go to
52   *         Window>Preferences>Java>Code Generation>Code and Comments
53   */
54  public class ModelIteratorTest {
55  
56  	@Test
57  	public void testModelIterator() {
58  		try {
59  			ISolver solver = new ModelIterator(SolverFactory.newDefault());
60  			solver.newVar(3);
61  			IVecInt clause = new VecInt();
62  			clause.push(1);
63  			clause.push(2);
64  			clause.push(3);
65  			solver.addClause(clause);
66  			clause.clear();
67  			clause.push(-1);
68  			clause.push(-2);
69  			clause.push(-3);
70  			solver.addClause(clause);
71  			int counter = 0;
72  			while (solver.isSatisfiable()) {
73  				solver.model();
74  				counter++;
75  			}
76  			assertEquals(6, counter);
77  		} catch (ContradictionException e) {
78  			fail();
79  		} catch (TimeoutException e) {
80  			fail();
81  		}
82  	}
83  
84  	// Is not Implemented Yet. We need a Backup/Restore solution to do so.
85  	// public void testIncMinModel() {
86  	// try {
87  	// ISolver solver = new ModelIterator(new
88  	// Minimal4InclusionModel(SolverFactory.newMiniLearning()));
89  	// solver.newVar(3);
90  	// VecInt clause = new VecInt();
91  	// clause.push(1);
92  	// clause.push(2);
93  	// clause.push(3);
94  	// solver.addClause(clause);
95  	// clause.clear();
96  	// clause.push(-1);
97  	// clause.push(-2);
98  	// clause.push(-3);
99  	// solver.addClause(clause);
100 	// int counter = 0;
101 	// while (solver.isSatisfiable()) {
102 	// int[] model = solver.model();
103 	// counter++;
104 	// }
105 	// assertEquals(3, counter);
106 	// } catch (ContradictionException e) {
107 	// fail();
108 	// } catch (TimeoutException e) {
109 	// fail();
110 	// }
111 	// }
112 	//    
113 	// public void testCardMinModel() {
114 	// try {
115 	// ISolver solver = new ModelIterator(new
116 	// Minimal4CardinalityModel(SolverFactory.newMiniLearning()));
117 	// solver.newVar(3);
118 	// VecInt clause = new VecInt();
119 	// clause.push(1);
120 	// clause.push(2);
121 	// clause.push(3);
122 	// solver.addClause(clause);
123 	// clause.clear();
124 	// clause.push(-1);
125 	// clause.push(-2);
126 	// clause.push(-3);
127 	// solver.addClause(clause);
128 	// int counter = 0;
129 	// while (solver.isSatisfiable()) {
130 	// int[] model = solver.model();
131 	// counter++;
132 	// }
133 	// assertEquals(3, counter);
134 	// } catch (ContradictionException e) {
135 	// fail();
136 	// } catch (TimeoutException e) {
137 	// fail();
138 	// }
139 	// }
140 
141 	@Test
142 	public void testCardModel() {
143 		try {
144 			ISolver solver = new Minimal4CardinalityModel(SolverFactory
145 					.newDefault());
146 			solver.newVar(3);
147 			IVecInt clause = new VecInt();
148 			clause.push(1);
149 			clause.push(-2);
150 			clause.push(3);
151 			solver.addClause(clause);
152 			clause.clear();
153 			clause.push(-1);
154 			clause.push(2);
155 			clause.push(-3);
156 			solver.addClause(clause);
157 			int counter = 0;
158 			while (solver.isSatisfiable() && (counter < 10)) {
159 				solver.model();
160 				counter++;
161 			}
162 			assertEquals(10, counter);
163 		} catch (ContradictionException e) {
164 			fail();
165 		} catch (TimeoutException e) {
166 			fail();
167 		}
168 	}
169 
170 	@Test
171 	public void testIncModel() {
172 		try {
173 			ISolver solver = new Minimal4InclusionModel(SolverFactory
174 					.newDefault());
175 			solver.newVar(3);
176 			IVecInt clause = new VecInt();
177 			clause.push(1);
178 			clause.push(-2);
179 			clause.push(3);
180 			solver.addClause(clause);
181 			clause.clear();
182 			clause.push(-1);
183 			clause.push(2);
184 			clause.push(-3);
185 			solver.addClause(clause);
186 			int counter = 0;
187 			while (solver.isSatisfiable() && (counter < 10)) {
188 				solver.model();
189 				counter++;
190 			}
191 			assertEquals(10, counter);
192 		} catch (ContradictionException e) {
193 			fail();
194 		} catch (TimeoutException e) {
195 			fail();
196 		}
197 	}
198 
199 	@Test
200 	public void testIsSatisfiableVecInt() {
201 		try {
202 			ISolver solver = SolverFactory.newDefault();
203 			solver.newVar(3);
204 			IVecInt clause = new VecInt();
205 			clause.push(1);
206 			clause.push(2);
207 			clause.push(3);
208 			solver.addClause(clause);
209 			clause.clear();
210 			clause.push(-1);
211 			clause.push(-2);
212 			clause.push(-3);
213 			solver.addClause(clause);
214 			assertTrue(solver.isSatisfiable());
215 			IVecInt cube = new VecInt();
216 			cube.push(1);
217 			assertTrue(solver.isSatisfiable(cube));
218 			// printModel(solver.model());
219 			cube.push(2);
220 			assertEquals(2, cube.size());
221 			assertTrue(solver.isSatisfiable(cube));
222 			// printModel(solver.model());
223 			cube.push(-3);
224 			assertEquals(3, cube.size());
225 			assertTrue(solver.isSatisfiable(cube));
226 			// printModel(solver.model());
227 			cube.pop();
228 			cube.push(3);
229 			assertEquals(3, cube.size());
230 			// System.out.println(" cube " + cube);
231 			boolean sat = solver.isSatisfiable(cube);
232 			// if (sat) {
233 			// printModel(solver.model());
234 			// }
235 			assertFalse(sat);
236 		} catch (ContradictionException e) {
237 			fail();
238 		} catch (TimeoutException e) {
239 			fail();
240 		}
241 	}
242 
243 	@Test(timeout = 5000)
244 	public void testGlobalTimeoutCounter() {
245 		SolutionCounter counter = new SolutionCounter(SolverFactory
246 				.newDefault());
247 		IVecInt clause = new VecInt();
248 		for (int i = 1; i < 100; i++) {
249 			clause.push(i);
250 		}
251 		try {
252 			counter.addClause(clause);
253 			counter.setTimeout(3);
254 			counter.countSolutions();
255 		} catch (TimeoutException e) {
256 			assertTrue(counter.lowerBound() > 0);
257 		} catch (ContradictionException e) {
258 			fail();
259 		}
260 	}
261 	
262 	@Test(timeout = 5000)
263 	public void testGlobalTimeoutIterator() {
264 		ModelIterator iterator = new ModelIterator(SolverFactory
265 				.newDefault());
266 		IVecInt clause = new VecInt();
267 		for (int i = 1; i < 100; i++) {
268 			clause.push(i);
269 		}
270 		try {
271 			iterator.addClause(clause);
272 			iterator.setTimeout(3);
273 			while (iterator.isSatisfiable()) {
274 				iterator.model();
275 			}
276 		} catch (TimeoutException e) {
277 
278 		} catch (ContradictionException e) {
279 			fail();
280 		}
281 	}
282 	
283 
284 	@Test(timeout = 11000)
285 	public void testSpecificValues() throws ContradictionException, TimeoutException {
286 		assertEquals(3L,count(2));
287 		assertEquals(7L,count(3));
288 		assertEquals(15L,count(4));
289 		assertEquals(31L,count(5));
290 		assertEquals(63L,count(6));
291 		assertEquals(127L,count(7));
292 		assertEquals(255L,count(8));
293 		assertEquals(511L,count(9));
294 	}
295 
296 	private long count(int size) throws ContradictionException,
297 			TimeoutException {
298 		SolutionCounter counter = new SolutionCounter(SolverFactory
299 				.newDefault());
300 		IVecInt clause = new VecInt();
301 		for (int i = 1; i <= size; i++) {
302 			clause.push(i);
303 		}
304 		counter.addClause(clause);
305 		counter.setTimeout(10);
306 		return counter.countSolutions();
307 	}
308 }