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 package org.sat4j.opt;
29
30 import org.sat4j.core.VecInt;
31 import org.sat4j.specs.ContradictionException;
32 import org.sat4j.specs.IConstr;
33 import org.sat4j.specs.IOptimizationProblem;
34 import org.sat4j.specs.ISolver;
35 import org.sat4j.specs.IVecInt;
36 import org.sat4j.specs.TimeoutException;
37 import org.sat4j.tools.SolverDecorator;
38
39
40
41
42
43
44
45
46 public final class MinOneDecorator extends SolverDecorator<ISolver> implements
47 IOptimizationProblem {
48
49
50
51
52 private static final long serialVersionUID = 1L;
53
54 private int[] prevmodel;
55
56 private boolean isSolutionOptimal;
57
58 public MinOneDecorator(ISolver solver) {
59 super(solver);
60 }
61
62 public boolean admitABetterSolution() throws TimeoutException {
63 return admitABetterSolution(VecInt.EMPTY);
64 }
65
66
67
68
69 public boolean admitABetterSolution(IVecInt assumps)
70 throws TimeoutException {
71 isSolutionOptimal = false;
72 boolean result = isSatisfiable(assumps, true);
73 if (result) {
74 prevmodel = super.model();
75 calculateObjectiveValue();
76 } else {
77 isSolutionOptimal = true;
78 }
79 return result;
80 }
81
82 public boolean hasNoObjectiveFunction() {
83 return false;
84 }
85
86 public boolean nonOptimalMeansSatisfiable() {
87 return true;
88 }
89
90 private int counter;
91
92 public Number calculateObjective() {
93 calculateObjectiveValue();
94 return counter;
95 }
96
97 private void calculateObjectiveValue() {
98 counter = 0;
99 for (int p : prevmodel) {
100 if (p > 0) {
101 counter++;
102 }
103 }
104 }
105
106 private final IVecInt literals = new VecInt();
107
108 private IConstr previousConstr;
109
110
111
112
113 public void discardCurrentSolution() throws ContradictionException {
114 if (literals.isEmpty()) {
115 for (int i = 1; i <= nVars(); i++) {
116 literals.push(i);
117 }
118 }
119 if (previousConstr != null) {
120 super.removeConstr(previousConstr);
121 }
122 previousConstr = addAtMost(literals, counter - 1);
123 }
124
125 @Override
126 public int[] model() {
127
128 return prevmodel;
129 }
130
131 @Override
132 public void reset() {
133 literals.clear();
134 previousConstr = null;
135 super.reset();
136 }
137
138
139
140
141 public Number getObjectiveValue() {
142 return counter;
143 }
144
145 public void discard() throws ContradictionException {
146 discardCurrentSolution();
147 }
148
149
150
151
152 public void forceObjectiveValueTo(Number forcedValue)
153 throws ContradictionException {
154 try {
155 addAtMost(literals, forcedValue.intValue());
156 } catch (ContradictionException ce) {
157 isSolutionOptimal = true;
158 throw ce;
159 }
160
161 }
162
163 public boolean isOptimal() {
164 return isSolutionOptimal;
165 }
166 }