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 private final Sequential seq = new Sequential();
48 private final Binary binary = new Binary();
49 private final Product product = new Product();
50 private final Commander commander = new Commander();
51 private final Binomial binomial = new Binomial();
52 private final Ladder ladder = new Ladder();
53
54 private EncodingStrategyAdapter atMostOneEncoding;
55 private EncodingStrategyAdapter atMostKEncoding;
56 private EncodingStrategyAdapter exactlyOneEncoding;
57 private EncodingStrategyAdapter exactlyKEncoding;
58 private EncodingStrategyAdapter atLeastOneEncoding;
59 private EncodingStrategyAdapter atLeastKEncoding;
60
61 private EncodingStrategyAdapter getAdapterFromEncodingName(
62 EncodingStrategy encodingName) {
63 switch (encodingName) {
64 case BINARY:
65 return this.binary;
66 case BINOMIAL:
67 return this.binomial;
68 case COMMANDER:
69 return this.commander;
70 case LADDER:
71 return this.ladder;
72 case PRODUCT:
73 return this.product;
74 case SEQUENTIAL:
75 return this.seq;
76 default:
77 return null;
78 }
79 }
80
81 public EncodingStrategyAdapter getAtMostOneEncoding() {
82 return this.atMostOneEncoding;
83 }
84
85 public void setAtMostOneEncoding(EncodingStrategyAdapter atMostOneEncoding) {
86 this.atMostOneEncoding = atMostOneEncoding;
87 }
88
89 public void setAtMostOneEncoding(EncodingStrategy atMostOneEncoding) {
90 this.atMostOneEncoding = getAdapterFromEncodingName(atMostOneEncoding);
91 }
92
93 public EncodingStrategyAdapter getAtMostKEncoding() {
94 return this.atMostKEncoding;
95 }
96
97 public void setAtMostKEncoding(EncodingStrategyAdapter atMostKEncoding) {
98 this.atMostKEncoding = atMostKEncoding;
99 }
100
101 public void setAtMostKEncoding(EncodingStrategy atMostKEncoding) {
102 this.atMostKEncoding = getAdapterFromEncodingName(atMostKEncoding);
103 }
104
105 public EncodingStrategyAdapter getExactlyOneEncoding() {
106 return this.exactlyOneEncoding;
107 }
108
109 public void setExactlyOneEncoding(EncodingStrategyAdapter exactlyOneEncoding) {
110 this.exactlyOneEncoding = exactlyOneEncoding;
111 }
112
113 public void setExactlyOneEncoding(EncodingStrategy exactlyOneEncoding) {
114 this.exactlyOneEncoding = getAdapterFromEncodingName(exactlyOneEncoding);
115 }
116
117 public EncodingStrategyAdapter getExactlyKEncoding() {
118 return this.exactlyKEncoding;
119 }
120
121 public void setExactlyKEncoding(EncodingStrategyAdapter exactlyKEncoding) {
122 this.exactlyKEncoding = exactlyKEncoding;
123 }
124
125 public void setExactlyKEncoding(EncodingStrategy exactlyKEncoding) {
126 this.exactlyKEncoding = getAdapterFromEncodingName(exactlyKEncoding);
127 }
128
129 public EncodingStrategyAdapter getAtLeastOneEncoding() {
130 return this.atLeastOneEncoding;
131 }
132
133 public void setAtLeastOneEncoding(EncodingStrategyAdapter atLeastOneEncoding) {
134 this.atLeastOneEncoding = atLeastOneEncoding;
135 }
136
137 public void setAtLeastOneEncoding(EncodingStrategy atLeastOneEncoding) {
138 this.atLeastOneEncoding = getAdapterFromEncodingName(atLeastOneEncoding);
139 }
140
141 public EncodingStrategyAdapter getAtLeastKEncoding() {
142 return this.atLeastKEncoding;
143 }
144
145 public void setAtLeastKEncoding(EncodingStrategyAdapter atLeastKEncoding) {
146 this.atLeastKEncoding = atLeastKEncoding;
147 }
148
149 public void setAtLeastKEncoding(EncodingStrategy atLeastKEncoding) {
150 this.atLeastKEncoding = getAdapterFromEncodingName(atLeastKEncoding);
151 }
152
153 @Override
154 public IConstr addAtMost(ISolver solver, IVecInt literals, int k)
155 throws ContradictionException {
156
157 if (k == 0 || literals.size() == 1) {
158
159 return super.addAtMost(solver, literals, k);
160 }
161 if (literals.size() <= 1) {
162 throw new UnsupportedOperationException(
163 "requires at least 2 literals");
164 }
165 if (k == 1 && this.atMostOneEncoding != null) {
166 return this.atMostOneEncoding.addAtMostOne(solver, literals);
167 }
168 if (this.atMostKEncoding != null) {
169 if (k == 1) {
170 return this.atMostKEncoding.addAtMostOne(solver, literals);
171 } else {
172 return this.atMostKEncoding.addAtMost(solver, literals, k);
173 }
174 }
175 return super.addAtMost(solver, literals, k);
176 }
177
178 @Override
179 public IConstr addExactly(ISolver solver, IVecInt literals, int n)
180 throws ContradictionException {
181 if (n == 1 && this.exactlyOneEncoding != null) {
182 return this.exactlyOneEncoding.addExactlyOne(solver, literals);
183 } else if (this.exactlyKEncoding != null) {
184 if (n == 1) {
185 return this.exactlyKEncoding.addExactlyOne(solver, literals);
186 } else {
187 return this.exactlyKEncoding.addExactly(solver, literals, n);
188 }
189 }
190
191 return super.addExactly(solver, literals, n);
192 }
193
194 @Override
195 public IConstr addAtLeast(ISolver solver, IVecInt literals, int n)
196 throws ContradictionException {
197 if (n == 1) {
198 if (this.atLeastOneEncoding != null) {
199 return this.atLeastOneEncoding.addAtLeastOne(solver, literals);
200 }
201 } else if (this.atLeastKEncoding != null) {
202 return this.atLeastKEncoding.addAtLeast(solver, literals, n);
203 }
204
205 return super.addAtLeast(solver, literals, n);
206
207 }
208
209 }