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.pb;
31
32 import java.math.BigInteger;
33 import java.util.HashMap;
34 import java.util.Map;
35
36 import org.sat4j.core.Vec;
37 import org.sat4j.core.VecInt;
38 import org.sat4j.minisat.core.ILits;
39 import org.sat4j.pb.ObjectiveFunction;
40 import org.sat4j.specs.ContradictionException;
41 import org.sat4j.specs.IVec;
42 import org.sat4j.specs.IVecInt;
43
44 public abstract class Pseudos {
45
46 public static IDataStructurePB niceCheckedParameters(IVecInt ps,
47 IVec<BigInteger> bigCoefs, boolean moreThan, BigInteger bigDeg,
48 ILits voc) {
49 assert ps.size() != 0 && ps.size() == bigCoefs.size();
50 int[] lits = new int[ps.size()];
51 ps.copyTo(lits);
52 BigInteger[] bc = new BigInteger[bigCoefs.size()];
53 bigCoefs.copyTo(bc);
54 BigInteger bigDegree = Pseudos.niceCheckedParametersForCompetition(
55 lits, bc, moreThan, bigDeg);
56
57 IDataStructurePB mpb = new MapPb(voc.nVars() * 2 + 2);
58 if (bigDegree.signum() > 0) {
59 bigDegree = mpb.cuttingPlane(lits, bc, bigDegree);
60 }
61 if (bigDegree.signum() > 0) {
62 bigDegree = mpb.saturation();
63 }
64 if (bigDegree.signum() <= 0) {
65 return null;
66 }
67 return mpb;
68 }
69
70 public static BigInteger niceCheckedParametersForCompetition(int[] lits,
71 BigInteger[] bc, boolean moreThan, BigInteger bigDeg) {
72 BigInteger bigDegree = bigDeg;
73 if (!moreThan) {
74 for (int i = 0; i < lits.length; i++) {
75 bc[i] = bc[i].negate();
76 }
77 bigDegree = bigDegree.negate();
78 }
79
80 for (int i = 0; i < bc.length; i++) {
81 if (bc[i].signum() < 0) {
82 lits[i] = lits[i] ^ 1;
83 bc[i] = bc[i].negate();
84 bigDegree = bigDegree.add(bc[i]);
85 }
86 }
87
88 for (int i = 0; i < bc.length; i++) {
89 if (bc[i].compareTo(bigDegree) > 0) {
90 bc[i] = bigDegree;
91 }
92 }
93
94 return bigDegree;
95
96 }
97
98 public static IDataStructurePB niceParameters(IVecInt ps,
99 IVec<BigInteger> bigCoefs, boolean moreThan, BigInteger bigDeg,
100 ILits voc) throws ContradictionException {
101
102 if (ps.size() == 0 && bigDeg.signum() > 0) {
103 throw new ContradictionException("Creating Empty clause ?");
104 } else if (ps.size() != bigCoefs.size()) {
105 throw new IllegalArgumentException(
106 "Contradiction dans la taille des tableaux ps=" + ps.size()
107 + " coefs=" + bigCoefs.size() + ".");
108 }
109 return niceCheckedParameters(ps, bigCoefs, moreThan, bigDeg, voc);
110 }
111
112 public static BigInteger niceParametersForCompetition(int[] ps,
113 BigInteger[] bigCoefs, boolean moreThan, BigInteger bigDeg)
114 throws ContradictionException {
115
116 if (ps.length == 0 && bigDeg.signum() > 0) {
117 throw new ContradictionException("Creating Empty clause ?");
118 } else if (ps.length != bigCoefs.length) {
119 throw new IllegalArgumentException(
120 "Contradiction dans la taille des tableaux ps=" + ps.length
121 + " coefs=" + bigCoefs.length + ".");
122 }
123 return niceCheckedParametersForCompetition(ps, bigCoefs, moreThan,
124 bigDeg);
125 }
126
127 public static IVec<BigInteger> toVecBigInt(IVecInt vec) {
128 IVec<BigInteger> bigVec = new Vec<BigInteger>(vec.size());
129 for (int i = 0; i < vec.size(); ++i) {
130 bigVec.push(BigInteger.valueOf(vec.get(i)));
131 }
132 return bigVec;
133 }
134
135 public static BigInteger toBigInt(int i) {
136 return BigInteger.valueOf(i);
137 }
138
139 public static ObjectiveFunction normalizeObjective(ObjectiveFunction initial) {
140 IVec<BigInteger> initCoeffs = initial.getCoeffs();
141 IVecInt initLits = initial.getVars();
142 assert initCoeffs.size() == initLits.size();
143 Map<Integer, BigInteger> reduced = new HashMap<Integer, BigInteger>();
144 int lit;
145 for (int i = 0; i < initLits.size(); i++) {
146 lit = initLits.get(i);
147 BigInteger oldCoef = reduced.get(lit);
148 if (oldCoef == null) {
149 reduced.put(lit, initCoeffs.get(i));
150 } else {
151 reduced.put(lit, oldCoef.add(initCoeffs.get(i)));
152 }
153 }
154 assert reduced.size() <= initLits.size();
155 if (reduced.size() < initLits.size()) {
156 IVecInt newLits = new VecInt(reduced.size());
157 IVec<BigInteger> newCoefs = new Vec<BigInteger>(reduced.size());
158 for (Map.Entry<Integer, BigInteger> entry : reduced.entrySet()) {
159 newLits.push(entry.getKey());
160 newCoefs.push(entry.getValue());
161 }
162 return new ObjectiveFunction(newLits, newCoefs);
163 }
164 return initial;
165 }
166
167 }