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(lits,bc,moreThan,bigDeg);
49
50 IDataStructurePB mpb = new MapPb(voc.nVars()*2+2);
51 if (bigDegree.signum() > 0)
52 bigDegree = mpb.cuttingPlane(lits, bc, bigDegree);
53 if (bigDegree.signum() > 0)
54 bigDegree = mpb.saturation();
55 if (bigDegree.signum() <= 0)
56 return null;
57 return mpb;
58 }
59
60 public static BigInteger niceCheckedParametersForCompetition(int[] lits,
61 BigInteger[] bc, boolean moreThan, BigInteger bigDeg) {
62 BigInteger bigDegree = bigDeg;
63 if (!moreThan) {
64 for (int i = 0; i < lits.length; i++) {
65 bc[i] = bc[i].negate();
66 }
67 bigDegree = bigDegree.negate();
68 }
69
70 for (int i = 0; i < bc.length; i++)
71 if (bc[i].signum() < 0) {
72 lits[i] = lits[i] ^ 1;
73 bc[i] = bc[i].negate();
74 bigDegree = bigDegree.add(bc[i]);
75 }
76
77 for (int i = 0; i < bc.length; i++)
78 if (bc[i].compareTo(bigDegree) > 0)
79 bc[i] = bigDegree;
80
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, bigDeg);
112 }
113
114 public static IVec<BigInteger> toVecBigInt(IVecInt vec) {
115 IVec<BigInteger> bigVec = new Vec<BigInteger>(vec.size());
116 for (int i = 0; i < vec.size(); ++i)
117 bigVec.push(BigInteger.valueOf(vec.get(i)));
118 return bigVec;
119 }
120
121 }