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.pb.tools;
29
30 import java.math.BigInteger;
31 import java.util.ArrayList;
32 import java.util.List;
33
34 import org.sat4j.core.Vec;
35 import org.sat4j.pb.IPBSolver;
36 import org.sat4j.pb.ObjectiveFunction;
37 import org.sat4j.specs.ContradictionException;
38 import org.sat4j.specs.IConstr;
39 import org.sat4j.specs.IVec;
40 import org.sat4j.specs.IVecInt;
41 import org.sat4j.specs.TimeoutException;
42 import org.sat4j.tools.LexicoDecorator;
43
44 public class LexicoDecoratorPB extends LexicoDecorator<IPBSolver> implements
45 IPBSolver {
46
47
48
49
50 private static final long serialVersionUID = 1L;
51
52 private final List<ObjectiveFunction> objs = new ArrayList<ObjectiveFunction>();
53 private BigInteger bigCurrentValue;
54
55 public LexicoDecoratorPB(IPBSolver solver) {
56 super(solver);
57 }
58
59 public IConstr addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs,
60 boolean moreThan, BigInteger d) throws ContradictionException {
61 return decorated().addPseudoBoolean(lits, coeffs, moreThan, d);
62 }
63
64 public void setObjectiveFunction(ObjectiveFunction obj) {
65 throw new UnsupportedOperationException();
66
67 }
68
69 public ObjectiveFunction getObjectiveFunction() {
70 throw new UnsupportedOperationException();
71 }
72
73 @Override
74 public boolean admitABetterSolution(IVecInt assumps)
75 throws TimeoutException {
76 decorated().setObjectiveFunction(objs.get(currentCriterion));
77 return super.admitABetterSolution(assumps);
78 }
79
80 @Override
81 public void addCriterion(IVecInt literals) {
82 objs.add(new ObjectiveFunction(literals, new Vec<BigInteger>(literals
83 .size(), BigInteger.ONE)));
84 }
85
86 public void addCriterion(IVecInt literals, IVec<BigInteger> coefs) {
87 objs.add(new ObjectiveFunction(literals, coefs));
88 }
89
90 @Override
91 protected Number evaluate() {
92 bigCurrentValue = objs.get(currentCriterion).calculateDegree(this);
93 return bigCurrentValue;
94 }
95
96 @Override
97 protected void fixCriterionValue() throws ContradictionException {
98 addPseudoBoolean(objs.get(currentCriterion).getVars(),
99 objs.get(currentCriterion).getCoeffs(), true, bigCurrentValue);
100 addPseudoBoolean(objs.get(currentCriterion).getVars(),
101 objs.get(currentCriterion).getCoeffs(), false, bigCurrentValue);
102 }
103
104 @Override
105 protected IConstr discardSolutionsForOptimizing()
106 throws ContradictionException {
107 return addPseudoBoolean(objs.get(currentCriterion).getVars(),
108 objs.get(currentCriterion).getCoeffs(), false,
109 bigCurrentValue.subtract(BigInteger.ONE));
110 }
111
112 @Override
113 protected int numberOfCriteria() {
114 return objs.size();
115 }
116
117 public IConstr addAtMost(IVecInt literals, IVecInt coeffs, int degree)
118 throws ContradictionException {
119 throw new UnsupportedOperationException();
120 }
121
122 public IConstr addAtMost(IVecInt literals, IVec<BigInteger> coeffs,
123 BigInteger degree) throws ContradictionException {
124 throw new UnsupportedOperationException();
125 }
126
127 public IConstr addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
128 throws ContradictionException {
129 throw new UnsupportedOperationException();
130 }
131
132 public IConstr addAtLeast(IVecInt literals, IVec<BigInteger> coeffs,
133 BigInteger degree) throws ContradictionException {
134 throw new UnsupportedOperationException();
135 }
136
137 public IConstr addExactly(IVecInt literals, IVecInt coeffs, int weight)
138 throws ContradictionException {
139 throw new UnsupportedOperationException();
140 }
141
142 public IConstr addExactly(IVecInt literals, IVec<BigInteger> coeffs,
143 BigInteger weight) throws ContradictionException {
144 throw new UnsupportedOperationException();
145 }
146
147 }