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.minisat.constraints.card; |
29 |
| |
30 |
| import java.io.Serializable; |
31 |
| |
32 |
| import org.sat4j.minisat.core.Constr; |
33 |
| import org.sat4j.minisat.core.ILits; |
34 |
| import org.sat4j.minisat.core.Undoable; |
35 |
| import org.sat4j.minisat.core.UnitPropagationListener; |
36 |
| import org.sat4j.specs.ContradictionException; |
37 |
| import org.sat4j.specs.IVecInt; |
38 |
| |
39 |
| |
40 |
| |
41 |
| |
42 |
| |
43 |
| |
44 |
| |
45 |
| |
46 |
| |
47 |
| public class AtLeast implements Constr, Undoable, Serializable { |
48 |
| |
49 |
| private static final long serialVersionUID = 1L; |
50 |
| |
51 |
| |
52 |
| private int n; |
53 |
| |
54 |
| |
55 |
| private int counter; |
56 |
| |
57 |
| |
58 |
| |
59 |
| |
60 |
| private final int[] lits; |
61 |
| |
62 |
| private final ILits voc; |
63 |
| |
64 |
| |
65 |
| |
66 |
| |
67 |
| |
68 |
| |
69 |
| |
70 |
252740
| private AtLeast(ILits voc, IVecInt ps, int n) {
|
71 |
252740
| this.n = ps.size() - n;
|
72 |
252740
| this.voc = voc;
|
73 |
252740
| counter = 0;
|
74 |
252740
| lits = new int[ps.size()];
|
75 |
252740
| ps.moveTo(lits);
|
76 |
252740
| for (int q : lits) {
|
77 |
822293
| voc.watch(q ^ 1, this);
|
78 |
| } |
79 |
| } |
80 |
| |
81 |
252817
| public static AtLeast atLeastNew(UnitPropagationListener s, ILits voc,
|
82 |
| IVecInt ps, int n) throws ContradictionException { |
83 |
252817
| if (ps.size() < n)
|
84 |
40
| throw new ContradictionException();
|
85 |
252777
| int degree = n;
|
86 |
252777
| for (int i = 0; i < ps.size();) {
|
87 |
| |
88 |
823112
| if (!voc.isUnassigned(ps.get(i))) {
|
89 |
| |
90 |
| |
91 |
327
| if (voc.isSatisfied(ps.get(i))) {
|
92 |
153
| degree--;
|
93 |
| } |
94 |
| |
95 |
| |
96 |
327
| ps.delete(i);
|
97 |
| } else { |
98 |
| |
99 |
822785
| i++;
|
100 |
| } |
101 |
| } |
102 |
| |
103 |
| |
104 |
252777
| ps.sortUnique();
|
105 |
| |
106 |
| |
107 |
| |
108 |
| |
109 |
252777
| for (int i = 0; i < ps.size() - 1;) {
|
110 |
570008
| if (ps.get(i) == (ps.get(i + 1) ^ 1)) {
|
111 |
| |
112 |
| |
113 |
| |
114 |
| |
115 |
| |
116 |
| |
117 |
| |
118 |
13
| i++;
|
119 |
| } else { |
120 |
569995
| i++;
|
121 |
| } |
122 |
| } |
123 |
| |
124 |
252777
| if (ps.size() == degree) {
|
125 |
22
| for (int i = 0; i < ps.size(); i++) {
|
126 |
387
| if (!s.enqueue(ps.get(i))) {
|
127 |
0
| throw new ContradictionException();
|
128 |
| } |
129 |
| } |
130 |
22
| return null;
|
131 |
| } |
132 |
| |
133 |
252755
| if (ps.size() < degree)
|
134 |
15
| throw new ContradictionException();
|
135 |
252740
| if (degree == 0)
|
136 |
0
| return null;
|
137 |
| |
138 |
252740
| return new AtLeast(voc, ps, degree);
|
139 |
| } |
140 |
| |
141 |
| |
142 |
| |
143 |
| |
144 |
| |
145 |
| |
146 |
0
| public void remove() {
|
147 |
0
| for (int q : lits) {
|
148 |
0
| voc.watches(q ^ 1).remove(this);
|
149 |
| } |
150 |
| } |
151 |
| |
152 |
| |
153 |
| |
154 |
| |
155 |
| |
156 |
| |
157 |
339525105
| public boolean propagate(UnitPropagationListener s, int p) {
|
158 |
| |
159 |
339525105
| voc.watch(p, this);
|
160 |
| |
161 |
339525105
| if (counter == n)
|
162 |
12806131
| return false;
|
163 |
| |
164 |
326718974
| counter++;
|
165 |
326718974
| voc.undos(p).push(this);
|
166 |
| |
167 |
| |
168 |
326718974
| if (counter == n)
|
169 |
205808821
| for (int q : lits) {
|
170 |
1092700953
| if (voc.isUnassigned(q)) {
|
171 |
251829038
| if (!s.enqueue(q, this)) {
|
172 |
0
| return false;
|
173 |
| } |
174 |
| } |
175 |
| } |
176 |
326718974
| return true;
|
177 |
| } |
178 |
| |
179 |
| |
180 |
| |
181 |
| |
182 |
| |
183 |
| |
184 |
458488
| public boolean simplify() {
|
185 |
458488
| return false;
|
186 |
| } |
187 |
| |
188 |
| |
189 |
| |
190 |
| |
191 |
| |
192 |
| |
193 |
326679697
| public void undo(int p) {
|
194 |
326679697
| counter--;
|
195 |
| } |
196 |
| |
197 |
| |
198 |
| |
199 |
| |
200 |
| |
201 |
| |
202 |
117977943
| public void calcReason(int p, IVecInt outReason) {
|
203 |
117977943
| for (int q : lits) {
|
204 |
960506479
| if (voc.isFalsified(q)) {
|
205 |
419471597
| outReason.push(q ^ 1);
|
206 |
| } |
207 |
| } |
208 |
| } |
209 |
| |
210 |
| |
211 |
| |
212 |
| |
213 |
| |
214 |
| |
215 |
117977943
| public boolean learnt() {
|
216 |
| |
217 |
117977943
| return false;
|
218 |
| } |
219 |
| |
220 |
| |
221 |
| |
222 |
| |
223 |
| |
224 |
| |
225 |
0
| public double getActivity() {
|
226 |
| |
227 |
0
| return 0;
|
228 |
| } |
229 |
| |
230 |
| |
231 |
| |
232 |
| |
233 |
| |
234 |
| |
235 |
0
| public void incActivity(double claInc) {
|
236 |
| |
237 |
| |
238 |
| } |
239 |
| |
240 |
| |
241 |
| |
242 |
| |
243 |
0
| public boolean locked() {
|
244 |
| |
245 |
| |
246 |
0
| return true;
|
247 |
| } |
248 |
| |
249 |
0
| public void setLearnt() {
|
250 |
0
| throw new UnsupportedOperationException();
|
251 |
| } |
252 |
| |
253 |
0
| public void register() {
|
254 |
0
| throw new UnsupportedOperationException();
|
255 |
| } |
256 |
| |
257 |
0
| public int size() {
|
258 |
0
| return lits.length;
|
259 |
| } |
260 |
| |
261 |
0
| public int get(int i) {
|
262 |
0
| return lits[i];
|
263 |
| } |
264 |
| |
265 |
0
| public void rescaleBy(double d) {
|
266 |
0
| throw new UnsupportedOperationException();
|
267 |
| } |
268 |
| |
269 |
0
| public void assertConstraint(UnitPropagationListener s) {
|
270 |
0
| throw new UnsupportedOperationException();
|
271 |
| } |
272 |
| } |