1 package org.sat4j;
2
3 import static org.junit.Assert.assertNotNull;
4 import static org.junit.Assert.assertNull;
5 import static org.junit.Assert.assertTrue;
6
7 import java.util.HashSet;
8 import java.util.Set;
9
10 import org.junit.Before;
11 import org.junit.Test;
12 import org.sat4j.core.VecInt;
13 import org.sat4j.minisat.SolverFactory;
14 import org.sat4j.specs.ContradictionException;
15 import org.sat4j.specs.TimeoutException;
16 import org.sat4j.tools.GateTranslator;
17
18 public class BugSAT81 {
19
20 private GateTranslator solver;
21
22
23
24
25 @Before
26 public void setUp() throws Exception {
27 solver = new GateTranslator(SolverFactory.newDefault());
28 }
29
30 @Test
31 public void testSimplePhoneSATSmall() throws ContradictionException,
32 TimeoutException {
33
34 VecInt clause0 = new VecInt();
35 clause0.push(1);
36 solver.addClause(clause0);
37
38
39 VecInt clause1 = new VecInt();
40 clause1.push(1);
41 clause1.push(-2);
42 solver.addClause(clause1);
43
44 VecInt clause2 = new VecInt();
45 clause2.push(2);
46 clause2.push(-1);
47 solver.addClause(clause2);
48
49
50 VecInt clause3 = new VecInt();
51 clause3.push(3);
52 clause3.push(-2);
53 solver.addClause(clause3);
54
55 VecInt clause8 = new VecInt();
56 clause8.push(2);
57 clause8.push(-3);
58 solver.addClause(clause8);
59
60
61 VecInt clause4 = new VecInt();
62 clause4.push(-4);
63 clause4.push(1);
64 solver.addClause(clause4);
65
66
67 VecInt clause5 = new VecInt();
68 clause5.push(-5);
69 clause5.push(4);
70 solver.addClause(clause5);
71
72 VecInt clause6 = new VecInt();
73 clause6.push(-6);
74 clause6.push(4);
75 solver.addClause(clause6);
76
77 VecInt clause7 = new VecInt();
78 clause7.push(5);
79 clause7.push(6);
80 clause7.push(-4);
81 solver.addAtLeast(clause6, 1);
82
83 assertTrue(solver.isSatisfiable());
84 VecInt bound1 = new VecInt();
85 bound1.push(3);
86 assertNotNull(solver.findModel(bound1));
87
88 VecInt bound2 = new VecInt();
89 bound2.push(-3);
90 assertNull(solver.findModel(bound2));
91
92 VecInt bound3 = new VecInt();
93 bound3.push(5);
94 bound3.push(3);
95 assertNotNull(solver.findModel(bound3));
96
97 VecInt bound4 = new VecInt();
98 bound4.push(5);
99 bound4.push(-3);
100 assertNull(solver.findModel(bound4));
101
102 VecInt bound5 = new VecInt();
103 bound5.push(4);
104 bound5.push(-3);
105 assertNull(solver.findModel(bound5));
106
107 VecInt bound6 = new VecInt();
108 bound6.push(4);
109 bound6.push(3);
110 assertNotNull(solver.findModel(bound6));
111
112 VecInt bound7 = new VecInt();
113 bound7.push(4);
114
115 int[] model = solver.findModel(bound7);
116 assertNotNull(model);
117
118 Set<Integer> satisfiedModel = new HashSet<Integer>();
119 for (int i : model) {
120 satisfiedModel.add(new Integer(i));
121 }
122 assertTrue(satisfiedModel.contains(new Integer(4)));
123 assertTrue(satisfiedModel.contains(new Integer(1)));
124 assertTrue(satisfiedModel.contains(new Integer(2)));
125 }
126 }