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 org.sat4j.core.VecInt; |
29 |
|
import org.sat4j.specs.ContradictionException; |
30 |
|
import org.sat4j.specs.IConstr; |
31 |
|
import org.sat4j.specs.IOptimizationProblem; |
32 |
|
import org.sat4j.specs.ISolver; |
33 |
|
import org.sat4j.specs.IVecInt; |
34 |
|
|
|
|
| 0% |
Uncovered Elements: 30 (30) |
Complexity: 5 |
Complexity Density: 0,65 |
|
35 |
|
public class MaxSatDecorator extends AbstractSelectorVariablesDecorator |
36 |
|
implements IOptimizationProblem { |
37 |
|
|
38 |
|
|
39 |
|
|
40 |
|
|
41 |
|
private static final long serialVersionUID = 1L; |
42 |
|
|
43 |
|
|
44 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
45 |
0
|
public MaxSatDecorator(ISolver solver) {... |
46 |
0
|
super(solver); |
47 |
|
} |
48 |
|
|
|
|
| 0% |
Uncovered Elements: 2 (2) |
Complexity: 1 |
Complexity Density: 0,5 |
|
49 |
0
|
@Override... |
50 |
|
public IConstr addClause(IVecInt literals) throws ContradictionException { |
51 |
0
|
literals.push(nborigvars + ++nbnewvar); |
52 |
0
|
return super.addClause(literals); |
53 |
|
} |
54 |
|
|
|
|
| 0% |
Uncovered Elements: 3 (3) |
Complexity: 1 |
Complexity Density: 0,33 |
|
55 |
0
|
@Override... |
56 |
|
public void reset() { |
57 |
0
|
nbnewvar = 0; |
58 |
0
|
vec.clear(); |
59 |
0
|
super.reset(); |
60 |
|
} |
61 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
62 |
0
|
public boolean hasNoObjectiveFunction() {... |
63 |
0
|
return false; |
64 |
|
} |
65 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
66 |
0
|
public boolean nonOptimalMeansSatisfiable() {... |
67 |
0
|
return false; |
68 |
|
} |
69 |
|
|
|
|
| 0% |
Uncovered Elements: 7 (7) |
Complexity: 3 |
Complexity Density: 0,6 |
|
70 |
0
|
public Number calculateObjective() {... |
71 |
0
|
counter = 0; |
72 |
0
|
for (int q : prevfullmodel) { |
73 |
0
|
if (q > nborigvars) { |
74 |
0
|
counter++; |
75 |
|
} |
76 |
|
} |
77 |
0
|
return counter; |
78 |
|
} |
79 |
|
|
80 |
|
private final IVecInt vec = new VecInt(); |
81 |
|
|
82 |
|
private int counter; |
83 |
|
|
|
|
| 0% |
Uncovered Elements: 8 (8) |
Complexity: 3 |
Complexity Density: 0,75 |
|
84 |
0
|
public void discard() throws ContradictionException {... |
85 |
0
|
if (vec.isEmpty()) { |
86 |
0
|
for (int i = nborigvars + 1; i <= nVars(); i++) { |
87 |
0
|
vec.push(i); |
88 |
|
} |
89 |
|
} |
90 |
|
|
91 |
|
|
92 |
|
|
93 |
0
|
super.addAtMost(vec, counter - 1); |
94 |
|
} |
95 |
|
|
96 |
|
} |