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.specs.ContradictionException;
40 import org.sat4j.specs.IVec;
41 import org.sat4j.specs.IVecInt;
42
43 public abstract class AbstractPBClauseCardConstrDataStructure extends
44 AbstractPBDataStructureFactory {
45
46
47
48
49 private static final long serialVersionUID = 1L;
50
51 static final BigInteger MAX_INT_VALUE = BigInteger
52 .valueOf(Integer.MAX_VALUE);
53
54 private final IPBConstructor ipbc;
55 private final ICardConstructor icardc;
56 private final IClauseConstructor iclausec;
57
58 AbstractPBClauseCardConstrDataStructure(IClauseConstructor iclausec,
59 ICardConstructor icardc, IPBConstructor ipbc) {
60 this.iclausec = iclausec;
61 this.icardc = icardc;
62 this.ipbc = ipbc;
63 }
64
65 @Override
66 public Constr createClause(IVecInt literals) throws ContradictionException {
67 IVecInt v = Clauses.sanityCheck(literals, getVocabulary(), this.solver);
68 return constructClause(v);
69 }
70
71 @Override
72 public Constr createUnregisteredClause(IVecInt literals) {
73 return constructLearntClause(literals);
74 }
75
76
77
78
79
80
81
82
83 @Override
84 protected Constr constraintFactory(int[] literals, BigInteger[] coefs,
85 BigInteger degree) throws ContradictionException {
86 if (literals.length == 0 && degree.signum() <= 0) {
87 return null;
88 }
89 if (degree.equals(BigInteger.ONE)) {
90 IVecInt v = Clauses.sanityCheck(new VecInt(literals),
91 getVocabulary(), this.solver);
92 if (v == null) {
93 return null;
94 }
95 return constructClause(v);
96 }
97 if (coefficientsEqualToOne(coefs)) {
98 assert degree.compareTo(MAX_INT_VALUE) < 0;
99 return constructCard(new VecInt(literals), degree.intValue());
100 }
101 return constructPB(literals, coefs, degree);
102 }
103
104
105
106
107
108
109
110 @Override
111 protected Constr learntConstraintFactory(IDataStructurePB dspb) {
112 if (dspb.getDegree().equals(BigInteger.ONE)) {
113 IVecInt literals = new VecInt();
114 IVec<BigInteger> resCoefs = new Vec<BigInteger>();
115 dspb.buildConstraintFromConflict(literals, resCoefs);
116
117 int indLit = dspb.getAssertiveLiteral();
118 if (indLit > -1) {
119 int tmp = literals.get(indLit);
120 literals.set(indLit, literals.get(0));
121 literals.set(0, tmp);
122 }
123 return constructLearntClause(literals);
124 }
125 if (dspb.isCardinality()) {
126 return constructLearntCard(dspb);
127 }
128 return constructLearntPB(dspb);
129 }
130
131 static boolean coefficientsEqualToOne(BigInteger[] coefs) {
132 for (int i = 0; i < coefs.length; i++) {
133 if (!coefs[i].equals(BigInteger.ONE)) {
134 return false;
135 }
136 }
137 return true;
138 }
139
140 protected Constr constructClause(IVecInt v) {
141 return this.iclausec.constructClause(this.solver, getVocabulary(), v);
142 }
143
144 protected Constr constructCard(IVecInt theLits, int degree)
145 throws ContradictionException {
146 return this.icardc.constructCard(this.solver, getVocabulary(), theLits,
147 degree);
148 }
149
150 protected Constr constructPB(int[] theLits, BigInteger[] coefs,
151 BigInteger degree) throws ContradictionException {
152 return this.ipbc.constructPB(this.solver, getVocabulary(), theLits,
153 coefs, degree, sumOfCoefficients(coefs));
154 }
155
156 protected Constr constructLearntClause(IVecInt literals) {
157 return this.iclausec.constructLearntClause(getVocabulary(), literals);
158 }
159
160 protected Constr constructLearntCard(IDataStructurePB dspb) {
161 return this.icardc.constructLearntCard(getVocabulary(), dspb);
162 }
163
164 protected Constr constructLearntPB(IDataStructurePB dspb) {
165 return this.ipbc.constructLearntPB(getVocabulary(), dspb);
166 }
167
168 public static final BigInteger sumOfCoefficients(BigInteger[] coefs) {
169 BigInteger sumCoefs = BigInteger.ZERO;
170 for (BigInteger c : coefs) {
171 sumCoefs = sumCoefs.add(c);
172 }
173 return sumCoefs;
174 }
175
176 }