View Javadoc

1   package org.sat4j.multicore;
2   
3   import java.io.PrintStream;
4   import java.io.PrintWriter;
5   import java.util.Map;
6   
7   import org.sat4j.core.ASolverFactory;
8   import org.sat4j.specs.ContradictionException;
9   import org.sat4j.specs.IConstr;
10  import org.sat4j.specs.ISolver;
11  import org.sat4j.specs.IVec;
12  import org.sat4j.specs.IVecInt;
13  import org.sat4j.specs.TimeoutException;
14  
15  public class ManyCore implements ISolver, OutcomeListener {
16  
17  	/**
18  	 * 
19  	 */
20  	private static final long serialVersionUID = 1L;
21  
22  	private String[] availableSolvers; // = { };
23  
24  	private ISolver[] solvers;
25  	private int numberOfSolvers;
26  	private int winnerId;
27  	private boolean needToWait;
28  	private boolean resultFound;
29  	private int remainingSolvers;
30  
31  	public ManyCore(ASolverFactory<? extends ISolver> factory, String ... solverNames) {
32  		availableSolvers = solverNames;
33  		Runtime runtime = Runtime.getRuntime();
34  		long memory = runtime.maxMemory();
35  		int numberOfCores = runtime.availableProcessors();
36  		if (memory > 1000000000L) {
37  			numberOfSolvers = numberOfCores;
38  		} else {
39  			numberOfSolvers = 1;
40  		}
41  		if (solverNames.length<numberOfSolvers) {
42  			throw new IllegalArgumentException("I need more solver names to run ManyCore on such computer!");
43  		}
44  		solvers = new ISolver[numberOfSolvers];
45  		for (int i = 0; i < numberOfSolvers; i++) {
46  			solvers[i] = factory.createSolverByName(
47  					availableSolvers[i]);
48  		}
49  	}
50  
51  	public void addAllClauses(IVec<IVecInt> clauses)
52  			throws ContradictionException {
53  		for (int i = 0; i < numberOfSolvers; i++) {
54  			solvers[i].addAllClauses(clauses);
55  		}
56  	}
57  
58  	public IConstr addAtLeast(IVecInt literals, int degree)
59  			throws ContradictionException {
60  		for (int i = 0; i < numberOfSolvers; i++) {
61  			solvers[i].addAtLeast(literals, degree);
62  		}
63  		return null;
64  	}
65  
66  	public IConstr addAtMost(IVecInt literals, int degree)
67  			throws ContradictionException {
68  		for (int i = 0; i < numberOfSolvers; i++) {
69  			solvers[i].addAtMost(literals, degree);
70  		}
71  		return null;
72  	}
73  
74  	public IConstr addClause(IVecInt literals) throws ContradictionException {
75  		for (int i = 0; i < numberOfSolvers; i++) {
76  			solvers[i].addClause(literals);
77  		}
78  		return null;
79  	}
80  
81  	public void clearLearntClauses() {
82  		for (int i = 0; i < numberOfSolvers; i++) {
83  			solvers[i].clearLearntClauses();
84  		}
85  	}
86  
87  	public void expireTimeout() {
88  		for (int i = 0; i < numberOfSolvers; i++) {
89  			solvers[i].expireTimeout();
90  		}
91  	}
92  
93  	public Map<String, Number> getStat() {
94  		return solvers[winnerId].getStat();
95  	}
96  
97  	public int getTimeout() {
98  		return solvers[0].getTimeout();
99  	}
100 
101 	public long getTimeoutMs() {
102 		return solvers[0].getTimeoutMs();
103 	}
104 	
105 	public int newVar() {
106 		throw new UnsupportedOperationException();
107 	}
108 
109 	public int newVar(int howmany) {
110 		int result = 0;
111 		for (int i = 0; i < numberOfSolvers; i++) {
112 			result = solvers[i].newVar(howmany);
113 		}
114 		return result;
115 	}
116 
117 	@Deprecated
118 	public void printStat(PrintStream out, String prefix) {
119 		solvers[winnerId].printStat(out, prefix);
120 	}
121 
122 	public void printStat(PrintWriter out, String prefix) {
123 		solvers[winnerId].printStat(out, prefix);
124 	}
125 
126 	public boolean removeConstr(IConstr c) {
127 		throw new UnsupportedOperationException();
128 	}
129 
130 	public void reset() {
131 		for (int i = 0; i < numberOfSolvers; i++) {
132 			solvers[i].reset();
133 		}
134 	}
135 
136 	public void setExpectedNumberOfClauses(int nb) {
137 		for (int i = 0; i < numberOfSolvers; i++) {
138 			solvers[i].setExpectedNumberOfClauses(nb);
139 		}
140 	}
141 
142 	public void setTimeout(int t) {
143 		for (int i = 0; i < numberOfSolvers; i++) {
144 			solvers[i].setTimeout(t);
145 		}
146 	}
147 
148 	public void setTimeoutMs(long t) {
149 		for (int i = 0; i < numberOfSolvers; i++) {
150 			solvers[i].setTimeoutMs(t);
151 		}
152 	}
153 
154 	public void setTimeoutOnConflicts(int count) {
155 		for (int i = 0; i < numberOfSolvers; i++) {
156 			solvers[i].setTimeoutOnConflicts(count);
157 		}
158 	}
159 
160 	public String toString(String prefix) {
161 		StringBuffer res = new StringBuffer();
162 		res.append("ManyCore solver with ");
163 		res.append(numberOfSolvers);
164         res.append(" solvers running in parallel");
165         res.append("\n");
166         for (int i=0;i<numberOfSolvers;i++) {
167         	res.append(solvers[i].toString(prefix));
168         	res.append("\n");
169         }
170 		return res.toString();
171 	}
172 
173 	public int[] findModel() throws TimeoutException {
174 		throw new UnsupportedOperationException();
175 	}
176 
177 	public int[] findModel(IVecInt assumps) throws TimeoutException {
178 		throw new UnsupportedOperationException();
179 	}
180 
181 	public boolean isSatisfiable() throws TimeoutException {
182 		remainingSolvers = numberOfSolvers;
183 		needToWait = true;
184 		for (int i = 0; i < numberOfSolvers; i++) {
185 			new Thread(new RunnableSolver(i, solvers[i], this)).start();
186 		}
187 		try {
188 			do {
189 				Thread.sleep(1000);
190 			} while (needToWait && remainingSolvers > 0);
191 		} catch (InterruptedException e) {
192 			// TODO: handle exception
193 		}
194 		if (remainingSolvers == 0) {
195 			throw new TimeoutException();
196 		}
197 		return resultFound;
198 	}
199 
200 	public boolean isSatisfiable(IVecInt assumps, boolean globalTimeout)
201 			throws TimeoutException {
202 		throw new UnsupportedOperationException();
203 	}
204 
205 	public boolean isSatisfiable(boolean globalTimeout) throws TimeoutException {
206 		throw new UnsupportedOperationException();
207 	}
208 
209 	public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
210 		throw new UnsupportedOperationException();
211 	}
212 
213 	public int[] model() {
214 		return solvers[winnerId].model();
215 	}
216 
217 	public boolean model(int var) {
218 		return solvers[winnerId].model(var);
219 	}
220 
221 	public int nConstraints() {
222 		return solvers[0].nConstraints();
223 	}
224 
225 	public int nVars() {
226 		return solvers[0].nVars();
227 	}
228 
229 	public void printInfos(PrintWriter out, String prefix) {
230 		for (int i = 0; i < numberOfSolvers; i++) {
231 			solvers[i].printInfos(out, prefix);
232 		}
233 	}
234 
235 	public synchronized void onFinishWithAnswer(boolean finished,
236 			boolean result, int index) {
237 		if (finished) {
238 			winnerId = index;
239 			resultFound = result;
240 			for (int i = 0; i < numberOfSolvers; i++) {
241 				if (i != winnerId)
242 					solvers[i].expireTimeout();
243 			}
244 			System.out.println("c And the winner is "+availableSolvers[winnerId]);
245 			needToWait = false;
246 		} else {
247 			remainingSolvers--;
248 		}
249 	}
250 
251 	public boolean isDBSimplificationAllowed() {
252 		return solvers[0].isDBSimplificationAllowed();
253 	}
254 
255 	public void setDBSimplificationAllowed(boolean status) {
256 		for (int i = 0; i < numberOfSolvers; i++) {
257 			solvers[i].setDBSimplificationAllowed(status);
258 		}		
259 	}
260 
261 }
262 
263 interface OutcomeListener {
264 	void onFinishWithAnswer(boolean finished, boolean result, int index);
265 }
266 
267 class RunnableSolver implements Runnable {
268 
269 	private final int index;
270 	private final ISolver solver;
271 	private final OutcomeListener ol;
272 
273 	public RunnableSolver(int i, ISolver solver, OutcomeListener ol) {
274 		index = i;
275 		this.solver = solver;
276 		this.ol = ol;
277 	}
278 
279 	public void run() {
280 		try {
281 			boolean result = solver.isSatisfiable();
282 			ol.onFinishWithAnswer(true, result, index);
283 		} catch (TimeoutException e) {
284 			ol.onFinishWithAnswer(false, false, index);
285 		}
286 	}
287 
288 }