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 package org.sat4j.pb.constraints;
31
32 import java.lang.reflect.Field;
33 import java.math.BigInteger;
34
35 import org.sat4j.core.Vec;
36 import org.sat4j.core.VecInt;
37 import org.sat4j.minisat.constraints.AbstractDataStructureFactory;
38 import org.sat4j.minisat.constraints.cnf.Clauses;
39 import org.sat4j.minisat.constraints.cnf.LearntBinaryClause;
40 import org.sat4j.minisat.constraints.cnf.LearntHTClause;
41 import org.sat4j.minisat.constraints.cnf.Lits;
42 import org.sat4j.minisat.constraints.cnf.OriginalBinaryClause;
43 import org.sat4j.minisat.constraints.cnf.OriginalHTClause;
44 import org.sat4j.minisat.constraints.cnf.UnitClause;
45 import org.sat4j.minisat.core.Constr;
46 import org.sat4j.minisat.core.ILits;
47 import org.sat4j.pb.constraints.pb.AtLeastPB;
48 import org.sat4j.pb.constraints.pb.IDataStructurePB;
49 import org.sat4j.pb.constraints.pb.Pseudos;
50 import org.sat4j.pb.core.PBDataStructureFactory;
51 import org.sat4j.specs.ContradictionException;
52 import org.sat4j.specs.IVec;
53 import org.sat4j.specs.IVecInt;
54
55
56
57
58
59 public abstract class AbstractPBDataStructureFactory extends
60 AbstractDataStructureFactory implements PBDataStructureFactory {
61
62 interface INormalizer {
63 PBContainer nice(IVecInt ps, IVec<BigInteger> bigCoefs,
64 boolean moreThan, BigInteger bigDeg, ILits voc)
65 throws ContradictionException;
66 }
67
68 public static final INormalizer FOR_COMPETITION = new INormalizer() {
69
70 public PBContainer nice(IVecInt literals, IVec<BigInteger> coefs,
71 boolean moreThan, BigInteger degree, ILits voc)
72 throws ContradictionException {
73 if (literals.size() != coefs.size()) {
74 throw new IllegalArgumentException(
75 "Number of coeff and literals are different!!!");
76 }
77 IVecInt cliterals = new VecInt(literals.size());
78 literals.copyTo(cliterals);
79 IVec<BigInteger> ccoefs = new Vec<BigInteger>(literals.size());
80 coefs.copyTo(ccoefs);
81 for (int i = 0; i < cliterals.size();) {
82 if (ccoefs.get(i).equals(BigInteger.ZERO)) {
83 cliterals.delete(i);
84 ccoefs.delete(i);
85 } else {
86 i++;
87 }
88 }
89 int[] theLits = new int[cliterals.size()];
90 cliterals.copyTo(theLits);
91 BigInteger[] normCoefs = new BigInteger[ccoefs.size()];
92 ccoefs.copyTo(normCoefs);
93 BigInteger degRes = Pseudos.niceParametersForCompetition(theLits,
94 normCoefs, moreThan, degree);
95 return new PBContainer(theLits, normCoefs, degRes);
96
97 }
98
99 };
100
101 public static final INormalizer NO_COMPETITION = new INormalizer() {
102
103 public PBContainer nice(IVecInt literals, IVec<BigInteger> coefs,
104 boolean moreThan, BigInteger degree, ILits voc)
105 throws ContradictionException {
106 IDataStructurePB res = Pseudos.niceParameters(literals, coefs,
107 moreThan, degree, voc);
108 int size = res.size();
109 int[] theLits = new int[size];
110 BigInteger[] theCoefs = new BigInteger[size];
111 res.buildConstraintFromMapPb(theLits, theCoefs);
112 BigInteger theDegree = res.getDegree();
113 return new PBContainer(theLits, theCoefs, theDegree);
114 }
115 };
116
117 private INormalizer norm = FOR_COMPETITION;
118
119 protected INormalizer getNormalizer() {
120 return this.norm;
121 }
122
123 public void setNormalizer(String simp) {
124 Field f;
125 try {
126 f = AbstractPBDataStructureFactory.class.getDeclaredField(simp);
127 this.norm = (INormalizer) f.get(this);
128 } catch (Exception e) {
129 e.printStackTrace();
130 this.norm = FOR_COMPETITION;
131 }
132 }
133
134 public void setNormalizer(INormalizer normalizer) {
135 this.norm = normalizer;
136 }
137
138
139
140
141 private static final long serialVersionUID = 1L;
142
143 public Constr createClause(IVecInt literals) throws ContradictionException {
144 IVecInt v = Clauses.sanityCheck(literals, getVocabulary(), this.solver);
145 if (v == null) {
146
147 return null;
148 }
149 if (v.size() == 1) {
150 return new UnitClause(v.last());
151 }
152 if (v.size() == 2) {
153 return OriginalBinaryClause.brandNewClause(this.solver,
154 getVocabulary(), v);
155 }
156 return OriginalHTClause.brandNewClause(this.solver, getVocabulary(), v);
157 }
158
159 public Constr createUnregisteredClause(IVecInt literals) {
160 if (literals.size() == 1) {
161 return new UnitClause(literals.last());
162 }
163 if (literals.size() == 2) {
164 return new LearntBinaryClause(literals, getVocabulary());
165 }
166 return new LearntHTClause(literals, getVocabulary());
167 }
168
169 @Override
170 public Constr createCardinalityConstraint(IVecInt literals, int degree)
171 throws ContradictionException {
172 return AtLeastPB.atLeastNew(this.solver, getVocabulary(), literals,
173 degree);
174 }
175
176 public Constr createPseudoBooleanConstraint(IVecInt literals,
177 IVec<BigInteger> coefs, boolean moreThan, BigInteger degree)
178 throws ContradictionException {
179 PBContainer res = getNormalizer().nice(literals, coefs, moreThan,
180 degree, getVocabulary());
181 return constraintFactory(res.lits, res.coefs, res.degree);
182 }
183
184 public Constr createAtMostPBConstraint(IVecInt literals,
185 IVec<BigInteger> coefs, BigInteger degree)
186 throws ContradictionException {
187 return createPseudoBooleanConstraint(literals, coefs, false, degree);
188 }
189
190 public Constr createAtLeastPBConstraint(IVecInt literals,
191 IVec<BigInteger> coefs, BigInteger degree)
192 throws ContradictionException {
193 return createPseudoBooleanConstraint(literals, coefs, true, degree);
194 }
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224 public Constr createUnregisteredPseudoBooleanConstraint(
225 IDataStructurePB dspb) {
226 return learntConstraintFactory(dspb);
227 }
228
229 protected abstract Constr constraintFactory(int[] literals,
230 BigInteger[] coefs, BigInteger degree)
231 throws ContradictionException;
232
233 protected abstract Constr learntConstraintFactory(IDataStructurePB dspb);
234
235 @Override
236 protected ILits createLits() {
237 return new Lits();
238 }
239
240 }