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
29
30 package org.sat4j.pb.tools;
31
32 import java.math.BigInteger;
33
34 import org.sat4j.pb.IPBSolver;
35 import org.sat4j.pb.ObjectiveFunction;
36 import org.sat4j.specs.ContradictionException;
37 import org.sat4j.specs.IConstr;
38 import org.sat4j.specs.IVec;
39 import org.sat4j.specs.IVecInt;
40 import org.sat4j.tools.ClausalCardinalitiesDecorator;
41 import org.sat4j.tools.encoding.EncodingStrategyAdapter;
42 import org.sat4j.tools.encoding.Policy;
43
44 public class ClausalConstraintsDecorator extends
45 ClausalCardinalitiesDecorator<IPBSolver> implements IPBSolver {
46
47
48
49
50 private static final long serialVersionUID = 1L;
51
52 private final IPBSolver solver;
53
54 public ClausalConstraintsDecorator(IPBSolver solver,
55 EncodingStrategyAdapter encodingAd) {
56 super(solver, encodingAd);
57 this.solver = solver;
58 }
59
60 public ClausalConstraintsDecorator(IPBSolver solver) {
61 super(solver, new Policy());
62 this.solver = solver;
63 }
64
65 public IConstr addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs,
66 boolean moreThan, BigInteger d) throws ContradictionException {
67 if (isCardinality(coeffs)) {
68 if (moreThan) {
69 return super.addAtLeast(lits, d.intValue());
70 } else {
71 return super.addAtMost(lits, d.intValue());
72 }
73 } else {
74 return solver.addPseudoBoolean(lits, coeffs, moreThan, d);
75 }
76 }
77
78 public void setObjectiveFunction(ObjectiveFunction obj) {
79 solver.setObjectiveFunction(obj);
80 }
81
82 public ObjectiveFunction getObjectiveFunction() {
83 return solver.getObjectiveFunction();
84 }
85
86 public IConstr addAtMost(IVecInt literals, IVecInt coeffs, int degree)
87 throws ContradictionException {
88 if (isCardinality(coeffs)) {
89 return super.addAtMost(literals, degree);
90 } else {
91 return solver.addAtMost(literals, coeffs, degree);
92 }
93 }
94
95 public IConstr addAtMost(IVecInt literals, IVec<BigInteger> coeffs,
96 BigInteger degree) throws ContradictionException {
97 if (isCardinality(coeffs)) {
98 return super.addAtMost(literals, degree.intValue());
99 } else {
100 return solver.addAtMost(literals, coeffs, degree);
101 }
102 }
103
104 public IConstr addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
105 throws ContradictionException {
106 if (isCardinality(coeffs)) {
107 return super.addAtLeast(literals, degree);
108 } else {
109 return solver.addAtLeast(literals, coeffs, degree);
110 }
111 }
112
113 public IConstr addAtLeast(IVecInt literals, IVec<BigInteger> coeffs,
114 BigInteger degree) throws ContradictionException {
115 if (isCardinality(coeffs)) {
116 return super.addAtLeast(literals, degree.intValue());
117 } else {
118 return solver.addAtLeast(literals, coeffs, degree);
119 }
120 }
121
122 public IConstr addExactly(IVecInt literals, IVecInt coeffs, int weight)
123 throws ContradictionException {
124 if (isCardinality(coeffs)) {
125 return super.addExactly(literals, weight);
126 } else {
127 return solver.addExactly(literals, coeffs, weight);
128 }
129 }
130
131 public IConstr addExactly(IVecInt literals, IVec<BigInteger> coeffs,
132 BigInteger weight) throws ContradictionException {
133 if (isCardinality(coeffs)) {
134 return super.addExactly(literals, weight.intValue());
135 } else {
136 return solver.addExactly(literals, coeffs, weight);
137 }
138 }
139
140 public static boolean isCardinality(IVecInt coeffs) {
141 boolean result = true;
142 int i = 0;
143 while (result && i < coeffs.size()) {
144 result = (coeffs.get(i) == 1);
145 i++;
146 }
147 return result;
148 }
149
150 public static boolean isCardinality(IVec<BigInteger> coeffs) {
151 boolean result = true;
152 int i = 0;
153 while (result && i < coeffs.size()) {
154 result = (coeffs.get(i) == BigInteger.ONE);
155 i++;
156 }
157 return result;
158 }
159 }