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