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
32 import org.sat4j.core.Vec;
33 import org.sat4j.minisat.core.ILits;
34 import org.sat4j.specs.ContradictionException;
35 import org.sat4j.specs.IVec;
36 import org.sat4j.specs.IVecInt;
37
38 public abstract class Pseudos {
39
40 public static IDataStructurePB niceCheckedParameters(IVecInt ps,
41 IVec<BigInteger> bigCoefs, boolean moreThan, BigInteger bigDeg,
42 ILits voc) {
43 assert ps.size() != 0 && ps.size() == bigCoefs.size();
44 int[] lits = new int[ps.size()];
45 ps.copyTo(lits);
46 BigInteger[] bc = new BigInteger[bigCoefs.size()];
47 bigCoefs.copyTo(bc);
48 BigInteger bigDegree = Pseudos.niceCheckedParametersForCompetition(
49 lits, bc, moreThan, bigDeg);
50
51 IDataStructurePB mpb = new MapPb(voc.nVars() * 2 + 2);
52 if (bigDegree.signum() > 0)
53 bigDegree = mpb.cuttingPlane(lits, bc, bigDegree);
54 if (bigDegree.signum() > 0)
55 bigDegree = mpb.saturation();
56 if (bigDegree.signum() <= 0)
57 return null;
58 return mpb;
59 }
60
61 public static BigInteger niceCheckedParametersForCompetition(int[] lits,
62 BigInteger[] bc, boolean moreThan, BigInteger bigDeg) {
63 BigInteger bigDegree = bigDeg;
64 if (!moreThan) {
65 for (int i = 0; i < lits.length; i++) {
66 bc[i] = bc[i].negate();
67 }
68 bigDegree = bigDegree.negate();
69 }
70
71 for (int i = 0; i < bc.length; i++)
72 if (bc[i].signum() < 0) {
73 lits[i] = lits[i] ^ 1;
74 bc[i] = bc[i].negate();
75 bigDegree = bigDegree.add(bc[i]);
76 }
77
78 for (int i = 0; i < bc.length; i++)
79 if (bc[i].compareTo(bigDegree) > 0)
80 bc[i] = bigDegree;
81
82 return bigDegree;
83
84 }
85
86 public static IDataStructurePB niceParameters(IVecInt ps,
87 IVec<BigInteger> bigCoefs, boolean moreThan, BigInteger bigDeg,
88 ILits voc) throws ContradictionException {
89
90 if (ps.size() == 0) {
91 throw new ContradictionException("Creating Empty clause ?");
92 } else if (ps.size() != bigCoefs.size()) {
93 throw new IllegalArgumentException(
94 "Contradiction dans la taille des tableaux ps=" + ps.size()
95 + " coefs=" + bigCoefs.size() + ".");
96 }
97 return niceCheckedParameters(ps, bigCoefs, moreThan, bigDeg, voc);
98 }
99
100 public static BigInteger niceParametersForCompetition(int[] ps,
101 BigInteger[] bigCoefs, boolean moreThan, BigInteger bigDeg)
102 throws ContradictionException {
103
104 if (ps.length == 0) {
105 throw new ContradictionException("Creating Empty clause ?");
106 } else if (ps.length != bigCoefs.length) {
107 throw new IllegalArgumentException(
108 "Contradiction dans la taille des tableaux ps=" + ps.length
109 + " coefs=" + bigCoefs.length + ".");
110 }
111 return niceCheckedParametersForCompetition(ps, bigCoefs, moreThan,
112 bigDeg);
113 }
114
115 public static IVec<BigInteger> toVecBigInt(IVecInt vec) {
116 IVec<BigInteger> bigVec = new Vec<BigInteger>(vec.size());
117 for (int i = 0; i < vec.size(); ++i)
118 bigVec.push(BigInteger.valueOf(vec.get(i)));
119 return bigVec;
120 }
121
122 public static BigInteger toBigInt(int i) {
123 return BigInteger.valueOf(i);
124 }
125
126 }