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.constraints.pb;
29
30 import java.math.BigInteger;
31
32 import org.sat4j.minisat.constraints.card.MinWatchCard;
33 import org.sat4j.minisat.core.ILits;
34 import org.sat4j.minisat.core.UnitPropagationListener;
35 import org.sat4j.specs.ContradictionException;
36 import org.sat4j.specs.IVecInt;
37
38 public class MinWatchCardPB extends MinWatchCard implements PBConstr {
39
40
41
42
43 private static final long serialVersionUID = 1L;
44
45 private final BigInteger degree;
46
47 public MinWatchCardPB(ILits voc, IVecInt ps, boolean moreThan, int degree) {
48 super(voc, ps, moreThan, degree);
49 this.degree = BigInteger.valueOf(degree);
50 }
51
52 public MinWatchCardPB(ILits voc, IVecInt ps, int degree) {
53 super(voc, ps, degree);
54 this.degree = BigInteger.valueOf(degree);
55 }
56
57
58
59
60
61
62 public BigInteger getCoef(int literal) {
63 return BigInteger.ONE;
64 }
65
66
67
68
69
70
71 public BigInteger getDegree() {
72 return degree;
73 }
74
75 public BigInteger[] getCoefs() {
76 BigInteger[] tmp = new BigInteger[size()];
77 for (int i = 0; i < tmp.length; i++)
78 tmp[i] = BigInteger.ONE;
79 return tmp;
80 }
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96 public static MinWatchCardPB normalizedMinWatchCardPBNew(
97 UnitPropagationListener s, ILits voc, IVecInt ps, int degree)
98 throws ContradictionException {
99 return minWatchCardPBNew(s, voc, ps, ATLEAST, degree, true);
100 }
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118 public static MinWatchCardPB minWatchCardPBNew(UnitPropagationListener s,
119 ILits voc, IVecInt ps, boolean moreThan, int degree)
120 throws ContradictionException {
121 return minWatchCardPBNew(s, voc, ps, moreThan, degree, false);
122 }
123
124 private static MinWatchCardPB minWatchCardPBNew(UnitPropagationListener s,
125 ILits voc, IVecInt ps, boolean moreThan, int degree,
126 boolean normalized) throws ContradictionException {
127 int mydegree = degree + linearisation(voc, ps);
128
129 if (ps.size() == 0 && mydegree > 0) {
130 throw new ContradictionException();
131 } else if (ps.size() == mydegree || ps.size() <= 0) {
132 for (int i = 0; i < ps.size(); i++)
133 if (!s.enqueue(ps.get(i))) {
134 throw new ContradictionException();
135 }
136 return null;
137 }
138
139
140 MinWatchCardPB retour = null;
141 if (normalized)
142 retour = new MinWatchCardPB(voc, ps, mydegree);
143 else
144 retour = new MinWatchCardPB(voc, ps, moreThan, mydegree);
145
146 if (retour.degree.signum() <= 0)
147 return null;
148
149 retour.computeWatches();
150
151 return ((MinWatchCardPB) retour.computePropagation(s));
152 }
153
154
155
156
157 private boolean learnt = false;
158
159
160
161
162
163
164
165 @Override
166 public boolean learnt() {
167 return learnt;
168 }
169
170 @Override
171 public void setLearnt() {
172 learnt = true;
173 }
174
175 @Override
176 public void register() {
177 assert learnt;
178 computeWatches();
179 }
180
181 @Override
182 public void assertConstraint(UnitPropagationListener s) {
183 for (int i = 0; i < size(); i++) {
184 if (getVocabulary().isUnassigned(get(i))) {
185 boolean ret = s.enqueue(get(i), this);
186 assert ret;
187 }
188 }
189 }
190
191 public IVecInt computeAnImpliedClause() {
192 return null;
193 }
194
195
196 }