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