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   * Based on the original MiniSat specification from:
20   * 
21   * An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
22   * Sixth International Conference on Theory and Applications of Satisfiability
23   * Testing, LNCS 2919, pp 502-518, 2003.
24   *
25   * See www.minisat.se for the original solver in C++.
26   * 
27   * The reason simplification methods are coming from MiniSAT 1.14 released under 
28   * the MIT license:
29   * MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson
30   *
31   * Permission is hereby granted, free of charge, to any person obtaining a
32   * copy of this software and associated documentation files (the
33   * "Software"), to deal in the Software without restriction, including
34   * without limitation the rights to use, copy, modify, merge, publish,
35   * distribute, sublicense, and/or sell copies of the Software, and to
36   * permit persons to whom the Software is furnished to do so, subject to
37   * the following conditions:
38   *
39   * The above copyright notice and this permission notice shall be included
40   * in all copies or substantial portions of the Software.
41   * 
42   * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS
43   * OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
44   * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
45   * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
46   * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
47   * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
48   * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. 
49   *******************************************************************************/
50  package org.sat4j.minisat.core;
51  
52  import static org.sat4j.core.LiteralsUtils.var;
53  import static org.sat4j.core.LiteralsUtils.toDimacs;
54  
55  import java.io.PrintStream;
56  import java.io.PrintWriter;
57  import java.io.Serializable;
58  import java.lang.reflect.Field;
59  import java.util.Comparator;
60  import java.util.HashMap;
61  import java.util.Iterator;
62  import java.util.Map;
63  import java.util.Timer;
64  import java.util.TimerTask;
65  
66  import org.sat4j.core.Vec;
67  import org.sat4j.core.VecInt;
68  import org.sat4j.specs.ContradictionException;
69  import org.sat4j.specs.IConstr;
70  import org.sat4j.specs.ISolver;
71  import org.sat4j.specs.IVec;
72  import org.sat4j.specs.IVecInt;
73  import org.sat4j.specs.IteratorInt;
74  import org.sat4j.specs.TimeoutException;
75  
76  /**
77   * The backbone of the library providing the modular implementation of a MiniSAT
78   * (Chaff) like solver.
79   * 
80   * @author leberre
81   */
82  public class Solver<L extends ILits, D extends DataStructureFactory<L>>
83  		implements ISolver, UnitPropagationListener, ActivityListener, Learner {
84  
85  	private static final long serialVersionUID = 1L;
86  
87  	private static final double CLAUSE_RESCALE_FACTOR = 1e-20;
88  
89  	private static final double CLAUSE_RESCALE_BOUND = 1 / CLAUSE_RESCALE_FACTOR;
90  
91  	/**
92  	 * List des contraintes du probl?me.
93  	 */
94  	private final IVec<Constr> constrs = new Vec<Constr>(); // Constr
95  
96  	/**
97  	 * Liste des clauses apprises.
98  	 */
99  	private final IVec<Constr> learnts = new Vec<Constr>(); // Clause
100 
101 	/**
102 	 * incr?ment pour l'activit? des clauses.
103 	 */
104 	private double claInc = 1.0;
105 
106 	/**
107 	 * decay factor pour l'activit? des clauses.
108 	 */
109 	private double claDecay = 1.0;
110 
111 	/**
112 	 * Queue de propagation
113 	 */
114 	// private final IntQueue propQ = new IntQueue(); // Lit
115 	// head of the queue in trail ... (taken from MiniSAT 1.14)
116 	private int qhead = 0;
117 
118 	// queue
119 
120 	/**
121 	 * affectation en ordre chronologique
122 	 */
123 	protected final IVecInt trail = new VecInt(); // lit
124 
125 	// vector
126 
127 	/**
128 	 * indice des s?parateurs des diff?rents niveau de d?cision dans trail
129 	 */
130 	protected final IVecInt trailLim = new VecInt(); // int
131 
132 	// vector
133 
134 	/**
135 	 * S?pare les hypoth?ses incr?mentale et recherche
136 	 */
137 	protected int rootLevel;
138 
139 	private int[] model = null;
140 
141 	protected L voc;
142 
143 	private IOrder<L> order;
144 
145 	private final ActivityComparator comparator = new ActivityComparator();
146 
147 	private final SolverStats stats = new SolverStats();
148 
149 	private final LearningStrategy<L, D> learner;
150 
151 	protected final AssertingClauseGenerator analyzer;
152 
153 	private volatile boolean undertimeout;
154 
155 	private long timeout = Integer.MAX_VALUE;
156 
157 	private boolean timeBasedTimeout = true;
158 
159 	protected D dsfactory;
160 
161 	private SearchParams params;
162 
163 	private final IVecInt __dimacs_out = new VecInt();
164 
165 	private SearchListener slistener = new NullSearchListener();
166 
167 	private RestartStrategy restarter;
168 
169 	private final Map<String, Counter> constrTypes = new HashMap<String, Counter>();
170 
171 	private boolean isDBSimplificationAllowed = false;
172 
173 	private int learnedLiterals = 0;
174 
175 	protected IVecInt dimacs2internal(IVecInt in) {
176 		// if (voc.nVars() == 0) {
177 		// throw new RuntimeException(
178 		// "Please set the number of variables (solver.newVar() or solver.newVar(maxvar)) before adding constraints!"
179 		// );
180 		// }
181 		__dimacs_out.clear();
182 		__dimacs_out.ensure(in.size());
183 		for (int i = 0; i < in.size(); i++) {
184 			assert (in.get(i) != 0); // && (Math.abs(in.get(i)) <= voc.nVars());
185 			__dimacs_out.unsafePush(voc.getFromPool(in.get(i)));
186 		}
187 		return __dimacs_out;
188 	}
189 
190 	/**
191 	 * creates a Solver without LearningListener. A learningListener must be
192 	 * added to the solver, else it won't backtrack!!! A data structure factory
193 	 * must be provided, else it won't work either.
194 	 * 
195 	 * @param acg
196 	 *            an asserting clause generator
197 	 */
198 
199 	public Solver(AssertingClauseGenerator acg, LearningStrategy<L, D> learner,
200 			D dsf, IOrder<L> order, RestartStrategy restarter) {
201 		this(acg, learner, dsf, new SearchParams(), order, restarter);
202 	}
203 
204 	public Solver(AssertingClauseGenerator acg, LearningStrategy<L, D> learner,
205 			D dsf, SearchParams params, IOrder<L> order,
206 			RestartStrategy restarter) {
207 		analyzer = acg;
208 		this.learner = learner;
209 		this.order = order;
210 		this.params = params;
211 		setDataStructureFactory(dsf);
212 		this.restarter = restarter;
213 	}
214 
215 	/**
216 	 * Change the internal representation of the contraints. Note that the
217 	 * heuristics must be changed prior to calling that method.
218 	 * 
219 	 * @param dsf
220 	 *            the internal factory
221 	 */
222 	public final void setDataStructureFactory(D dsf) {
223 		dsfactory = dsf;
224 		dsfactory.setUnitPropagationListener(this);
225 		dsfactory.setLearner(this);
226 		voc = dsf.getVocabulary();
227 		order.setLits(voc);
228 	}
229 
230 	public void setSearchListener(SearchListener sl) {
231 		slistener = sl;
232 	}
233 
234 	public void setTimeout(int t) {
235 		timeout = t * 1000L;
236 		timeBasedTimeout = true;
237 	}
238 
239 	public void setTimeoutMs(long t) {
240 		timeout = t;
241 		timeBasedTimeout = true;
242 	}
243 
244 	public void setTimeoutOnConflicts(int count) {
245 		timeout = count;
246 		timeBasedTimeout = false;
247 	}
248 
249 	public void setSearchParams(SearchParams sp) {
250 		params = sp;
251 	}
252 
253 	public void setRestartStrategy(RestartStrategy restarter) {
254 		this.restarter = restarter;
255 	}
256 
257 	public void expireTimeout() {
258 		undertimeout = false;
259 	}
260 
261 	protected int nAssigns() {
262 		return trail.size();
263 	}
264 
265 	public int nConstraints() {
266 		return constrs.size() + trail.size() - learnedLiterals;
267 	}
268 
269 	public void learn(Constr c) {
270 		learnts.push(c);
271 		c.setLearnt();
272 		c.register();
273 		stats.learnedclauses++;
274 		switch (c.size()) {
275 		case 2:
276 			stats.learnedbinaryclauses++;
277 			break;
278 		case 3:
279 			stats.learnedternaryclauses++;
280 			break;
281 		default:
282 			// do nothing
283 		}
284 	}
285 
286 	public int decisionLevel() {
287 		return trailLim.size();
288 	}
289 
290 	@Deprecated
291 	public int newVar() {
292 		int index = voc.nVars() + 1;
293 		voc.ensurePool(index);
294 		return index;
295 	}
296 
297 	public int newVar(int howmany) {
298 		voc.ensurePool(howmany);
299 		return voc.nVars();
300 	}
301 
302 	public IConstr addClause(IVecInt literals) throws ContradictionException {
303 		IVecInt vlits = dimacs2internal(literals);
304 		return addConstr(dsfactory.createClause(vlits));
305 	}
306 
307 	public boolean removeConstr(IConstr co) {
308 		if (co == null) {
309 			throw new IllegalArgumentException(
310 					"Reference to the constraint to remove needed!"); //$NON-NLS-1$
311 		}
312 		Constr c = (Constr) co;
313 		c.remove();
314 		constrs.remove(c);
315 		clearLearntClauses();
316 		cancelLearntLiterals();
317 		return true;
318 	}
319 
320 	public void addAllClauses(IVec<IVecInt> clauses)
321 			throws ContradictionException {
322 		for (Iterator<IVecInt> iterator = clauses.iterator(); iterator
323 				.hasNext();) {
324 			addClause(iterator.next());
325 		}
326 	}
327 
328 	public IConstr addAtMost(IVecInt literals, int degree)
329 			throws ContradictionException {
330 		int n = literals.size();
331 		IVecInt opliterals = new VecInt(n);
332 		for (IteratorInt iterator = literals.iterator(); iterator.hasNext();) {
333 			opliterals.push(-iterator.next());
334 		}
335 		return addAtLeast(opliterals, n - degree);
336 	}
337 
338 	public IConstr addAtLeast(IVecInt literals, int degree)
339 			throws ContradictionException {
340 		IVecInt vlits = dimacs2internal(literals);
341 		return addConstr(dsfactory.createCardinalityConstraint(vlits, degree));
342 	}
343 
344 	@SuppressWarnings("unchecked")
345 	public boolean simplifyDB() {
346 		// aucune raison de recommencer un propagate?
347 		// if (propagate() != null) {
348 		// // Un conflit est d?couvert, la base est inconsistante
349 		// return false;
350 		// }
351 
352 		// Simplifie la base de clauses apres la premiere propagation des
353 		// clauses unitaires
354 		IVec<Constr>[] cs = new IVec[] { constrs, learnts };
355 		for (int type = 0; type < 2; type++) {
356 			int j = 0;
357 			for (int i = 0; i < cs[type].size(); i++) {
358 				if (cs[type].get(i).simplify()) {
359 					// enleve les contraintes satisfaites de la base
360 					cs[type].get(i).remove();
361 				} else {
362 					cs[type].moveTo(j++, i);
363 				}
364 			}
365 			cs[type].shrinkTo(j);
366 		}
367 		return true;
368 	}
369 
370 	/**
371 	 * Si un mod?le est trouv?, ce vecteur contient le mod?le.
372 	 * 
373 	 * @return un mod?le de la formule.
374 	 */
375 	public int[] model() {
376 		if (model == null) {
377 			throw new UnsupportedOperationException(
378 					"Call the solve method first!!!"); //$NON-NLS-1$
379 		}
380 		int[] nmodel = new int[model.length];
381 		System.arraycopy(model, 0, nmodel, 0, model.length);
382 		return nmodel;
383 	}
384 
385 	/**
386 	 * Satisfait un litt?ral
387 	 * 
388 	 * @param p
389 	 *            le litt?ral
390 	 * @return true si tout se passe bien, false si un conflit appara?t.
391 	 */
392 	public boolean enqueue(int p) {
393 		return enqueue(p, null);
394 	}
395 
396 	/**
397 	 * Put the literal on the queue of assignments to be done.
398 	 * 
399 	 * @param p
400 	 *            the literal.
401 	 * @param from
402 	 *            the reason to propagate that literal, else null
403 	 * @return true if the asignment can be made, false if a conflict is
404 	 *         detected.
405 	 */
406 	public boolean enqueue(int p, Constr from) {
407 		assert p > 1;
408 		if (voc.isSatisfied(p)) {
409 			// literal is already satisfied. Skipping.
410 			return true;
411 		}
412 		if (voc.isFalsified(p)) {
413 			// conflicting enqueued assignment
414 			return false;
415 		}
416 		// new fact, store it
417 		voc.satisfies(p);
418 		voc.setLevel(p, decisionLevel());
419 		voc.setReason(p, from);
420 		trail.push(p);
421 		return true;
422 	}
423 
424 	private boolean[] mseen = new boolean[0];
425 
426 	private final IVecInt preason = new VecInt();
427 
428 	private final IVecInt outLearnt = new VecInt();
429 
430 	public void analyze(Constr confl, Pair results) {
431 		assert confl != null;
432 		outLearnt.clear();
433 
434 		final boolean[] seen = mseen;
435 
436 		assert outLearnt.size() == 0;
437 		for (int i = 0; i < seen.length; i++) {
438 			seen[i] = false;
439 		}
440 
441 		analyzer.initAnalyze();
442 		int p = ILits.UNDEFINED;
443 
444 		outLearnt.push(ILits.UNDEFINED);
445 		// reserve de la place pour le litteral falsifie
446 		int outBtlevel = 0;
447 
448 		do {
449 			preason.clear();
450 			assert confl != null;
451 			confl.calcReason(p, preason);
452 			if (confl.learnt())
453 				claBumpActivity(confl);
454 			// Trace reason for p
455 			for (int j = 0; j < preason.size(); j++) {
456 				int q = preason.get(j);
457 				order.updateVar(q);
458 				if (!seen[q >> 1]) {
459 					// order.updateVar(q); // MINISAT
460 					seen[q >> 1] = true;
461 					if (voc.getLevel(q) == decisionLevel()) {
462 						analyzer.onCurrentDecisionLevelLiteral(q);
463 					} else if (voc.getLevel(q) > 0) {
464 						// ajoute les variables depuis le niveau de d?cision 0
465 						outLearnt.push(q ^ 1);
466 						outBtlevel = Math.max(outBtlevel, voc.getLevel(q));
467 					}
468 				}
469 			}
470 
471 			// select next reason to look at
472 			do {
473 				p = trail.last();
474 				confl = voc.getReason(p);
475 				undoOne();
476 			} while (!seen[p >> 1]);
477 			// seen[p.var] indique que p se trouve dans outLearnt ou dans
478 			// le dernier niveau de d?cision
479 		} while (analyzer.clauseNonAssertive(confl));
480 
481 		outLearnt.set(0, p ^ 1);
482 		simplifier.simplify(outLearnt);
483 
484 		Constr c = dsfactory.createUnregisteredClause(outLearnt);
485 		slistener.learn(c);
486 
487 		results.reason = c;
488 
489 		assert outBtlevel > -1;
490 		results.backtrackLevel = outBtlevel;
491 	}
492 
493 	interface ISimplifier extends Serializable {
494 		void simplify(IVecInt outLearnt);
495 	}
496 
497 	public static final ISimplifier NO_SIMPLIFICATION = new ISimplifier() {
498 		/**
499          * 
500          */
501 		private static final long serialVersionUID = 1L;
502 
503 		public void simplify(IVecInt outLearnt) {
504 		}
505 
506 		@Override
507 		public String toString() {
508 			return "No reason simplification"; //$NON-NLS-1$
509 		}
510 	};
511 
512 	public final ISimplifier SIMPLE_SIMPLIFICATION = new ISimplifier() {
513 		/**
514          * 
515          */
516 		private static final long serialVersionUID = 1L;
517 
518 		public void simplify(IVecInt conflictToReduce) {
519 			simpleSimplification(conflictToReduce);
520 		}
521 
522 		@Override
523 		public String toString() {
524 			return "Simple reason simplification"; //$NON-NLS-1$
525 		}
526 	};
527 
528 	public final ISimplifier EXPENSIVE_SIMPLIFICATION = new ISimplifier() {
529 
530 		/**
531          * 
532          */
533 		private static final long serialVersionUID = 1L;
534 
535 		public void simplify(IVecInt conflictToReduce) {
536 			expensiveSimplification(conflictToReduce);
537 		}
538 
539 		@Override
540 		public String toString() {
541 			return "Expensive reason simplification"; //$NON-NLS-1$
542 		}
543 	};
544 
545 	private ISimplifier simplifier = NO_SIMPLIFICATION;
546 
547 	/**
548 	 * Setup the reason simplification strategy. By default, there is no reason
549 	 * simplification. NOTE THAT REASON SIMPLIFICATION DOES NOT WORK WITH
550 	 * SPECIFIC DATA STRUCTURE FOR HANDLING BOTH BINARY AND TERNARY CLAUSES.
551 	 * 
552 	 * @param simp
553 	 *            the name of the simplifier (one of NO_SIMPLIFICATION,
554 	 *            SIMPLE_SIMPLIFICATION, EXPENSIVE_SIMPLIFICATION).
555 	 */
556 	public void setSimplifier(String simp) {
557 		Field f;
558 		try {
559 			f = Solver.class.getDeclaredField(simp);
560 			simplifier = (ISimplifier) f.get(this);
561 		} catch (Exception e) {
562 			e.printStackTrace();
563 			simplifier = NO_SIMPLIFICATION;
564 		}
565 	}
566 
567 	/**
568 	 * Setup the reason simplification strategy. By default, there is no reason
569 	 * simplification. NOTE THAT REASON SIMPLIFICATION IS ONLY ALLOWED FOR WL
570 	 * CLAUSAL data structures. USING REASON SIMPLIFICATION ON CB CLAUSES,
571 	 * CARDINALITY CONSTRAINTS OR PB CONSTRAINTS MIGHT RESULT IN INCORRECT
572 	 * RESULTS.
573 	 * 
574 	 * @param simp
575 	 */
576 	public void setSimplifier(ISimplifier simp) {
577 		simplifier = simp;
578 	}
579 
580 	// MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson
581 	//
582 	// Permission is hereby granted, free of charge, to any person obtaining a
583 	// copy of this software and associated documentation files (the
584 	// "Software"), to deal in the Software without restriction, including
585 	// without limitation the rights to use, copy, modify, merge, publish,
586 	// distribute, sublicense, and/or sell copies of the Software, and to
587 	// permit persons to whom the Software is furnished to do so, subject to
588 	// the following conditions:
589 	//
590 	// The above copyright notice and this permission notice shall be included
591 	// in all copies or substantial portions of the Software.
592 	//
593 	// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS
594 	// OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
595 	// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
596 	// NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
597 	// LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
598 	// OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
599 	// WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
600 
601 	// Taken from MiniSAT 1.14: Simplify conflict clause (a little):
602 	private void simpleSimplification(IVecInt conflictToReduce) {
603 		int i, j;
604 		final boolean[] seen = mseen;
605 		for (i = j = 1; i < conflictToReduce.size(); i++) {
606 			IConstr r = voc.getReason(conflictToReduce.get(i));
607 			if (r == null) {
608 				conflictToReduce.moveTo(j++, i);
609 			} else {
610 				for (int k = 0; k < r.size(); k++)
611 					if (voc.isFalsified(r.get(k)) && !seen[r.get(k) >> 1]
612 							&& (voc.getLevel(r.get(k)) != 0)) {
613 						conflictToReduce.moveTo(j++, i);
614 						break;
615 					}
616 			}
617 		}
618 		conflictToReduce.shrink(i - j);
619 		stats.reducedliterals += (i - j);
620 	}
621 
622 	private final IVecInt analyzetoclear = new VecInt();
623 
624 	private final IVecInt analyzestack = new VecInt();
625 
626 	// Taken from MiniSAT 1.14
627 	private void expensiveSimplification(IVecInt conflictToReduce) {
628 		// Simplify conflict clause (a lot):
629 		//
630 		int i, j;
631 		// (maintain an abstraction of levels involved in conflict)
632 		analyzetoclear.clear();
633 		conflictToReduce.copyTo(analyzetoclear);
634 		for (i = 1, j = 1; i < conflictToReduce.size(); i++)
635 			if (voc.getReason(conflictToReduce.get(i)) == null
636 					|| !analyzeRemovable(conflictToReduce.get(i)))
637 				conflictToReduce.moveTo(j++, i);
638 		conflictToReduce.shrink(i - j);
639 		stats.reducedliterals += (i - j);
640 	}
641 
642 	// Check if 'p' can be removed.' min_level' is used to abort early if
643 	// visiting literals at a level that cannot be removed.
644 	//
645 	private boolean analyzeRemovable(int p) {
646 		assert voc.getReason(p) != null;
647 		analyzestack.clear();
648 		analyzestack.push(p);
649 		final boolean[] seen = mseen;
650 		int top = analyzetoclear.size();
651 		while (analyzestack.size() > 0) {
652 			int q = analyzestack.last();
653 			assert voc.getReason(q) != null;
654 			Constr c = voc.getReason(q);
655 			analyzestack.pop();
656 			for (int i = 0; i < c.size(); i++) {
657 				int l = c.get(i);
658 				if (voc.isFalsified(l) && !seen[var(l)] && voc.getLevel(l) != 0) {
659 					if (voc.getReason(l) == null) {
660 						for (int j = top; j < analyzetoclear.size(); j++)
661 							seen[analyzetoclear.get(j) >> 1] = false;
662 						analyzetoclear.shrink(analyzetoclear.size() - top);
663 						return false;
664 					}
665 					seen[l >> 1] = true;
666 					analyzestack.push(l);
667 					analyzetoclear.push(l);
668 				}
669 			}
670 		}
671 
672 		return true;
673 	}
674 
675 	// END Minisat 1.14 cut and paste
676 
677 	/**
678      * 
679      */
680 	protected void undoOne() {
681 		// recupere le dernier litteral affecte
682 		int p = trail.last();
683 		assert p > 1;
684 		assert voc.getLevel(p) >= 0;
685 		int x = p >> 1;
686 		// desaffecte la variable
687 		voc.unassign(p);
688 		voc.setReason(p, null);
689 		voc.setLevel(p, -1);
690 		// met a jour l'heuristique
691 		order.undo(x);
692 		// depile le litteral des affectations
693 		trail.pop();
694 		// met a jour les contraintes apres desaffectation du litteral :
695 		// normalement, il n'y a rien a faire ici pour les prouveurs de type
696 		// Chaff??
697 		IVec<Undoable> undos = voc.undos(p);
698 		assert undos != null;
699 		while (undos.size() > 0) {
700 			undos.last().undo(p);
701 			undos.pop();
702 		}
703 	}
704 
705 	/**
706 	 * Propagate activity to a constraint
707 	 * 
708 	 * @param confl
709 	 *            a constraint
710 	 */
711 	public void claBumpActivity(Constr confl) {
712 		confl.incActivity(claInc);
713 		if (confl.getActivity() > CLAUSE_RESCALE_BOUND)
714 			claRescalActivity();
715 		// for (int i = 0; i < confl.size(); i++) {
716 		// varBumpActivity(confl.get(i));
717 		// }
718 	}
719 
720 	public void varBumpActivity(int p) {
721 		order.updateVar(p);
722 	}
723 
724 	private void claRescalActivity() {
725 		for (int i = 0; i < learnts.size(); i++) {
726 			learnts.get(i).rescaleBy(CLAUSE_RESCALE_FACTOR);
727 		}
728 		claInc *= CLAUSE_RESCALE_FACTOR;
729 	}
730 
731 	/**
732 	 * @return null if not conflict is found, else a conflicting constraint.
733 	 */
734 	public Constr propagate() {
735 		while (qhead < trail.size()) {
736 			stats.propagations++;
737 			int p = trail.get(qhead++);
738 			slistener.propagating(toDimacs(p));
739 			order.assignLiteral(p);
740 			// p is the literal to propagate
741 			// Moved original MiniSAT code to dsfactory to avoid
742 			// watches manipulation in counter Based clauses for instance.
743 			assert p > 1;
744 			IVec<Propagatable> watched = dsfactory.getAttachesFor(p);
745 
746 			final int size = watched.size();
747 			for (int i = 0; i < size; i++) {
748 				stats.inspects++;
749 				if (!watched.get(i).propagate(this, p)) {
750 					// Constraint is conflicting: copy remaining watches to
751 					// watches[p]
752 					// and return constraint
753 					dsfactory.conflictDetectedInAttachesFor(p, i);
754 					qhead = trail.size(); // propQ.clear();
755 					// FIXME enlever le transtypage
756 					return (Constr) watched.get(i);
757 				}
758 			}
759 		}
760 		return null;
761 	}
762 
763 	void record(Constr constr) {
764 		constr.assertConstraint(this);
765 		slistener.adding(toDimacs(constr.get(0)));
766 		if (constr.size() == 1) {
767 			stats.learnedliterals++;
768 			learnedLiterals++;
769 		} else {
770 			learner.learns(constr);
771 		}
772 	}
773 
774 	/**
775 	 * @return false ssi conflit imm?diat.
776 	 */
777 	public boolean assume(int p) {
778 		// Precondition: assume propagation queue is empty
779 		assert trail.size() == qhead;
780 		trailLim.push(trail.size());
781 		return enqueue(p);
782 	}
783 
784 	/**
785 	 * Revert to the state before the last push()
786 	 */
787 	private void cancel() {
788 		// assert trail.size() == qhead || !undertimeout;
789 		int decisionvar = trail.unsafeGet(trailLim.last());
790 		slistener.backtracking(toDimacs(decisionvar));
791 		for (int c = trail.size() - trailLim.last(); c > 0; c--) {
792 			undoOne();
793 		}
794 		trailLim.pop();
795 	}
796 
797 	/**
798 	 * Restore literals
799 	 */
800 	private void cancelLearntLiterals() {
801 		// assert trail.size() == qhead || !undertimeout;
802 		for (int c = learnedLiterals; c > 0; c--) {
803 			undoOne();
804 		}
805 		qhead = trail.size();
806 	}
807 
808 	/**
809 	 * Cancel several levels of assumptions
810 	 * 
811 	 * @param level
812 	 */
813 	protected void cancelUntil(int level) {
814 		while (decisionLevel() > level) {
815 			cancel();
816 		}
817 		qhead = trail.size();
818 	}
819 
820 	private final Pair analysisResult = new Pair();
821 
822 	private boolean[] fullmodel;
823 
824 	Lbool search(long nofConflicts) {
825 		assert rootLevel == decisionLevel();
826 		stats.starts++;
827 		int conflictC = 0;
828 
829 		// varDecay = 1 / params.varDecay;
830 		order.setVarDecay(1 / params.getVarDecay());
831 		claDecay = 1 / params.getClaDecay();
832 
833 		do {
834 			slistener.beginLoop();
835 			// propage les clauses unitaires
836 			Constr confl = propagate();
837 			assert trail.size() == qhead;
838 
839 			if (confl == null) {
840 				// No conflict found
841 				// simpliFYDB() prevents a correct use of
842 				// constraints removal.
843 				if (decisionLevel() == 0 && isDBSimplificationAllowed) {
844 					// // Simplify the set of problem clause
845 					// // iff rootLevel==0
846 					stats.rootSimplifications++;
847 					boolean ret = simplifyDB();
848 					assert ret;
849 				}
850 				// was learnts.size() - nAssigns() > nofLearnts
851 				// if (nofLearnts.obj >= 0 && learnts.size() > nofLearnts.obj) {
852 				assert nAssigns() <= voc.realnVars();
853 				if (nAssigns() == voc.realnVars()) {
854 					slistener.solutionFound();
855 					modelFound();
856 					return Lbool.TRUE;
857 				}
858 				if (conflictC >= nofConflicts) {
859 					// Reached bound on number of conflicts
860 					// Force a restart
861 					cancelUntil(rootLevel);
862 					return Lbool.UNDEFINED;
863 				}
864 				if (needToReduceDB) {
865 					reduceDB();
866 					needToReduceDB = false;
867 					// Runtime.getRuntime().gc();
868 				}
869 				// New variable decision
870 				stats.decisions++;
871 				int p = order.select();
872 				assert p > 1;
873 				slistener.assuming(toDimacs(p));
874 				boolean ret = assume(p);
875 				assert ret;
876 			} else {
877 				// un conflit apparait
878 				stats.conflicts++;
879 				conflictC++;
880 				slistener.conflictFound();
881 				conflictCount.newConflict();
882 				if (decisionLevel() == rootLevel) {
883 					// on est a la racine, la formule est inconsistante
884 					return Lbool.FALSE;
885 				}
886 				// analyze conflict
887 				analyze(confl, analysisResult);
888 				assert analysisResult.backtrackLevel < decisionLevel();
889 				cancelUntil(Math.max(analysisResult.backtrackLevel, rootLevel));
890 				assert (decisionLevel() >= rootLevel)
891 						&& (decisionLevel() >= analysisResult.backtrackLevel);
892 				if (analysisResult.reason == null) {
893 					return Lbool.FALSE;
894 				}
895 				record(analysisResult.reason);
896 				analysisResult.reason = null;
897 				decayActivities();
898 			}
899 		} while (undertimeout);
900 		return Lbool.UNDEFINED; // timeout occured
901 	}
902 
903 	protected void analyzeAtRootLevel(Constr conflict) {
904 	}
905 
906 	/**
907      * 
908      */
909 	void modelFound() {
910 		model = new int[trail.size()];
911 		fullmodel = new boolean[nVars()];
912 		int index = 0;
913 		for (int i = 1; i <= voc.nVars(); i++) {
914 			if (voc.belongsToPool(i)) {
915 				int p = voc.getFromPool(i);
916 				if (!voc.isUnassigned(p)) {
917 					model[index++] = voc.isSatisfied(p) ? i : -i;
918 					fullmodel[i - 1] = voc.isSatisfied(p);
919 				}
920 			}
921 		}
922 		assert index == model.length;
923 		cancelUntil(rootLevel);
924 	}
925 
926 	public boolean model(int var) {
927 		if (var <= 0 || var > nVars()) {
928 			throw new IllegalArgumentException(
929 					"Use a valid Dimacs var id as argument!"); //$NON-NLS-1$
930 		}
931 		if (fullmodel == null) {
932 			throw new UnsupportedOperationException(
933 					"Call the solve method first!!!"); //$NON-NLS-1$
934 		}
935 		return fullmodel[var - 1];
936 	}
937 
938 	/**
939      * 
940      */
941 	protected void reduceDB() {
942 		reduceDB(claInc / learnts.size());
943 	}
944 
945 	public void clearLearntClauses() {
946 		for (Iterator<Constr> iterator = learnts.iterator(); iterator.hasNext();)
947 			iterator.next().remove();
948 		learnts.clear();
949 	}
950 
951 	protected void reduceDB(double lim) {
952 		int i, j;
953 		sortOnActivity();
954 		stats.reduceddb++;
955 		for (i = j = 0; i < learnts.size() / 2; i++) {
956 			Constr c = learnts.get(i);
957 			if (c.locked()) {
958 				learnts.set(j++, learnts.get(i));
959 			} else {
960 				c.remove();
961 			}
962 		}
963 		for (; i < learnts.size(); i++) {
964 			// Constr c = learnts.get(i);
965 			// if (!c.locked() && (c.getActivity() < lim)) {
966 			// c.remove();
967 			// } else {
968 			learnts.set(j++, learnts.get(i));
969 			// }
970 		}
971 		System.out.println("c cleaning " + (learnts.size() - j) //$NON-NLS-1$
972 				+ " clauses out of " + learnts.size() + " for limit " + lim); //$NON-NLS-1$ //$NON-NLS-2$
973 		learnts.shrinkTo(j);
974 	}
975 
976 	/**
977 	 * @param learnts
978 	 */
979 	private void sortOnActivity() {
980 		learnts.sort(comparator);
981 	}
982 
983 	/**
984      * 
985      */
986 	protected void decayActivities() {
987 		order.varDecayActivity();
988 		claDecayActivity();
989 	}
990 
991 	/**
992      * 
993      */
994 	private void claDecayActivity() {
995 		claInc *= claDecay;
996 	}
997 
998 	/**
999 	 * @return true iff the set of constraints is satisfiable, else false.
1000 	 */
1001 	public boolean isSatisfiable() throws TimeoutException {
1002 		return isSatisfiable(VecInt.EMPTY);
1003 	}
1004 
1005 	/**
1006 	 * @return true iff the set of constraints is satisfiable, else false.
1007 	 */
1008 	public boolean isSatisfiable(boolean global) throws TimeoutException {
1009 		return isSatisfiable(VecInt.EMPTY, global);
1010 	}
1011 
1012 	private double timebegin = 0;
1013 
1014 	private boolean needToReduceDB;
1015 
1016 	private ConflictTimer conflictCount;
1017 
1018 	private transient Timer timer;
1019 
1020 	public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
1021 		return isSatisfiable(assumps, false);
1022 	}
1023 
1024 	public boolean isSatisfiable(IVecInt assumps, boolean global)
1025 			throws TimeoutException {
1026 		Lbool status = Lbool.UNDEFINED;
1027 
1028 		final int howmany = voc.nVars();
1029 		if (mseen.length < howmany) {
1030 			mseen = new boolean[howmany + 1];
1031 		}
1032 		trail.ensure(howmany);
1033 		trailLim.ensure(howmany);
1034 		learnedLiterals = 0;
1035 		order.init();
1036 		learner.init();
1037 		restarter.init(params);
1038 		timebegin = System.currentTimeMillis();
1039 		slistener.start();
1040 		model = null; // forget about previous model
1041 		fullmodel = null;
1042 
1043 		// propagate constraints
1044 		Constr confl = propagate();
1045 		if (confl != null) {
1046 			analyzeAtRootLevel(confl);
1047 			slistener.end(Lbool.FALSE);
1048 			cancelUntil(0);
1049 			return false;
1050 		}
1051 
1052 		// push incremental assumptions
1053 		for (IteratorInt iterator = assumps.iterator(); iterator.hasNext();) {
1054 			if (!assume(voc.getFromPool(iterator.next()))
1055 					|| (propagate() != null)) {
1056 				slistener.end(Lbool.FALSE);
1057 				cancelUntil(0);
1058 				return false;
1059 			}
1060 		}
1061 		rootLevel = decisionLevel();
1062 
1063 		final long memorybound = Runtime.getRuntime().freeMemory() / 10;
1064 
1065 		ConflictTimer freeMem = new ConflictTimerAdapter(500) {
1066 			private static final long serialVersionUID = 1L;
1067 
1068 			@Override
1069 			void run() {
1070 				long freemem = Runtime.getRuntime().freeMemory();
1071 				// System.out.println("c Free memory "+freemem);
1072 				if (freemem < memorybound) {
1073 					// Reduce the set of learnt clauses
1074 					needToReduceDB = true;
1075 				}
1076 			}
1077 		};
1078 
1079 		if (timeBasedTimeout) {
1080 			if (!global || timer == null) {
1081 				TimerTask stopMe = new TimerTask() {
1082 					@Override
1083 					public void run() {
1084 						undertimeout = false;
1085 					}
1086 				};
1087 				timer = new Timer(true);
1088 				timer.schedule(stopMe, timeout);
1089 				conflictCount = freeMem;
1090 			}
1091 		} else {
1092 			if (!global || conflictCount == null) {
1093 				ConflictTimer conflictTimeout = new ConflictTimerAdapter(
1094 						(int) timeout) {
1095 					private static final long serialVersionUID = 1L;
1096 
1097 					@Override
1098 					public void run() {
1099 						undertimeout = false;
1100 					}
1101 				};
1102 				conflictCount = new ConflictTimerContainer().add(
1103 						conflictTimeout).add(freeMem);
1104 			}
1105 		}
1106 		needToReduceDB = false;
1107 		undertimeout = true;
1108 
1109 		// Solve
1110 		while ((status == Lbool.UNDEFINED) && undertimeout) {
1111 			status = search(restarter.nextRestartNumberOfConflict());
1112 			// System.out.println("c speed
1113 			// "+(stats.decisions/((System.currentTimeMillis()-timebegin)/1000))+"
1114 			// dec/s, "+stats.starts+"/"+stats.conflicts);
1115 			restarter.onRestart();
1116 		}
1117 
1118 		cancelUntil(0);
1119 		if (!global && timeBasedTimeout) {
1120 			timer.cancel();
1121 			timer = null;
1122 		}
1123 		slistener.end(status);
1124 		if (!undertimeout) {
1125 			throw new TimeoutException(" Timeout (" + timeout + "s) exceeded"); //$NON-NLS-1$//$NON-NLS-2$
1126 		}
1127 		return status == Lbool.TRUE;
1128 	}
1129 
1130 	public void printInfos(PrintWriter out, String prefix) {
1131 		out.print(prefix);
1132 		out.println("constraints type ");
1133 		for (Map.Entry<String, Counter> entry : constrTypes.entrySet()) {
1134 			out.println(prefix + entry.getKey() + " => " + entry.getValue());
1135 		}
1136 	}
1137 
1138 	public void printLearntClausesInfos(PrintWriter out, String prefix) {
1139 		Map<String,Counter> learntTypes = new HashMap<String,Counter>();
1140 		for (Iterator<Constr> it = learnts.iterator(); it.hasNext();) {
1141 			String type = it.next().getClass().getName();
1142 			Counter count = learntTypes.get(type);
1143 			if (count == null) {
1144 				learntTypes.put(type, new Counter());
1145 			} else {
1146 				count.inc();
1147 			}
1148 		}
1149 		out.print(prefix);
1150 		out.println("learnt constraints type ");
1151 		for (Map.Entry<String, Counter> entry : learntTypes.entrySet()) {
1152 			out.println(prefix + entry.getKey() + " => " + entry.getValue());
1153 		}
1154 	}
1155 
1156 	public SolverStats getStats() {
1157 		return stats;
1158 	}
1159 
1160 	public IOrder<L> getOrder() {
1161 		return order;
1162 	}
1163 
1164 	public void setOrder(IOrder<L> h) {
1165 		order = h;
1166 		order.setLits(voc);
1167 	}
1168 
1169 	public L getVocabulary() {
1170 		return voc;
1171 	}
1172 
1173 	public void reset() {
1174 		// FIXME verify that cleanup is OK
1175 		voc.resetPool();
1176 		dsfactory.reset();
1177 		constrs.clear();
1178 		learnts.clear();
1179 		stats.reset();
1180 		constrTypes.clear();
1181 	}
1182 
1183 	public int nVars() {
1184 		return voc.nVars();
1185 	}
1186 
1187 	/**
1188 	 * @param constr
1189 	 *            a constraint implementing the Constr interface.
1190 	 * @return a reference to the constraint for external use.
1191 	 */
1192 	protected IConstr addConstr(Constr constr) {
1193 		if (constr != null) {
1194 			constrs.push(constr);
1195 			String type = constr.getClass().getName();
1196 			Counter count = constrTypes.get(type);
1197 			if (count == null) {
1198 				constrTypes.put(type, new Counter());
1199 			} else {
1200 				count.inc();
1201 			}
1202 		}
1203 		return constr;
1204 	}
1205 
1206 	public DataStructureFactory<L> getDSFactory() {
1207 		return dsfactory;
1208 	}
1209 
1210 	public IVecInt getOutLearnt() {
1211 		return outLearnt;
1212 	}
1213 
1214 	/**
1215 	 * returns the ith constraint in the solver.
1216 	 * 
1217 	 * @param i
1218 	 *            the constraint number (begins at 0)
1219 	 * @return the ith constraint
1220 	 */
1221 	public IConstr getIthConstr(int i) {
1222 		return constrs.get(i);
1223 	}
1224 
1225 	/*
1226 	 * (non-Javadoc)
1227 	 * 
1228 	 * @see org.sat4j.specs.ISolver#printStat(java.io.PrintStream,
1229 	 * java.lang.String)
1230 	 */
1231 	public void printStat(PrintStream out, String prefix) {
1232 		printStat(new PrintWriter(out), prefix);
1233 	}
1234 
1235 	public void printStat(PrintWriter out, String prefix) {
1236 		stats.printStat(out, prefix);
1237 		double cputime = (System.currentTimeMillis() - timebegin) / 1000;
1238 		out.println(prefix
1239 				+ "speed (assignments/second)\t: " + stats.propagations //$NON-NLS-1$
1240 				/ cputime);
1241 		order.printStat(out, prefix);
1242 		printLearntClausesInfos(out, prefix);
1243 	}
1244 
1245 	/*
1246 	 * (non-Javadoc)
1247 	 * 
1248 	 * @see java.lang.Object#toString()
1249 	 */
1250 	public String toString(String prefix) {
1251 		StringBuffer stb = new StringBuffer();
1252 		Object[] objs = { analyzer, dsfactory, learner, params, order,
1253 				simplifier, restarter };
1254 		stb.append(prefix);
1255 		stb.append("--- Begin Solver configuration ---"); //$NON-NLS-1$
1256 		stb.append("\n"); //$NON-NLS-1$
1257 		for (Object o : objs) {
1258 			stb.append(prefix);
1259 			stb.append(o.toString());
1260 			stb.append("\n"); //$NON-NLS-1$
1261 		}
1262 		stb.append(prefix);
1263 		stb.append("timeout=");
1264 		if (timeBasedTimeout) {
1265 			stb.append(timeout / 1000);
1266 			stb.append("s\n");
1267 		} else {
1268 			stb.append(timeout);
1269 			stb.append(" conflicts\n");
1270 		}
1271 		stb.append(prefix);
1272 		stb.append("DB Simplification allowed=");
1273 		stb.append(isDBSimplificationAllowed);
1274 		stb.append("\n");
1275 		stb.append(prefix);
1276 		stb.append("--- End Solver configuration ---"); //$NON-NLS-1$
1277 		return stb.toString();
1278 	}
1279 
1280 	/*
1281 	 * (non-Javadoc)
1282 	 * 
1283 	 * @see java.lang.Object#toString()
1284 	 */
1285 	@Override
1286 	public String toString() {
1287 		return toString(""); //$NON-NLS-1$
1288 	}
1289 
1290 	public int getTimeout() {
1291 		return (int) (timeBasedTimeout ? timeout / 1000 : timeout);
1292 	}
1293 
1294 	public long getTimeoutMs() {
1295 		if (!timeBasedTimeout) {
1296 			throw new UnsupportedOperationException(
1297 					"The timeout is given in number of conflicts!");
1298 		}
1299 		return timeout;
1300 	}
1301 
1302 	public void setExpectedNumberOfClauses(int nb) {
1303 		constrs.ensure(nb);
1304 	}
1305 
1306 	public Map<String, Number> getStat() {
1307 		return stats.toMap();
1308 	}
1309 
1310 	public int[] findModel() throws TimeoutException {
1311 		if (isSatisfiable()) {
1312 			return model();
1313 		}
1314 		// DLB findbugs ok
1315 		// A zero length array would mean that the formula is a tautology.
1316 		return null;
1317 	}
1318 
1319 	public int[] findModel(IVecInt assumps) throws TimeoutException {
1320 		if (isSatisfiable(assumps)) {
1321 			return model();
1322 		}
1323 		// DLB findbugs ok
1324 		// A zero length array would mean that the formula is a tautology.
1325 		return null;
1326 	}
1327 
1328 	public boolean isDBSimplificationAllowed() {
1329 		return isDBSimplificationAllowed;
1330 	}
1331 
1332 	public void setDBSimplificationAllowed(boolean status) {
1333 		isDBSimplificationAllowed = status;
1334 	}
1335 
1336 }
1337 
1338 class ActivityComparator implements Comparator<Constr>, Serializable {
1339 
1340 	private static final long serialVersionUID = 1L;
1341 
1342 	/*
1343 	 * (non-Javadoc)
1344 	 * 
1345 	 * @see java.util.Comparator#compare(java.lang.Object, java.lang.Object)
1346 	 */
1347 	public int compare(Constr c1, Constr c2) {
1348 		return (int) Math.round(c1.getActivity() - c2.getActivity());
1349 	}
1350 }
1351 
1352 interface ConflictTimer {
1353 
1354 	void reset();
1355 
1356 	void newConflict();
1357 }
1358 
1359 abstract class ConflictTimerAdapter implements Serializable, ConflictTimer {
1360 
1361 	/**
1362 	 * 
1363 	 */
1364 	private static final long serialVersionUID = 1L;
1365 
1366 	private int counter;
1367 
1368 	private final int bound;
1369 
1370 	ConflictTimerAdapter(final int bound) {
1371 		this.bound = bound;
1372 		counter = 0;
1373 	}
1374 
1375 	public void reset() {
1376 		counter = 0;
1377 	}
1378 
1379 	public void newConflict() {
1380 		counter++;
1381 		if (counter == bound) {
1382 			run();
1383 			counter = 0;
1384 		}
1385 	}
1386 
1387 	abstract void run();
1388 }
1389 
1390 class ConflictTimerContainer implements Serializable, ConflictTimer {
1391 
1392 	/**
1393 	 * 
1394 	 */
1395 	private static final long serialVersionUID = 1L;
1396 
1397 	private final IVec<ConflictTimer> timers = new Vec<ConflictTimer>();
1398 
1399 	ConflictTimerContainer add(ConflictTimer timer) {
1400 		timers.push(timer);
1401 		return this;
1402 	}
1403 
1404 	public void reset() {
1405 		Iterator<ConflictTimer> it = timers.iterator();
1406 		while (it.hasNext()) {
1407 			it.next().reset();
1408 		}
1409 	}
1410 
1411 	public void newConflict() {
1412 		Iterator<ConflictTimer> it = timers.iterator();
1413 		while (it.hasNext()) {
1414 			it.next().newConflict();
1415 		}
1416 	}
1417 }