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
29
30
31 package org.sat4j.tools.encoding;
32
33 import org.sat4j.specs.ContradictionException;
34 import org.sat4j.specs.IConstr;
35 import org.sat4j.specs.ISolver;
36 import org.sat4j.specs.IVecInt;
37
38
39
40
41
42
43
44
45 public class Policy extends EncodingStrategyAdapter {
46
47
48
49
50 private static final long serialVersionUID = 1L;
51 private final Sequential seq = new Sequential();
52 private final Binary binary = new Binary();
53 private final Product product = new Product();
54 private final Commander commander = new Commander();
55 private final Binomial binomial = new Binomial();
56 private final Ladder ladder = new Ladder();
57
58 private EncodingStrategyAdapter atMostOneEncoding = null;
59 private EncodingStrategyAdapter atMostKEncoding = null;
60 private EncodingStrategyAdapter exactlyOneEncoding = null;
61 private EncodingStrategyAdapter exactlyKEncoding = null;
62 private EncodingStrategyAdapter atLeastOneEncoding = null;
63 private EncodingStrategyAdapter atLeastKEncoding = null;
64
65 private EncodingStrategyAdapter getAdapterFromEncodingName(
66 EncodingStrategy encodingName) {
67 switch (encodingName) {
68 case BINARY:
69 return this.binary;
70 case BINOMIAL:
71 return this.binomial;
72 case COMMANDER:
73 return this.commander;
74 case LADDER:
75 return this.ladder;
76 case PRODUCT:
77 return this.product;
78 case SEQUENTIAL:
79 return this.seq;
80 case NATIVE:
81 default:
82 return null;
83 }
84 }
85
86 private EncodingStrategy getEncodingTypeFromAdapter(
87 EncodingStrategyAdapter adapter) {
88 if (adapter instanceof Binary) {
89 return EncodingStrategy.BINARY;
90 } else if (adapter instanceof Binomial) {
91 return EncodingStrategy.BINOMIAL;
92 } else if (adapter instanceof Commander) {
93 return EncodingStrategy.COMMANDER;
94 } else if (adapter instanceof Ladder) {
95 return EncodingStrategy.LADDER;
96 } else if (adapter instanceof Product) {
97 return EncodingStrategy.PRODUCT;
98 } else if (adapter instanceof Sequential) {
99 return EncodingStrategy.SEQUENTIAL;
100 } else {
101 return EncodingStrategy.NATIVE;
102 }
103
104 }
105
106 public EncodingStrategyAdapter getAtMostOneEncoding() {
107 return this.atMostOneEncoding;
108 }
109
110 public void setAtMostOneEncoding(EncodingStrategyAdapter atMostOneEncoding) {
111 this.atMostOneEncoding = atMostOneEncoding;
112 }
113
114 public void setAtMostOneEncoding(EncodingStrategy atMostOneEncoding) {
115 this.atMostOneEncoding = getAdapterFromEncodingName(atMostOneEncoding);
116 }
117
118 public EncodingStrategyAdapter getAtMostKEncoding() {
119 return this.atMostKEncoding;
120 }
121
122 public void setAtMostKEncoding(EncodingStrategyAdapter atMostKEncoding) {
123 this.atMostKEncoding = atMostKEncoding;
124 }
125
126 public void setAtMostKEncoding(EncodingStrategy atMostKEncoding) {
127 this.atMostKEncoding = getAdapterFromEncodingName(atMostKEncoding);
128 }
129
130 public EncodingStrategyAdapter getExactlyOneEncoding() {
131 return this.exactlyOneEncoding;
132 }
133
134 public void setExactlyOneEncoding(EncodingStrategyAdapter exactlyOneEncoding) {
135 this.exactlyOneEncoding = exactlyOneEncoding;
136 }
137
138 public void setExactlyOneEncoding(EncodingStrategy exactlyOneEncoding) {
139 this.exactlyOneEncoding = getAdapterFromEncodingName(exactlyOneEncoding);
140 }
141
142 public EncodingStrategyAdapter getExactlyKEncoding() {
143 return this.exactlyKEncoding;
144 }
145
146 public void setExactlyKEncoding(EncodingStrategyAdapter exactlyKEncoding) {
147 this.exactlyKEncoding = exactlyKEncoding;
148 }
149
150 public void setExactlyKEncoding(EncodingStrategy exactlyKEncoding) {
151 this.exactlyKEncoding = getAdapterFromEncodingName(exactlyKEncoding);
152 }
153
154 public EncodingStrategyAdapter getAtLeastOneEncoding() {
155 return this.atLeastOneEncoding;
156 }
157
158 public void setAtLeastOneEncoding(EncodingStrategyAdapter atLeastOneEncoding) {
159 this.atLeastOneEncoding = atLeastOneEncoding;
160 }
161
162 public void setAtLeastOneEncoding(EncodingStrategy atLeastOneEncoding) {
163 this.atLeastOneEncoding = getAdapterFromEncodingName(atLeastOneEncoding);
164 }
165
166 public EncodingStrategyAdapter getAtLeastKEncoding() {
167 return this.atLeastKEncoding;
168 }
169
170 public void setAtLeastKEncoding(EncodingStrategyAdapter atLeastKEncoding) {
171 this.atLeastKEncoding = atLeastKEncoding;
172 }
173
174 public void setAtLeastKEncoding(EncodingStrategy atLeastKEncoding) {
175 this.atLeastKEncoding = getAdapterFromEncodingName(atLeastKEncoding);
176 }
177
178 @Override
179 public IConstr addAtMost(ISolver solver, IVecInt literals, int k)
180 throws ContradictionException {
181
182 if (k == 0 || literals.size() == 1) {
183
184 return super.addAtMost(solver, literals, k);
185 }
186 if (literals.size() <= 1) {
187 throw new UnsupportedOperationException(
188 "requires at least 2 literals");
189 }
190 if (k == 1 && this.atMostOneEncoding != null) {
191 return this.atMostOneEncoding.addAtMostOne(solver, literals);
192 }
193 if (this.atMostKEncoding != null) {
194 if (k == 1) {
195 return this.atMostKEncoding.addAtMostOne(solver, literals);
196 } else {
197 return this.atMostKEncoding.addAtMost(solver, literals, k);
198 }
199 }
200 return super.addAtMost(solver, literals, k);
201 }
202
203 @Override
204 public IConstr addExactly(ISolver solver, IVecInt literals, int n)
205 throws ContradictionException {
206 if (n == 1 && this.exactlyOneEncoding != null) {
207 return this.exactlyOneEncoding.addExactlyOne(solver, literals);
208 } else if (this.exactlyKEncoding != null) {
209 if (n == 1) {
210 return this.exactlyKEncoding.addExactlyOne(solver, literals);
211 } else {
212 return this.exactlyKEncoding.addExactly(solver, literals, n);
213 }
214 }
215
216 return super.addExactly(solver, literals, n);
217 }
218
219 @Override
220 public IConstr addAtLeast(ISolver solver, IVecInt literals, int n)
221 throws ContradictionException {
222 if (n == 1) {
223 if (this.atLeastOneEncoding != null) {
224 return this.atLeastOneEncoding.addAtLeastOne(solver, literals);
225 }
226 } else if (this.atLeastKEncoding != null) {
227 return this.atLeastKEncoding.addAtLeast(solver, literals, n);
228 }
229
230 return super.addAtLeast(solver, literals, n);
231
232 }
233
234 @Override
235 public String toString() {
236 String s = "";
237 s += "Policy = [At most K: "
238 + getEncodingTypeFromAdapter(getAtMostKEncoding())
239 + ", at most 1: "
240 + getEncodingTypeFromAdapter(getAtMostOneEncoding())
241 + ", exactly K: "
242 + getEncodingTypeFromAdapter(getExactlyKEncoding())
243 + ", exactly 1: "
244 + getEncodingTypeFromAdapter(getExactlyOneEncoding()) + "]";
245
246 return s;
247 }
248
249 }