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