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;
31
32 import java.io.FileNotFoundException;
33 import java.io.IOException;
34 import java.math.BigInteger;
35
36 import org.sat4j.core.VecInt;
37 import org.sat4j.pb.reader.OPBReader2007;
38 import org.sat4j.reader.ParseFormatException;
39 import org.sat4j.specs.ContradictionException;
40 import org.sat4j.specs.IConstr;
41 import org.sat4j.specs.IProblem;
42 import org.sat4j.specs.IVec;
43 import org.sat4j.specs.IVecInt;
44 import org.sat4j.specs.TimeoutException;
45 import org.sat4j.tools.GateTranslator;
46 import org.sat4j.tools.SolverDecorator;
47
48
49
50
51
52
53
54 public class PseudoBitsAdderDecorator extends SolverDecorator<IPBSolver>
55 implements IPBSolver {
56
57
58
59
60 private static final long serialVersionUID = 1L;
61
62 private ObjectiveFunction objfct;
63
64 private final GateTranslator gator;
65 private final IPBSolver solver;
66
67 public PseudoBitsAdderDecorator(IPBSolver solver) {
68 super(solver);
69 this.gator = new GateTranslator(solver);
70 this.solver = solver;
71 }
72
73 public void setObjectiveFunction(ObjectiveFunction objf) {
74 this.objfct = objf;
75 }
76
77 @Override
78 public boolean isSatisfiable() throws TimeoutException {
79 return isSatisfiable(VecInt.EMPTY);
80 }
81
82 @Override
83 public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
84 if (this.objfct == null) {
85 return this.gator.isSatisfiable(assumps);
86 }
87 System.out.println("c Original number of variables and constraints");
88 System.out.println("c #vars: " + this.gator.nVars() + " #constraints: "
89 + this.gator.nConstraints());
90 IVecInt bitsLiterals = new VecInt();
91 System.out.println("c Creating optimization constraints ....");
92 try {
93 this.gator.optimisationFunction(this.objfct.getVars(),
94 this.objfct.getCoeffs(), bitsLiterals);
95 } catch (ContradictionException e) {
96 return false;
97 }
98 System.out.println("c ... done. " + bitsLiterals);
99 System.out.println("c New number of variables and constraints");
100 System.out.println("c #vars: " + this.gator.nVars() + " #constraints: "
101 + this.gator.nConstraints());
102 IVecInt fixedLiterals = new VecInt(bitsLiterals.size());
103 IVecInt nAssumpts = new VecInt(assumps.size() + bitsLiterals.size());
104 boolean result;
105 for (int litIndex = bitsLiterals.size() - 1; litIndex >= 0;) {
106 assumps.copyTo(nAssumpts);
107 fixedLiterals.copyTo(nAssumpts);
108 nAssumpts.push(-bitsLiterals.get(litIndex));
109 for (int j = litIndex - 1; j >= 0; j--) {
110 nAssumpts.push(bitsLiterals.get(j));
111 }
112 System.out.println("c assumptions " + nAssumpts);
113 result = this.gator.isSatisfiable(nAssumpts, true);
114 if (result) {
115
116
117
118
119
120
121
122
123
124 fixedLiterals.push(-bitsLiterals.get(litIndex--));
125 Number value = this.objfct.calculateDegree(this.gator);
126 System.out.println("o " + value);
127 System.out.println("c current objective value with fixed lits "
128 + fixedLiterals);
129 } else {
130 fixedLiterals.push(bitsLiterals.get(litIndex--));
131 System.out.println("c unsat. fixed lits " + fixedLiterals);
132 }
133 nAssumpts.clear();
134 }
135 assert fixedLiterals.size() == bitsLiterals.size();
136 assumps.copyTo(nAssumpts);
137 fixedLiterals.copyTo(nAssumpts);
138 return this.gator.isSatisfiable(nAssumpts);
139 }
140
141 public static void main(String[] args) {
142 PseudoBitsAdderDecorator decorator = new PseudoBitsAdderDecorator(
143 SolverFactory.newDefault());
144 decorator.setVerbose(false);
145 OPBReader2007 reader = new OPBReader2007(decorator);
146 long begin = System.currentTimeMillis();
147 try {
148 IProblem problem = reader.parseInstance(args[0]);
149 if (problem.isSatisfiable()) {
150 System.out.println("s OPTIMUM FOUND");
151 System.out.println("v " + reader.decode(problem.model()));
152 if (decorator.objfct != null) {
153 System.out
154 .println("c objective function="
155 + decorator.objfct
156 .calculateDegree(decorator.gator));
157 }
158 } else {
159 System.out.println("s UNSAT");
160 }
161 } catch (FileNotFoundException e) {
162
163 e.printStackTrace();
164 } catch (ParseFormatException e) {
165
166 e.printStackTrace();
167 } catch (IOException e) {
168
169 e.printStackTrace();
170 } catch (ContradictionException e) {
171 System.out.println("s UNSAT");
172 System.out.println("c trivial inconsistency");
173 } catch (TimeoutException e) {
174 System.out.println("s UNKNOWN");
175 }
176 long end = System.currentTimeMillis();
177 System.out.println("c Total wall clock time: " + (end - begin) / 1000.0
178 + " seconds");
179 }
180
181 public IConstr addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs,
182 boolean moreThan, BigInteger d) throws ContradictionException {
183 return this.solver.addPseudoBoolean(lits, coeffs, moreThan, d);
184 }
185
186 public ObjectiveFunction getObjectiveFunction() {
187 return this.objfct;
188 }
189
190 public IConstr addAtMost(IVecInt literals, IVecInt coeffs, int degree)
191 throws ContradictionException {
192 throw new UnsupportedOperationException();
193 }
194
195 public IConstr addAtMost(IVecInt literals, IVec<BigInteger> coeffs,
196 BigInteger degree) throws ContradictionException {
197 throw new UnsupportedOperationException();
198 }
199
200 public IConstr addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
201 throws ContradictionException {
202 throw new UnsupportedOperationException();
203 }
204
205 public IConstr addAtLeast(IVecInt literals, IVec<BigInteger> coeffs,
206 BigInteger degree) throws ContradictionException {
207 throw new UnsupportedOperationException();
208 }
209
210 public IConstr addExactly(IVecInt literals, IVecInt coeffs, int weight)
211 throws ContradictionException {
212 throw new UnsupportedOperationException();
213 }
214
215 public IConstr addExactly(IVecInt literals, IVec<BigInteger> coeffs,
216 BigInteger weight) throws ContradictionException {
217 throw new UnsupportedOperationException();
218 }
219 }