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 |
|
package org.sat4j.opt; |
27 |
|
|
28 |
|
import java.math.BigInteger; |
29 |
|
|
30 |
|
import org.sat4j.core.Vec; |
31 |
|
import org.sat4j.core.VecInt; |
32 |
|
import org.sat4j.specs.ContradictionException; |
33 |
|
import org.sat4j.specs.IConstr; |
34 |
|
import org.sat4j.specs.IOptimizationProblem; |
35 |
|
import org.sat4j.specs.ISolver; |
36 |
|
import org.sat4j.specs.IVec; |
37 |
|
import org.sat4j.specs.IVecInt; |
38 |
|
|
|
|
| 0% |
Uncovered Elements: 38 (38) |
Complexity: 6 |
Complexity Density: 0,59 |
|
39 |
|
public class WeightedMaxSatDecorator extends AbstractSelectorVariablesDecorator |
40 |
|
implements IOptimizationProblem { |
41 |
|
|
42 |
|
|
43 |
|
|
44 |
|
|
45 |
|
private static final long serialVersionUID = 1L; |
46 |
|
|
47 |
|
private final IVec<BigInteger> coefs = new Vec<BigInteger>(); |
48 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
49 |
0
|
public WeightedMaxSatDecorator(ISolver solver) {... |
50 |
0
|
super(solver); |
51 |
|
} |
52 |
|
|
53 |
|
|
54 |
|
protected int top = -1; |
55 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
56 |
0
|
public void setTopWeight(int top) {... |
57 |
0
|
this.top = top; |
58 |
|
} |
59 |
|
|
|
|
| 0% |
Uncovered Elements: 8 (8) |
Complexity: 2 |
Complexity Density: 0,33 |
|
60 |
0
|
@Override... |
61 |
|
public IConstr addClause(IVecInt literals) throws ContradictionException { |
62 |
0
|
int weight = literals.get(0); |
63 |
0
|
if (weight<top) { |
64 |
0
|
coefs.push(BigInteger.valueOf(weight)); |
65 |
0
|
literals.set(0, nborigvars + ++nbnewvar); |
66 |
|
} else { |
67 |
0
|
literals.delete(0); |
68 |
|
} |
69 |
0
|
return super.addClause(literals); |
70 |
|
} |
71 |
|
|
|
|
| 0% |
Uncovered Elements: 3 (3) |
Complexity: 1 |
Complexity Density: 0,33 |
|
72 |
0
|
@Override... |
73 |
|
public void reset() { |
74 |
0
|
coefs.clear(); |
75 |
0
|
vec.clear(); |
76 |
0
|
super.reset(); |
77 |
|
} |
78 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
79 |
0
|
public boolean hasNoObjectiveFunction() {... |
80 |
0
|
return false; |
81 |
|
} |
82 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
83 |
0
|
public boolean nonOptimalMeansSatisfiable() {... |
84 |
0
|
return false; |
85 |
|
} |
86 |
|
|
87 |
|
private BigInteger counter; |
88 |
|
|
|
|
| 0% |
Uncovered Elements: 7 (7) |
Complexity: 3 |
Complexity Density: 0,6 |
|
89 |
0
|
public Number calculateObjective() {... |
90 |
0
|
counter = BigInteger.ZERO; |
91 |
0
|
for (int q : prevfullmodel) { |
92 |
0
|
if (q > nborigvars) { |
93 |
0
|
counter = counter.add(coefs.get(q - nborigvars - 1)); |
94 |
|
} |
95 |
|
} |
96 |
0
|
return counter; |
97 |
|
} |
98 |
|
|
99 |
|
private final IVecInt vec = new VecInt(); |
100 |
|
|
101 |
|
|
102 |
|
|
|
|
| 0% |
Uncovered Elements: 8 (8) |
Complexity: 3 |
Complexity Density: 0,75 |
|
103 |
0
|
public void discard() throws ContradictionException {... |
104 |
0
|
if (vec.isEmpty()) { |
105 |
0
|
for (int i = 1; i <= nbnewvar; i++) { |
106 |
0
|
vec.push(nborigvars+i); |
107 |
|
} |
108 |
|
} |
109 |
|
|
110 |
|
|
111 |
|
|
112 |
|
|
113 |
0
|
super.addPseudoBoolean(vec, coefs, false, counter |
114 |
|
.subtract(BigInteger.ONE)); |
115 |
|
} |
116 |
|
|
117 |
|
} |