View Javadoc

1   /*******************************************************************************
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
3    *
4    * All rights reserved. This program and the accompanying materials
5    * are made available under the terms of the Eclipse Public License v1.0
6    * which accompanies this distribution, and is available at
7    * http://www.eclipse.org/legal/epl-v10.html
8    *
9    * Alternatively, the contents of this file may be used under the terms of
10   * either the GNU Lesser General Public License Version 2.1 or later (the
11   * "LGPL"), in which case the provisions of the LGPL are applicable instead
12   * of those above. If you wish to allow use of your version of this file only
13   * under the terms of the LGPL, and not to allow others to use your version of
14   * this file under the terms of the EPL, indicate your decision by deleting
15   * the provisions above and replace them with the notice and other provisions
16   * required by the LGPL. If you do not delete the provisions above, a recipient
17   * may use your version of this file under the terms of the EPL or the LGPL.
18   *******************************************************************************/
19  package org.sat4j;
20  
21  import java.io.FileNotFoundException;
22  import java.io.IOException;
23  import java.lang.reflect.Method;
24  import java.util.Properties;
25  import java.util.StringTokenizer;
26  
27  import org.apache.commons.beanutils.BeanUtils;
28  import org.apache.commons.cli.CommandLine;
29  import org.apache.commons.cli.HelpFormatter;
30  import org.apache.commons.cli.Option;
31  import org.apache.commons.cli.Options;
32  import org.apache.commons.cli.ParseException;
33  import org.apache.commons.cli.PosixParser;
34  import org.sat4j.core.ASolverFactory;
35  import org.sat4j.core.VecInt;
36  import org.sat4j.minisat.constraints.MixedDataStructureDaniel;
37  import org.sat4j.minisat.core.DataStructureFactory;
38  import org.sat4j.minisat.core.DotSearchListener;
39  import org.sat4j.minisat.core.IOrder;
40  import org.sat4j.minisat.core.LearningStrategy;
41  import org.sat4j.minisat.core.RestartStrategy;
42  import org.sat4j.minisat.core.SearchParams;
43  import org.sat4j.minisat.core.Solver;
44  import org.sat4j.minisat.learning.PercentLengthLearning;
45  import org.sat4j.minisat.orders.VarOrderHeap;
46  import org.sat4j.minisat.restarts.MiniSATRestarts;
47  import org.sat4j.minisat.uip.FirstUIP;
48  import org.sat4j.reader.InstanceReader;
49  import org.sat4j.reader.ParseFormatException;
50  import org.sat4j.reader.Reader;
51  import org.sat4j.specs.ContradictionException;
52  import org.sat4j.specs.IProblem;
53  import org.sat4j.specs.ISolver;
54  import org.sat4j.specs.IVecInt;
55  
56  /**
57   * This class is used to launch the SAT solvers from the command line. It is
58   * compliant with the SAT competition (www.satcompetition.org) I/O format. The
59   * launcher is to be used as follows:
60   * 
61   * <pre>
62   *                [solvername] filename [key=value]*
63   * </pre>
64   * 
65   * If no solver name is given, then the default solver of the solver factory is
66   * used (@see org.sat4j.core.ASolverFactory#defaultSolver()).
67   * 
68   * @author leberre
69   */
70  public class Lanceur extends AbstractLauncher {
71  
72  	/**
73       * 
74       */
75  	private static final long serialVersionUID = 1L;
76  
77  	/**
78  	 * Lance le prouveur sur un fichier Dimacs.
79  	 * 
80  	 * @param args
81  	 *            doit contenir le nom d'un fichier Dimacs, eventuellement
82  	 *            compress?.
83  	 */
84  	public static void main(final String[] args) {
85  		AbstractLauncher lanceur = new Lanceur();
86  		lanceur.run(args);
87  		System.exit(lanceur.getExitCode().value());
88  	}
89  
90  	protected ASolverFactory<ISolver> factory;
91  
92  	private String filename;
93  
94  	private int k = -1;
95  
96  	@SuppressWarnings("nls")
97  	private Options createCLIOptions() {
98  		Options options = new Options();
99  
100 		options.addOption("l", "library", true,
101 				"specifies the name of the library used (minisat by default)");
102 		options.addOption("s", "solver", true,
103 				"specifies the name of a prebuilt solver from the library");
104 		options.addOption("S", "Solver", true,
105 				"setup a solver using a solver config string");
106 		options.addOption("t", "timeout", true,
107 				"specifies the timeout (in seconds)");
108 		options.addOption("T", "timeoutms", true,
109 				"specifies the timeout (in milliseconds)");
110 		options.addOption("C", "conflictbased", false,
111 				"conflict based timeout (for deterministic behavior)");
112 		options
113 				.addOption("d", "dot", true,
114 						"create a sat4j.dot file in current directory representing the search");
115 		options
116 				.addOption("f", "filename", true,
117 						"specifies the file to use (in conjunction with -d for instance)");
118 		options.addOption("r", "replay", true, "replay stored results");
119 		options.addOption("b", "backup", true,
120 				"backup results in specified file");
121 		options
122 				.addOption("u", "update", false,
123 						"update results file if needed");
124 		options.addOption("m", "mute", false, "Set launcher in silent mode");
125 		options
126 				.addOption("k", "kleast", true,
127 						"limit the search to models having at least k variables set to false");
128 		Option op = options.getOption("l");
129 		op.setArgName("libname");
130 		op = options.getOption("s");
131 		op.setArgName("solvername");
132 		op = options.getOption("t");
133 		op.setArgName("delay");
134 		op = options.getOption("k");
135 		op.setArgName("k");
136 		options.getOption("d");
137 		return options;
138 	}
139 
140 	/**
141 	 * Configure the solver according to the command line parameters.
142 	 * 
143 	 * @param args
144 	 *            the command line
145 	 * @return a solver properly configured.
146 	 */
147 	@SuppressWarnings( { "nls", "unchecked" })
148 	@Override
149 	protected ISolver configureSolver(String[] args) {
150 		Options options = createCLIOptions();
151 		if (args.length == 0) {
152 			HelpFormatter helpf = new HelpFormatter();
153 			helpf.printHelp("java -jar sat4j.jar", options, true);
154 			return null;
155 		}
156 		try {
157 			CommandLine cmd = new PosixParser().parse(options, args);
158 
159 			String framework = cmd.getOptionValue("l"); //$NON-NLS-1$
160 			if (framework == null) { //$NON-NLS-1$
161 				framework = "minisat";
162 			}
163 
164 			try {
165 				Class<?> clazz = Class
166 						.forName("org.sat4j." + framework + ".SolverFactory"); //$NON-NLS-1$ //$NON-NLS-2$
167 				Class<?>[] params = {};
168 				Method m = clazz.getMethod("instance", params); //$NON-NLS-1$
169 				factory = (ASolverFactory) m.invoke(null, (Object[]) null);
170 			} catch (Exception e) { // DLB Findbugs warning ok
171 				System.err.println(Messages
172 						.getString("Lanceur.wrong.framework")); //$NON-NLS-1$
173 				e.printStackTrace();
174 			}
175 
176 			ISolver asolver;
177 			if (cmd.hasOption("S")) {
178 				asolver = configureFromString(cmd.getOptionValue("S"));
179 			} else {
180 				String solvername = cmd.getOptionValue("s");
181 				if (solvername == null) {
182 					asolver = factory.defaultSolver();
183 				} else {
184 					asolver = factory.createSolverByName(solvername);
185 				}
186 			}
187 			String timeout = cmd.getOptionValue("t");
188 			if (timeout == null) {
189 				timeout = cmd.getOptionValue("T");
190 				if (timeout != null) {
191 					asolver.setTimeoutMs(Long.parseLong(timeout));
192 				}
193 			} else {
194 				if (cmd.hasOption("C")) {
195 					asolver.setTimeoutOnConflicts(Integer.parseInt(timeout));
196 				} else {
197 					asolver.setTimeout(Integer.parseInt(timeout));
198 				}
199 			}
200 			filename = cmd.getOptionValue("f");
201 
202 			if (cmd.hasOption("d")) {
203 				String dotfilename = null;
204 				if (filename != null) {
205 					dotfilename = cmd.getOptionValue("d");
206 				}
207 				if (dotfilename == null) {
208 					dotfilename = "sat4j.dot";
209 				}
210 				((Solver<?, DataStructureFactory<?>>) asolver)
211 						.setSearchListener(new DotSearchListener(dotfilename));
212 			}
213 
214 			if (cmd.hasOption("m")) {
215 				setSilent(true);
216 			}
217 
218 			if (cmd.hasOption("k")) {
219 				Integer myk = Integer.valueOf(cmd.getOptionValue("k"));
220 				if (myk != null) {
221 					k = myk.intValue();
222 				}
223 			}
224 			int others = 0;
225 			String[] rargs = cmd.getArgs();
226 			if (filename == null) {
227 				filename = rargs[others++];
228 			}
229 
230 			// use remaining data to configure the solver
231 			while (others < rargs.length) {
232 				String[] param = rargs[others].split("="); //$NON-NLS-1$
233 				assert param.length == 2;
234 				log("setting " + param[0] + " to " + param[1]); //$NON-NLS-1$ //$NON-NLS-2$
235 				try {
236 					BeanUtils.setProperty(asolver, param[0], param[1]);
237 				} catch (Exception e) {
238 					log("Cannot set parameter : " //$NON-NLS-1$
239 							+ args[others]);
240 				}
241 				others++;
242 			}
243 
244 			log(asolver.toString(COMMENT_PREFIX)); //$NON-NLS-1$
245 			return asolver;
246 		} catch (ParseException e1) {
247 			HelpFormatter helpf = new HelpFormatter();
248 			helpf.printHelp("java -jar sat4j.jar", options, true);
249 			usage();
250 		}
251 		return null;
252 	}
253 
254 	@Override
255 	protected Reader createReader(ISolver theSolver, String problemname) {
256 		return new InstanceReader(theSolver);
257 	}
258 
259 	@Override
260 	public void displayLicense() {
261 		super.displayLicense();
262 		log("This software uses some libraries from the Jakarta Commons project. See jakarta.apache.org for details."); //$NON-NLS-1$
263 	}
264 
265 	@Override
266 	public void usage() {
267 		showAvailableSolvers(factory);
268 	}
269 
270 	@Override
271 	protected String getInstanceName(String[] args) {
272 		return filename;
273 	}
274 
275 	@SuppressWarnings("unchecked")
276 	private final ISolver configureFromString(String solverconfig) {
277 		// AFAIK, there is no easy way to solve parameterized problems
278 		// when building the solver at runtime.
279 		StringTokenizer stk = new StringTokenizer(solverconfig, ",");
280 		Properties pf = new Properties();
281 		String token;
282 		String[] couple;
283 		while (stk.hasMoreElements()) {
284 			token = stk.nextToken();
285 			couple = token.split("=");
286 			pf.setProperty(couple[0], couple[1]);
287 		}
288 		DataStructureFactory dsf = setupObject("DSF", pf,
289 				new MixedDataStructureDaniel());
290 		LearningStrategy learning = setupObject("LEARNING", pf,
291 				new PercentLengthLearning());
292 		IOrder order = setupObject("ORDER", pf, new VarOrderHeap());
293 		RestartStrategy restarter = setupObject("RESTARTS", pf,
294 				new MiniSATRestarts());
295 		Solver theSolver = new Solver(new FirstUIP(), learning, dsf, order,
296 				restarter);
297 		learning.setSolver(theSolver);
298 		theSolver.setSimplifier(pf.getProperty("SIMP", "NO_SIMPLIFICATION"));
299 		SearchParams params = setupObject("PARAMS", pf, new SearchParams());
300 		theSolver.setSearchParams(params);
301 		return theSolver;
302 	}
303 
304 	@SuppressWarnings("unchecked")
305 	private final <T> T setupObject(String component, Properties pf,
306 			T defaultcomp) {
307 		try {
308 			String configline = pf.getProperty(component);
309 			if (configline == null) {
310 				log("using default component " + defaultcomp + " for "
311 						+ component);
312 				return defaultcomp;
313 			}
314 			log("configuring " + component);
315 			String[] config = configline.split("/");
316 			T comp = (T) Class.forName(config[0]).newInstance();
317 			for (int i = 1; i < config.length; i++) {
318 				String[] param = config[i].split(":"); //$NON-NLS-1$
319 				assert param.length == 2;
320 				try {
321 					// Check first that the property really exists
322 					BeanUtils.getProperty(comp, param[0]);
323 					BeanUtils.setProperty(comp, param[0], param[1]);
324 				} catch (Exception e) {
325 					log("Problem with component " + config[0] + " " + e);
326 				}
327 			}
328 			return comp;
329 		} catch (InstantiationException e) {
330 			log("Problem with component " + component + " " + e);
331 		} catch (IllegalAccessException e) {
332 			log("Problem with component " + component + " " + e);
333 		} catch (ClassNotFoundException e) {
334 			log("Problem with component " + component + " " + e);
335 		}
336 		log("using default component " + defaultcomp + " for " + component);
337 		return defaultcomp;
338 	}
339 
340 	@Override
341 	protected IProblem readProblem(String problemname)
342 			throws FileNotFoundException, ParseFormatException, IOException,
343 			ContradictionException {
344 		ISolver solver = (ISolver) super.readProblem(problemname);
345 		if (k > 0) {			
346 			IVecInt literals = new VecInt();
347 			for (int i = 1; i <= solver.nVars(); i++) {
348 				literals.push(-i);
349 			}
350 			solver.addAtLeast(literals, k);
351 			log("Limiting solutions to those having at least "+k+" variables assigned to false");
352 		}
353 		return solver;
354 	}
355 }