|
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 |
| } |
