IPODwBDD
| Revision | c0cae5fc0fde045f4ff87f5ea8bd569d2b6d52ce (tree) |
|---|---|
| Time | 2019-01-26 06:10:44 |
| Author | |
| Commiter | Tatsuhiro Tsuchiya |
Fixed big bugs related to SAT
| @@ -0,0 +1,35 @@ | ||
| 1 | +# [Parameter] | |
| 2 | +Low (true false) | |
| 3 | +Materials (true false) | |
| 4 | +Piston (true false) | |
| 5 | +Jet (true false) | |
| 6 | +Wood (true false) | |
| 7 | +Plastic (true false) | |
| 8 | +Engine (true false) | |
| 9 | +Cloth (true false) | |
| 10 | +Aircraft (true false) | |
| 11 | +Metal (true false) | |
| 12 | +Shoulder (true false) | |
| 13 | +High (true false) | |
| 14 | +Wing (true false) | |
| 15 | + | |
| 16 | +# [Constraint] | |
| 17 | +(== [Aircraft] true) | |
| 18 | +(or (== [Wing] false) (== [Aircraft] true)) | |
| 19 | +(or (== [Aircraft] false) (== [Wing] true)) | |
| 20 | +(or (== [Engine] false) (== [Aircraft] true)) | |
| 21 | +(or (== [Materials] false) (== [Aircraft] true)) | |
| 22 | +(or (== [Aircraft] false) (== [Materials] true)) | |
| 23 | +(or (== [High] false) (== [Wing] true)) | |
| 24 | +(or (== [Shoulder] false) (== [Wing] true)) | |
| 25 | +(or (== [Low] false) (== [Wing] true)) | |
| 26 | +(or (== [Wing] false) (== [High] true) (== [Shoulder] true) (== [Low] true)) | |
| 27 | +(or (== [Jet] false) (== [Engine] true)) | |
| 28 | +(or (== [Piston] false) (== [Engine] true)) | |
| 29 | +(or (== [Engine] false) (== [Jet] true) (== [Piston] true)) | |
| 30 | +(or (== [Jet] false) (== [Piston] false)) | |
| 31 | +(or (== [Metal] false) (== [Materials] true)) | |
| 32 | +(or (== [Wood] false) (== [Materials] true)) | |
| 33 | +(or (== [Cloth] false) (== [Materials] true)) | |
| 34 | +(or (== [Plastic] false) (== [Materials] true)) | |
| 35 | +(or (== [Materials] false) (== [Metal] true) (== [Wood] true) (== [Cloth] true) (== [Plastic] true)) |
| @@ -0,0 +1,91 @@ | ||
| 1 | +# [System] | |
| 2 | +# Name: Smart home | |
| 3 | + | |
| 4 | +# [Parameter] | |
| 5 | +Other_Group (true false) | |
| 6 | +Siren (true false) | |
| 7 | +Bell (true false) | |
| 8 | +Card_Reader (true false) | |
| 9 | +Environment_Control (true false) | |
| 10 | +_Fahrenheit (true false) | |
| 11 | +Measurement_Units (true false) | |
| 12 | +Touch_Screen (true false) | |
| 13 | +First_Aid_Group (true false) | |
| 14 | +Fire_Alarm (true false) | |
| 15 | +Manual_Windows (true false) | |
| 16 | +Automatic_Windows (true false) | |
| 17 | +Smart_Home (true false) | |
| 18 | +Mobile (true false) | |
| 19 | +Presence_Simulator (true false) | |
| 20 | +Light (true false) | |
| 21 | +Windows_Management (true false) | |
| 22 | +Music_Simulation (true false) | |
| 23 | +Simple_Control (true false) | |
| 24 | +Smart_Heating_Management (true false) | |
| 25 | +Smart_Light_Management (true false) | |
| 26 | +Fire_Control (true false) | |
| 27 | +_Celsius (true false) | |
| 28 | +Heating_Management (true false) | |
| 29 | +Temperature_Management (true false) | |
| 30 | +GUI (true false) | |
| 31 | +Light_Management (true false) | |
| 32 | +Pre_defined_Values (true false) | |
| 33 | +Fingerprint_Reader (true false) | |
| 34 | +Door_Lock (true false) | |
| 35 | +Blind_Simulation (true false) | |
| 36 | +Keypad_Reader (true false) | |
| 37 | +Fire_Department (true false) | |
| 38 | +Internet (true false) | |
| 39 | +Light_Simulation (true false) | |
| 40 | + | |
| 41 | + | |
| 42 | +# [Constraint]])) | |
| 43 | +(== true [Smart_Home]) | |
| 44 | +(or (== false [Environment_Control]) (== true [Smart_Home])) | |
| 45 | +(or (== false [Smart_Home]) (== true [Environment_Control])) | |
| 46 | +(or (== false [Light_Management]) (== true [Smart_Home])) | |
| 47 | +(or (== false [Smart_Home]) (== true [Light_Management])) | |
| 48 | +(or (== false [GUI]) (== true [Smart_Home])) | |
| 49 | +(or (== false [Smart_Home]) (== true [GUI])) | |
| 50 | +(or (== false [Presence_Simulator]) (== true [Smart_Home])) | |
| 51 | +(or (== false [Smart_Home]) (== true [Presence_Simulator])) | |
| 52 | +(or (== false [Fire_Control]) (== true [Smart_Home])) | |
| 53 | +(or (== false [Smart_Home]) (== true [Fire_Control])) | |
| 54 | +(or (== false [Door_Lock]) (== true [Smart_Home])) | |
| 55 | +(or (== false [Smart_Home]) (== true [Door_Lock])) | |
| 56 | +(or (== false [Measurement_Units]) (== true [Environment_Control])) | |
| 57 | +(or (== false [Environment_Control]) (== true [Measurement_Units])) | |
| 58 | +(or (== false [Temperature_Management]) (== true [Environment_Control])) | |
| 59 | +(or (== false [Environment_Control]) (== true [Temperature_Management])) | |
| 60 | +(or (== false [Windows_Management]) (== true [Environment_Control])) | |
| 61 | +(or (== false [Environment_Control]) (== true [Windows_Management])) | |
| 62 | +(or (== false [Smart_Light_Management]) (== true [Light_Management])) | |
| 63 | +(or (== false [Pre_defined_Values]) (== true [Light_Management])) | |
| 64 | +(or (== false [Simple_Control]) (== true [Light_Management])) | |
| 65 | +(or (== false [Light_Management]) (== true [Simple_Control])) | |
| 66 | +(or (== false [Touch_Screen]) (== true [GUI])) | |
| 67 | +(or (== false [Mobile]) (== true [GUI])) | |
| 68 | +(or (== false [Internet]) (== true [GUI])) | |
| 69 | +(or (== false [Light_Simulation]) (== true [Presence_Simulator])) | |
| 70 | +(or (== false [Blind_Simulation]) (== true [Presence_Simulator])) | |
| 71 | +(or (== false [Music_Simulation]) (== true [Presence_Simulator])) | |
| 72 | +(or (== false [First_Aid_Group]) (== true [Fire_Control])) | |
| 73 | +(or (== false [Fire_Control]) (== true [First_Aid_Group])) | |
| 74 | +(or (== false [Fire_Alarm]) (== true [Fire_Control])) | |
| 75 | +(or (== false [Fire_Control]) (== true [Fire_Alarm])) | |
| 76 | +(or (== false [Keypad_Reader]) (== true [Door_Lock])) | |
| 77 | +(or (== false [Card_Reader]) (== true [Door_Lock])) | |
| 78 | +(or (== false [Fingerprint_Reader]) (== true [Door_Lock])) | |
| 79 | +(or (== false [_Celsius]) (== true [Measurement_Units])) | |
| 80 | +(or (== false [_Fahrenheit]) (== true [Measurement_Units])) | |
| 81 | +(or (== false [Heating_Management]) (== true [Temperature_Management])) | |
| 82 | +(or (== false [Temperature_Management]) (== true [Heating_Management])) | |
| 83 | +(or (== false [Smart_Heating_Management]) (== true [Temperature_Management])) | |
| 84 | +(or (== false [Manual_Windows]) (== true [Windows_Management])) | |
| 85 | +(or (== false [Windows_Management]) (== true [Manual_Windows])) | |
| 86 | +(or (== false [Automatic_Windows]) (== true [Windows_Management])) | |
| 87 | +(or (== false [Fire_Department]) (== true [First_Aid_Group])) | |
| 88 | +(or (== false [Other_Group]) (== true [First_Aid_Group])) | |
| 89 | +(or (== false [Siren]) (== true [Fire_Alarm])) | |
| 90 | +(or (== false [Bell]) (== true [Fire_Alarm])) | |
| 91 | +(or (== false [Light]) (== true [Fire_Alarm])) |
| @@ -5,6 +5,7 @@ import java.util.List; | ||
| 5 | 5 | import java.util.TreeSet; |
| 6 | 6 | |
| 7 | 7 | import org.sat4j.minisat.SolverFactory; |
| 8 | +import org.sat4j.specs.IConstr; | |
| 8 | 9 | import org.sat4j.specs.ISolver; |
| 9 | 10 | |
| 10 | 11 | import bits.*; |
| @@ -153,7 +154,18 @@ class SATConstraintHandler implements ConstraintHandler { | ||
| 153 | 154 | int v = test.get(p); |
| 154 | 155 | if (v >= 0) { |
| 155 | 156 | int [] clause = {sat4jvariables[i][v]}; |
| 156 | - constList.add(solver.addClause(new org.sat4j.core.VecInt(clause))); | |
| 157 | + try { | |
| 158 | + IConstr tmp = solver.addClause(new org.sat4j.core.VecInt(clause)); | |
| 159 | + if (tmp != null) | |
| 160 | + constList.add(tmp); | |
| 161 | + } | |
| 162 | + catch (org.sat4j.specs.ContradictionException e) { | |
| 163 | + res = false; | |
| 164 | + for (org.sat4j.specs.IConstr cnst: constList) { | |
| 165 | + solver.removeConstr(cnst); | |
| 166 | + } | |
| 167 | + return res; | |
| 168 | + } | |
| 157 | 169 | } |
| 158 | 170 | } |
| 159 | 171 | org.sat4j.specs.IProblem problem = solver; |
| @@ -172,7 +184,7 @@ class SATConstraintHandler implements ConstraintHandler { | ||
| 172 | 184 | @Override |
| 173 | 185 | public boolean isPossible(int[] test) { |
| 174 | 186 | Boolean res = false; |
| 175 | - | |
| 187 | + | |
| 176 | 188 | // ArrayList<IProblem> problemArrayList = new ArrayList<IProblem>(); |
| 177 | 189 | // problemArrayList.add(booleanConstraint); |
| 178 | 190 | // try { |
| @@ -190,17 +202,30 @@ class SATConstraintHandler implements ConstraintHandler { | ||
| 190 | 202 | // } |
| 191 | 203 | |
| 192 | 204 | List<org.sat4j.specs.IConstr> constList = new ArrayList <org.sat4j.specs.IConstr>(); |
| 205 | + | |
| 193 | 206 | try { |
| 194 | 207 | for (int i = 0; i < parameterToIDAndNumLevels.size(); i++) { |
| 195 | 208 | int p = parameterToIDAndNumLevels.get(i).getID(); |
| 196 | 209 | int v = test[p]; |
| 197 | 210 | if (v >= 0) { |
| 198 | 211 | int [] clause = {sat4jvariables[i][v]}; |
| 199 | - constList.add(solver.addClause(new org.sat4j.core.VecInt(clause))); | |
| 212 | + try { | |
| 213 | + IConstr tmp = solver.addClause(new org.sat4j.core.VecInt(clause)); | |
| 214 | + if (tmp != null) | |
| 215 | + constList.add(tmp); | |
| 216 | + } | |
| 217 | + catch (org.sat4j.specs.ContradictionException e) { | |
| 218 | + res = false; | |
| 219 | + for (org.sat4j.specs.IConstr cnst: constList) { | |
| 220 | + solver.removeConstr(cnst); | |
| 221 | + } | |
| 222 | + return res; | |
| 223 | + } | |
| 200 | 224 | } |
| 201 | 225 | } |
| 202 | 226 | org.sat4j.specs.IProblem problem = solver; |
| 203 | 227 | res = problem.isSatisfiable(); |
| 228 | + | |
| 204 | 229 | for (org.sat4j.specs.IConstr cnst: constList) { |
| 205 | 230 | solver.removeConstr(cnst); |
| 206 | 231 | } |