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