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.math.BigInteger;
33
34 import org.sat4j.core.Vec;
35 import org.sat4j.core.VecInt;
36 import org.sat4j.minisat.constraints.cnf.Clauses;
37 import org.sat4j.minisat.core.Constr;
38 import org.sat4j.pb.constraints.pb.IDataStructurePB;
39 import org.sat4j.pb.constraints.pb.MapPb;
40 import org.sat4j.pb.constraints.pb.Pseudos;
41 import org.sat4j.specs.ContradictionException;
42 import org.sat4j.specs.IVec;
43 import org.sat4j.specs.IVecInt;
44
45 public abstract class AbstractPBClauseCardConstrDataStructure extends
46 AbstractPBDataStructureFactory {
47
48
49
50
51 private static final long serialVersionUID = 1L;
52
53 static final BigInteger MAX_INT_VALUE = BigInteger
54 .valueOf(Integer.MAX_VALUE);
55
56 private final IPBConstructor ipbc;
57 private final ICardConstructor icardc;
58 private final IClauseConstructor iclausec;
59
60 AbstractPBClauseCardConstrDataStructure(IClauseConstructor iclausec,
61 ICardConstructor icardc, IPBConstructor ipbc) {
62 this.iclausec = iclausec;
63 this.icardc = icardc;
64 this.ipbc = ipbc;
65 }
66
67 @Override
68 public Constr createClause(IVecInt literals) throws ContradictionException {
69 IVecInt v = Clauses.sanityCheck(literals, getVocabulary(), this.solver);
70 return constructClause(v);
71 }
72
73 @Override
74 public Constr createUnregisteredClause(IVecInt literals) {
75 return constructLearntClause(literals);
76 }
77
78
79
80
81
82
83
84
85 @Override
86 protected Constr constraintFactory(int[] literals, BigInteger[] coefs,
87 BigInteger degree) throws ContradictionException {
88 if (literals.length == 0 && degree.signum() <= 0) {
89 return null;
90 }
91 if (degree.equals(BigInteger.ONE)) {
92 IVecInt v = Clauses.sanityCheck(new VecInt(literals),
93 getVocabulary(), this.solver);
94 if (v == null) {
95 return null;
96 }
97 return constructClause(v);
98 }
99 if (coefficientsEqualToOne(coefs)) {
100 assert degree.compareTo(MAX_INT_VALUE) < 0;
101 return constructCard(new VecInt(literals), degree.intValue());
102 }
103 return constructPB(literals, coefs, degree);
104 }
105
106
107
108
109
110
111
112 @Override
113 protected Constr learntConstraintFactory(IDataStructurePB dspb) {
114 if (dspb.getDegree().equals(BigInteger.ONE)) {
115 IVecInt literals = new VecInt();
116 IVec<BigInteger> resCoefs = new Vec<BigInteger>();
117 dspb.buildConstraintFromConflict(literals, resCoefs);
118
119 int indLit = dspb.getAssertiveLiteral();
120 if (indLit > -1) {
121 int tmp = literals.get(indLit);
122 literals.set(indLit, literals.get(0));
123 literals.set(0, tmp);
124 }
125 return constructLearntClause(literals);
126 }
127 if (dspb.isCardinality()) {
128 return constructLearntCard(dspb);
129 }
130 return constructLearntPB(dspb);
131 }
132
133
134
135
136
137
138
139 private Constr learntConstraintFactory(IVecInt literals,
140 IVec<BigInteger> coefs, BigInteger degree, boolean moreThan) {
141 int[] lits = new int[literals.size()];
142 literals.copyTo(lits);
143 BigInteger[] bc = new BigInteger[coefs.size()];
144 coefs.copyTo(bc);
145 degree = Pseudos.niceCheckedParametersForCompetition(lits, bc,
146 moreThan, degree);
147
148 if (degree.equals(BigInteger.ONE)) {
149 return constructLearntClause(new VecInt(lits));
150 }
151 if (coefficientsEqualToOne(bc)) {
152 return constructLearntCard(new VecInt(lits),
153 new Vec<BigInteger>(bc), degree);
154 }
155 return constructLearntPB(new VecInt(lits), new Vec<BigInteger>(bc),
156 degree);
157 }
158
159 @Override
160 protected Constr learntAtLeastConstraintFactory(IVecInt literals,
161 IVec<BigInteger> coefs, BigInteger degree) {
162 return learntConstraintFactory(literals, coefs, degree, true);
163 }
164
165 @Override
166 protected Constr learntAtMostConstraintFactory(IVecInt literals,
167 IVec<BigInteger> coefs, BigInteger degree) {
168 return learntConstraintFactory(literals, coefs, degree, false);
169 }
170
171 static boolean coefficientsEqualToOne(BigInteger[] coefs) {
172 for (int i = 0; i < coefs.length; i++) {
173 if (!coefs[i].equals(BigInteger.ONE)) {
174 return false;
175 }
176 }
177 return true;
178 }
179
180 protected Constr constructClause(IVecInt v) {
181 return this.iclausec.constructClause(this.solver, getVocabulary(), v);
182 }
183
184 protected Constr constructCard(IVecInt theLits, int degree)
185 throws ContradictionException {
186 return this.icardc.constructCard(this.solver, getVocabulary(), theLits,
187 degree);
188 }
189
190 protected Constr constructPB(int[] theLits, BigInteger[] coefs,
191 BigInteger degree) throws ContradictionException {
192 return this.ipbc.constructPB(this.solver, getVocabulary(), theLits,
193 coefs, degree, sumOfCoefficients(coefs));
194 }
195
196 protected Constr constructLearntClause(IVecInt literals) {
197 return this.iclausec.constructLearntClause(getVocabulary(), literals);
198 }
199
200 protected Constr constructLearntCard(IDataStructurePB dspb) {
201 return this.icardc.constructLearntCard(getVocabulary(), dspb);
202 }
203
204 protected Constr constructLearntCard(IVecInt literals,
205 IVec<BigInteger> coefs, BigInteger degree) {
206 return this.icardc.constructLearntCard(getVocabulary(), new MapPb(
207 literals, coefs, degree));
208 }
209
210 protected Constr constructLearntPB(IDataStructurePB dspb) {
211 return this.ipbc.constructLearntPB(getVocabulary(), dspb);
212 }
213
214 protected Constr constructLearntPB(IVecInt literals,
215 IVec<BigInteger> coefs, BigInteger degree) {
216 return this.ipbc.constructLearntPB(getVocabulary(), new MapPb(literals,
217 coefs, degree));
218 }
219
220 public static final BigInteger sumOfCoefficients(BigInteger[] coefs) {
221 BigInteger sumCoefs = BigInteger.ZERO;
222 for (BigInteger c : coefs) {
223 sumCoefs = sumCoefs.add(c);
224 }
225 return sumCoefs;
226 }
227
228 }