1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28 package org.sat4j.pb.core;
29
30 import org.sat4j.core.Vec;
31 import org.sat4j.minisat.core.Constr;
32 import org.sat4j.minisat.core.IOrder;
33 import org.sat4j.minisat.core.LearningStrategy;
34 import org.sat4j.minisat.core.Pair;
35 import org.sat4j.minisat.core.RestartStrategy;
36 import org.sat4j.minisat.core.SearchParams;
37 import org.sat4j.minisat.restarts.MiniSATRestarts;
38 import org.sat4j.pb.constraints.pb.ConflictMap;
39 import org.sat4j.pb.constraints.pb.IConflict;
40 import org.sat4j.pb.constraints.pb.PBConstr;
41 import org.sat4j.specs.IVec;
42 import org.sat4j.specs.TimeoutException;
43
44
45
46
47
48 public class PBSolverCP extends PBSolver {
49
50 private static final long serialVersionUID = 1L;
51
52
53
54
55
56
57 public PBSolverCP(LearningStrategy<PBDataStructureFactory> learner,
58 PBDataStructureFactory dsf, IOrder order) {
59 super(learner, dsf, new SearchParams(1.5, 100), order,
60 new MiniSATRestarts());
61 }
62
63 public PBSolverCP(LearningStrategy<PBDataStructureFactory> learner,
64 PBDataStructureFactory dsf, SearchParams params, IOrder order,
65 RestartStrategy restarter) {
66 super(learner, dsf, params, order, restarter);
67 }
68
69 public PBSolverCP(LearningStrategy<PBDataStructureFactory> learner,
70 PBDataStructureFactory dsf, SearchParams params, IOrder order) {
71 super(learner, dsf, params, order, new MiniSATRestarts());
72 }
73
74 @Override
75 public void analyze(Constr myconfl, Pair results) throws TimeoutException {
76 if (someCriteria())
77 analyzeCP(myconfl, results);
78 else
79 super.analyze(myconfl, results);
80 }
81
82 public void analyzeCP(Constr myconfl, Pair results) throws TimeoutException {
83 int litImplied = trail.last();
84 int currentLevel = voc.getLevel(litImplied);
85 IConflict confl = chooseConflict((PBConstr) myconfl, currentLevel);
86 assert confl.slackConflict().signum() < 0;
87 while (!confl.isAssertive(currentLevel)) {
88 if (!undertimeout) {
89 throw new TimeoutException();
90 }
91 PBConstr constraint = (PBConstr) voc.getReason(litImplied);
92
93 confl.resolve(constraint, litImplied, this);
94 updateNumberOfReductions(confl);
95 assert confl.slackConflict().signum() <= 0;
96
97 if (trail.size() == 1)
98 break;
99 undoOne();
100
101 if (decisionLevel() == 0)
102 break;
103 litImplied = trail.last();
104 if (voc.getLevel(litImplied) != currentLevel) {
105 trailLim.pop();
106 confl.updateSlack(voc.getLevel(litImplied));
107 }
108 assert voc.getLevel(litImplied) <= currentLevel;
109 currentLevel = voc.getLevel(litImplied);
110 assert confl.slackIsCorrect(currentLevel);
111 assert currentLevel == decisionLevel();
112 assert litImplied > 1;
113 }
114 assert confl.isAssertive(currentLevel) || trail.size() == 1
115 || decisionLevel() == 0;
116
117 assert currentLevel == decisionLevel();
118 undoOne();
119
120 updateNumberOfReducedLearnedConstraints(confl);
121
122
123 if ((confl.size() == 0)
124 || ((decisionLevel() == 0 || trail.size() == 0) && confl
125 .slackConflict().signum() < 0)) {
126 results.reason = null;
127 results.backtrackLevel = -1;
128 return;
129 }
130
131
132 PBConstr resConstr = (PBConstr) dsfactory
133 .createUnregisteredPseudoBooleanConstraint(confl);
134
135 results.reason = resConstr;
136 getSearchListener().learn(resConstr);
137
138
139
140
141 if (decisionLevel() == 0 || trail.size() == 0)
142 results.backtrackLevel = -1;
143 else
144 results.backtrackLevel = confl.getBacktrackLevel(currentLevel);
145 }
146
147 IConflict chooseConflict(PBConstr myconfl, int level) {
148 return ConflictMap.createConflict(myconfl, level);
149 }
150
151 @Override
152 public String toString(String prefix) {
153 return prefix + "Cutting planes based inference ("
154 + this.getClass().getName() + ")\n" + super.toString(prefix);
155 }
156
157 private final IVec<String> conflictVariables = new Vec<String>();
158 private final IVec<String> conflictConstraints = new Vec<String>();
159
160 void initExplanation() {
161 conflictVariables.clear();
162 conflictConstraints.clear();
163 }
164
165 boolean someCriteria() {
166 return true;
167 }
168
169 protected void updateNumberOfReductions(IConflict confl) {
170 }
171
172 protected void updateNumberOfReducedLearnedConstraints(IConflict confl) {
173 }
174
175 }