• R/O
  • HTTP
  • SSH
  • HTTPS

Commit

Tags
No Tags

Frequently used words (click to add to your profile)

javac++androidlinuxc#windowsobjective-ccocoa誰得qtpythonphprubygameguibathyscaphec計画中(planning stage)翻訳omegatframeworktwitterdomtestvb.netdirectxゲームエンジンbtronarduinopreviewer

IPODwBDD


Commit MetaInfo

Revisionc0cae5fc0fde045f4ff87f5ea8bd569d2b6d52ce (tree)
Time2019-01-26 06:10:44
AuthorTatsuhiro Tsuchiya <tatsuhiro@ieee...>
CommiterTatsuhiro Tsuchiya

Log Message

Fixed big bugs related to SAT

Change Summary

Incremental Difference

--- /dev/null
+++ b/inputsamples/aircraft_fm.bach
@@ -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))
--- /dev/null
+++ b/inputsamples/smart_home_fm.bach
@@ -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]))
--- a/src/v1/SATConstraintHandler.java
+++ b/src/v1/SATConstraintHandler.java
@@ -5,6 +5,7 @@ import java.util.List;
55 import java.util.TreeSet;
66
77 import org.sat4j.minisat.SolverFactory;
8+import org.sat4j.specs.IConstr;
89 import org.sat4j.specs.ISolver;
910
1011 import bits.*;
@@ -153,7 +154,18 @@ class SATConstraintHandler implements ConstraintHandler {
153154 int v = test.get(p);
154155 if (v >= 0) {
155156 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+ }
157169 }
158170 }
159171 org.sat4j.specs.IProblem problem = solver;
@@ -172,7 +184,7 @@ class SATConstraintHandler implements ConstraintHandler {
172184 @Override
173185 public boolean isPossible(int[] test) {
174186 Boolean res = false;
175-
187+
176188 // ArrayList<IProblem> problemArrayList = new ArrayList<IProblem>();
177189 // problemArrayList.add(booleanConstraint);
178190 // try {
@@ -190,17 +202,30 @@ class SATConstraintHandler implements ConstraintHandler {
190202 // }
191203
192204 List<org.sat4j.specs.IConstr> constList = new ArrayList <org.sat4j.specs.IConstr>();
205+
193206 try {
194207 for (int i = 0; i < parameterToIDAndNumLevels.size(); i++) {
195208 int p = parameterToIDAndNumLevels.get(i).getID();
196209 int v = test[p];
197210 if (v >= 0) {
198211 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+ }
200224 }
201225 }
202226 org.sat4j.specs.IProblem problem = solver;
203227 res = problem.isSatisfiable();
228+
204229 for (org.sat4j.specs.IConstr cnst: constList) {
205230 solver.removeConstr(cnst);
206231 }