1 |
| package org.sat4j.minisat.constraints; |
2 |
| |
3 |
| import java.math.BigInteger; |
4 |
| |
5 |
| import org.sat4j.core.Vec; |
6 |
| import org.sat4j.core.VecInt; |
7 |
| import org.sat4j.minisat.constraints.cnf.WLClause; |
8 |
| import org.sat4j.minisat.constraints.pb.IDataStructurePB; |
9 |
| import org.sat4j.minisat.constraints.pb.PBConstr; |
10 |
| import org.sat4j.minisat.constraints.pb.WatchPb; |
11 |
| import org.sat4j.specs.ContradictionException; |
12 |
| import org.sat4j.specs.IVec; |
13 |
| import org.sat4j.specs.IVecInt; |
14 |
| |
15 |
| public abstract class AbstractPBClauseCardConstrDataStructure extends |
16 |
| AbstractPBDataStructureFactory { |
17 |
| |
18 |
| |
19 |
| |
20 |
| |
21 |
| |
22 |
| |
23 |
| |
24 |
4150
| @Override
|
25 |
| protected PBConstr constraintFactory(IVecInt literals, IVecInt coefs, |
26 |
| boolean moreThan, int degree) throws ContradictionException { |
27 |
4150
| return constraintFactory(literals, WatchPb.toVecBigInt(coefs),
|
28 |
| moreThan, WatchPb.toBigInt(degree)); |
29 |
| } |
30 |
| |
31 |
| |
32 |
| |
33 |
| |
34 |
| |
35 |
| |
36 |
| |
37 |
0
| @Override
|
38 |
| protected PBConstr constraintFactory(IVecInt literals, IVecInt coefs, |
39 |
| int degree) { |
40 |
0
| return constraintFactory(literals, WatchPb.toVecBigInt(coefs), WatchPb
|
41 |
| .toBigInt(degree)); |
42 |
| } |
43 |
| |
44 |
| |
45 |
| |
46 |
| |
47 |
| |
48 |
| |
49 |
| |
50 |
841834
| @Override
|
51 |
| protected PBConstr constraintFactory(IVecInt literals, |
52 |
| IVec<BigInteger> coefs, boolean moreThan, BigInteger degree) |
53 |
| throws ContradictionException { |
54 |
841834
| IDataStructurePB mpb = WatchPb.niceParameters(literals, coefs,
|
55 |
| moreThan, degree, getVocabulary()); |
56 |
841834
| if (mpb == null)
|
57 |
0
| return null;
|
58 |
841834
| int size = mpb.size();
|
59 |
841834
| int[] lits = new int[size];
|
60 |
841834
| BigInteger[] normCoefs = new BigInteger[size];
|
61 |
841834
| mpb.buildConstraintFromMapPb(lits, normCoefs);
|
62 |
841834
| if (mpb.getDegree().equals(BigInteger.ONE)) {
|
63 |
444424
| IVecInt v = WLClause.sanityCheck(new VecInt(lits), getVocabulary(),
|
64 |
| solver); |
65 |
444424
| if (v == null)
|
66 |
1026
| return null;
|
67 |
443398
| return constructClause(v);
|
68 |
| } |
69 |
397410
| if (coefficientsEqualToOne(new Vec<BigInteger>(normCoefs))) {
|
70 |
| assert mpb.getDegree().compareTo(new BigInteger(String.valueOf(Integer.MAX_VALUE))) < 0; |
71 |
27618
| return constructCard(new VecInt(lits), mpb.getDegree().intValue());
|
72 |
| } |
73 |
369792
| return constructPB(mpb);
|
74 |
| } |
75 |
| |
76 |
| |
77 |
| |
78 |
| |
79 |
| |
80 |
| |
81 |
| |
82 |
279930
| @Override
|
83 |
| protected PBConstr constraintFactory(IVecInt literals, |
84 |
| IVec<BigInteger> coefs, BigInteger degree) { |
85 |
279930
| if (degree.equals(BigInteger.ONE)) {
|
86 |
246930
| return constructLearntClause(literals);
|
87 |
| } |
88 |
33000
| if (coefficientsEqualToOne(coefs)) {
|
89 |
5106
| return constructLearntCard(literals, degree.intValue());
|
90 |
| } |
91 |
27894
| return constructLearntPB(literals, coefs, degree);
|
92 |
| } |
93 |
| |
94 |
430410
| private static boolean coefficientsEqualToOne(IVec<BigInteger> coeffs) {
|
95 |
430410
| for (int i = 0; i < coeffs.size(); i++)
|
96 |
3758679
| if (!coeffs.get(i).equals(BigInteger.ONE))
|
97 |
397686
| return false;
|
98 |
32724
| return true;
|
99 |
| } |
100 |
| |
101 |
| abstract protected PBConstr constructClause(IVecInt v); |
102 |
| |
103 |
| abstract protected PBConstr constructCard(IVecInt lits, int degree) |
104 |
| throws ContradictionException; |
105 |
| |
106 |
| abstract protected PBConstr constructPB(IDataStructurePB mpb) |
107 |
| throws ContradictionException; |
108 |
| |
109 |
| abstract protected PBConstr constructLearntClause(IVecInt literals); |
110 |
| |
111 |
| abstract protected PBConstr constructLearntCard(IVecInt literals, int degree); |
112 |
| |
113 |
| abstract protected PBConstr constructLearntPB(IVecInt literals, |
114 |
| IVec<BigInteger> coefs, BigInteger degree); |
115 |
| |
116 |
| } |