View Javadoc

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       * @throws java.lang.Exception
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          // SmallFeaturePhone (1)
34          VecInt clause0 = new VecInt();
35          clause0.push(1);
36          solver.addClause(clause0);
37  
38          // Message (2)
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          // SMS (3)
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          // Extras (4)
61          VecInt clause4 = new VecInt();
62          clause4.push(-4);
63          clause4.push(1);
64          solver.addClause(clause4);
65  
66          // MP3 (5) v Camera (6)
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)); // TODO Error
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 }