Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
396   1 227   79   4,66
184   771   0,41   21,25
85     1,92  
4    
 
  Solver       Line # 60 388 78 72,5% 0.7250384
  Solver.ISimplifier       Line # 474 0 1 - -1.0
  ActivityComparator       Line # 1190 1 1 100% 1.0
  ConflictTimer       Line # 1204 7 2 83,3% 0.8333333
 
  (187)
 
1    /*
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le Berre
3    *
4    * Based on the original minisat specification from:
5    *
6    * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the
7    * Sixth International Conference on Theory and Applications of Satisfiability
8    * Testing, LNCS 2919, pp 502-518, 2003.
9    *
10    * This library is free software; you can redistribute it and/or modify it under
11    * the terms of the GNU Lesser General Public License as published by the Free
12    * Software Foundation; either version 2.1 of the License, or (at your option)
13    * any later version.
14    *
15    * This library is distributed in the hope that it will be useful, but WITHOUT
16    * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
17    * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
18    * details.
19    *
20    * You should have received a copy of the GNU Lesser General Public License
21    * along with this library; if not, write to the Free Software Foundation, Inc.,
22    * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
23    *
24    */
25   
26    package org.sat4j.minisat.core;
27   
28    import static org.sat4j.minisat.core.LiteralsUtils.neg;
29    import static org.sat4j.minisat.core.LiteralsUtils.var;
30   
31    import java.io.PrintStream;
32    import java.io.PrintWriter;
33    import java.io.Serializable;
34    import java.lang.reflect.Field;
35    import java.math.BigInteger;
36    import java.util.Comparator;
37    import java.util.Map;
38    import java.util.Timer;
39    import java.util.TimerTask;
40   
41    import org.sat4j.core.Vec;
42    import org.sat4j.core.VecInt;
43    import org.sat4j.minisat.constraints.cnf.WLClause;
44    import org.sat4j.minisat.restarts.ArminRestarts;
45    import org.sat4j.minisat.restarts.LubyRestarts;
46    import org.sat4j.minisat.restarts.MiniSATRestarts;
47    import org.sat4j.specs.ContradictionException;
48    import org.sat4j.specs.IConstr;
49    import org.sat4j.specs.ISolver;
50    import org.sat4j.specs.IVec;
51    import org.sat4j.specs.IVecInt;
52    import org.sat4j.specs.TimeoutException;
53   
54    /**
55    * The backbone of the library providing the modular implementation of a MiniSAT
56    * (Chaff) like solver.
57    *
58    * @author leberre
59    */
 
60    public class Solver<L extends ILits> implements ISolver, UnitPropagationListener,
61    ActivityListener, Learner {
62   
63    private static final long serialVersionUID = 1L;
64   
65    private static final double CLAUSE_RESCALE_FACTOR = 1e-20;
66   
67    private static final double CLAUSE_RESCALE_BOUND = 1 / CLAUSE_RESCALE_FACTOR;
68   
69    /**
70    * List des contraintes du probl?me.
71    */
72    private final IVec<Constr> constrs = new Vec<Constr>(); // Constr
73   
74    /**
75    * Liste des clauses apprises.
76    */
77    private final IVec<Constr> learnts = new Vec<Constr>(); // Clause
78   
79    /**
80    * incr?ment pour l'activit? des clauses.
81    */
82    private double claInc = 1.0;
83   
84    /**
85    * decay factor pour l'activit? des clauses.
86    */
87    private double claDecay = 1.0;
88   
89    /**
90    * Queue de propagation
91    */
92    // private final IntQueue propQ = new IntQueue(); // Lit
93    // head of the queue in trail ... (taken from MiniSAT 1.14)
94    private int qhead = 0;
95   
96    // queue
97   
98    /**
99    * affectation en ordre chronologique
100    */
101    protected final IVecInt trail = new VecInt(); // lit
102   
103    // vector
104   
105    /**
106    * indice des s?parateurs des diff?rents niveau de d?cision dans trail
107    */
108    protected final IVecInt trailLim = new VecInt(); // int
109   
110    // vector
111   
112    /**
113    * S?pare les hypoth?ses incr?mentale et recherche
114    */
115    protected int rootLevel;
116   
117    private int[] model = null;
118   
119    protected L voc;
120   
121    private IOrder<L> order;
122   
123    private final ActivityComparator comparator = new ActivityComparator();
124   
125    private final SolverStats stats = new SolverStats();
126   
127    private final LearningStrategy<L> learner;
128   
129    protected final AssertingClauseGenerator analyzer;
130   
131    private boolean undertimeout;
132   
133    private long timeout = Integer.MAX_VALUE;
134   
135    protected DataStructureFactory<L> dsfactory;
136   
137    private SearchParams params;
138   
139    private final IVecInt __dimacs_out = new VecInt();
140   
141    private SearchListener slistener = new NullSearchListener();
142   
143    private RestartStrategy restarter;
144   
 
145  5693172 toggle protected IVecInt dimacs2internal(IVecInt in) {
146  5693172 if (voc.nVars() == 0) {
147  0 throw new RuntimeException(
148    "Please set the number of variables (solver.newVar() or solver.newVar(maxvar)) before adding constraints!");
149    }
150  5693172 __dimacs_out.clear();
151  5693172 __dimacs_out.ensure(in.size());
152  30108294 for (int i = 0; i < in.size(); i++) {
153  24415122 assert (in.get(i) != 0) && (Math.abs(in.get(i)) <= voc.nVars());
154  24415122 __dimacs_out.unsafePush(voc.getFromPool(in.get(i)));
155    }
156  5693172 return __dimacs_out;
157    }
158   
159    /**
160    * creates a Solver without LearningListener. A learningListener must be
161    * added to the solver, else it won't backtrack!!! A data structure factory
162    * must be provided, else it won't work either.
163    *
164    * @param acg
165    * an asserting clause generator
166    */
167   
 
168  1708 toggle public Solver(AssertingClauseGenerator acg, LearningStrategy<L> learner,
169    DataStructureFactory<L> dsf, IOrder<L> order) {
170  1708 this(acg, learner, dsf, new SearchParams(), order);
171    }
172   
 
173  2515 toggle public Solver(AssertingClauseGenerator acg, LearningStrategy<L> learner,
174    DataStructureFactory<L> dsf, SearchParams params, IOrder<L> order) {
175  2515 this(acg,learner,dsf,params,order,new MiniSATRestarts());
176    }
177   
 
178  2515 toggle public Solver(AssertingClauseGenerator acg, LearningStrategy<L> learner,
179    DataStructureFactory<L> dsf, SearchParams params, IOrder<L> order, RestartStrategy restarter) {
180  2515 analyzer = acg;
181  2515 this.learner = learner;
182  2515 this.order = order;
183  2515 this.params = params;
184  2515 setDataStructureFactory(dsf);
185  2515 this.restarter = restarter;
186    }
187   
188    /**
189    * Change the internatal representation of the contraints. Note that the
190    * heuristics must be changed prior to calling that method.
191    *
192    * @param dsf
193    * the internal factory
194    */
 
195  2515 toggle public final void setDataStructureFactory(DataStructureFactory<L> dsf) {
196  2515 dsfactory = dsf;
197  2515 dsfactory.setUnitPropagationListener(this);
198  2515 dsfactory.setLearner(this);
199  2515 voc = dsf.getVocabulary();
200  2515 order.setLits(voc);
201    }
202   
 
203  0 toggle public void setSearchListener(SearchListener sl) {
204  0 slistener = sl;
205    }
206   
 
207  2410 toggle public void setTimeout(int t) {
208  2410 timeout = t*1000L;
209    }
210   
 
211  0 toggle public void setTimeoutMs(long t) {
212  0 timeout = t;
213    }
214   
 
215  2 toggle public void setSearchParams(SearchParams sp) {
216  2 params = sp;
217    }
218   
 
219  3 toggle public void setRestartStrategy(RestartStrategy restarter) {
220  3 this.restarter = restarter;
221    }
222   
 
223  533961096 toggle protected int nAssigns() {
224  533961096 return trail.size();
225    }
226   
 
227  0 toggle public int nConstraints() {
228  0 return constrs.size();
229    }
230   
 
231  6441191 toggle public void learn(Constr c) {
232  6441191 learnts.push(c);
233  6441191 c.setLearnt();
234  6441191 c.register();
235  6441191 stats.learnedclauses++;
236  6441191 switch (c.size()) {
237  3462 case 2:
238  3462 stats.learnedbinaryclauses++;
239  3462 break;
240  4185 case 3:
241  4185 stats.learnedternaryclauses++;
242  4185 break;
243  6433544 default:
244    // do nothing
245    }
246    }
247   
 
248  17608096 toggle public int decisionLevel() {
249  17608096 return trailLim.size();
250    }
251   
 
252  741714 toggle public int newVar() {
253  741714 int index = voc.nVars() + 1;
254  741714 voc.ensurePool(index);
255  741714 mseen = new boolean[index + 1];
256  741714 trail.ensure(index);
257  741714 trailLim.ensure(index);
258  741714 order.newVar();
259  741714 return index;
260    }
261   
 
262  1686 toggle public int newVar(int howmany) {
263  1686 voc.ensurePool(howmany);
264  1686 order.newVar(howmany);
265  1686 mseen = new boolean[howmany + 1];
266  1686 trail.ensure(howmany);
267  1686 trailLim.ensure(howmany);
268  1686 return voc.nVars();
269    }
270   
 
271  4011536 toggle public IConstr addClause(IVecInt literals) throws ContradictionException {
272  4011536 IVecInt vlits = dimacs2internal(literals);
273  4011536 return addConstr(dsfactory.createClause(vlits));
274    }
275   
 
276  4 toggle public boolean removeConstr(IConstr co) {
277  4 if (co == null) {
278  0 throw new UnsupportedOperationException(
279    "Reference to the constraint to remove needed!"); //$NON-NLS-1$
280    }
281  4 Constr c = (Constr) co;
282  4 c.remove();
283  4 constrs.remove(c);
284  4 clearLearntClauses();
285  4 cancelLearntLiterals();
286  4 return true;
287    }
288   
 
289  1681623 toggle public IConstr addPseudoBoolean(IVecInt literals, IVec<BigInteger> coeffs,
290    boolean moreThan, BigInteger degree) throws ContradictionException {
291  1681623 IVecInt vlits = dimacs2internal(literals);
292  1681623 assert vlits.size() == literals.size();
293  1681623 assert literals.size() == coeffs.size();
294  1681623 return addConstr(dsfactory.createPseudoBooleanConstraint(vlits, coeffs,
295    moreThan, degree));
296    }
297   
 
298  0 toggle public void addAllClauses(IVec<IVecInt> clauses)
299    throws ContradictionException {
300  0 for (IVecInt clause : clauses) {
301  0 addClause(clause);
302    }
303    }
304   
 
305  13 toggle public IConstr addAtMost(IVecInt literals, int degree)
306    throws ContradictionException {
307  13 int n = literals.size();
308  13 IVecInt opliterals = new VecInt(n);
309  13 for (int p : literals) {
310  39 opliterals.push(-p);
311    }
312  13 return addAtLeast(opliterals, n - degree);
313    }
314   
 
315  13 toggle public IConstr addAtLeast(IVecInt literals, int degree)
316    throws ContradictionException {
317  13 IVecInt vlits = dimacs2internal(literals);
318  13 return addConstr(dsfactory.createCardinalityConstraint(vlits, degree));
319    }
320   
 
321  0 toggle @SuppressWarnings("unchecked")
322    public boolean simplifyDB() {
323    // aucune raison de recommencer un propagate?
324    // if (propagate() != null) {
325    // // Un conflit est d?couvert, la base est inconsistante
326    // return false;
327    // }
328   
329    // Simplifie la base de clauses apres la premiere propagation des
330    // clauses unitaires
331  0 IVec<Constr>[] cs = new IVec[] { constrs, learnts };
332  0 for (int type = 0; type < 2; type++) {
333  0 int j = 0;
334  0 for (int i = 0; i < cs[type].size(); i++) {
335  0 if (cs[type].get(i).simplify()) {
336    // enleve les contraintes satisfaites de la base
337  0 cs[type].get(i).remove();
338    } else {
339  0 cs[type].moveTo(j++, i);
340    }
341    }
342  0 cs[type].shrinkTo(j);
343    }
344  0 return true;
345    }
346   
347    /**
348    * Si un mod?le est trouv?, ce vecteur contient le mod?le.
349    *
350    * @return un mod?le de la formule.
351    */
 
352  43 toggle public int[] model() {
353  43 if (model == null) {
354  2 throw new UnsupportedOperationException(
355    "Call the solve method first!!!"); //$NON-NLS-1$
356    }
357  41 int[] nmodel = new int[model.length];
358  41 System.arraycopy(model, 0, nmodel, 0, model.length);
359  41 return nmodel;
360    }
361   
362    /**
363    * Satisfait un litt?ral
364    *
365    * @param p
366    * le litt?ral
367    * @return true si tout se passe bien, false si un conflit appara?t.
368    */
 
369  266953416 toggle public boolean enqueue(int p) {
370  266953416 return enqueue(p, null);
371    }
372   
373    /**
374    * Put the literal on the queue of assignments to be done.
375    *
376    * @param p
377    * the literal.
378    * @param from
379    * the reason to propagate that literal, else null
380    * @return true if the asignment can be made, false if a conflict is
381    * detected.
382    */
 
383    toggle public boolean enqueue(int p, Constr from) {
384    assert p > 1;
385    if (voc.isSatisfied(p)) {
386    // literal is already satisfied. Skipping.
387    return true;
388    }
389    if (voc.isFalsified(p)) {
390    // conflicting enqueued assignment
391  129662024 return false;
392    }
393    // new fact, store it
394    voc.satisfies(p);
395    voc.setLevel(p, decisionLevel());
396    voc.setReason(p, from);
397    trail.push(p);
398    return true;
399    }
400   
401    private boolean[] mseen = new boolean[0];
402   
403    private final IVecInt preason = new VecInt();
404   
405    private final IVecInt outLearnt = new VecInt();
406   
 
407  182717725 toggle public int analyze(Constr confl, Handle<Constr> outLearntRef) {
408  182717725 assert confl != null;
409  182717725 outLearnt.clear();
410   
411  182717725 final boolean[] seen = mseen;
412   
413  182717725 assert outLearnt.size() == 0;
414    for (int i = 0; i < seen.length; i++) {
415    seen[i] = false;
416    }
417   
418  182717725 analyzer.initAnalyze();
419  182717725 int p = ILits.UNDEFINED;
420   
421  182717725 outLearnt.push(ILits.UNDEFINED);
422    // reserve de la place pour le litteral falsifie
423  182717725 int outBtlevel = 0;
424   
425  182717725 do {
426  1836803003 preason.clear();
427  1836803003 assert confl != null;
428  1836803003 confl.calcReason(p, preason);
429  1836803003 if (confl.learnt())
430  168735687 claBumpActivity(confl);
431    // Trace reason for p
432    for (int j = 0; j < preason.size(); j++) {
433  449580690 int q = preason.get(j);
434  449580690 order.updateVar(q);
435  449580690 if (!seen[q >> 1]) {
436    // order.updateVar(q); // MINISAT
437    seen[q >> 1] = true;
438    if (voc.getLevel(q) == decisionLevel()) {
439  1836803003 analyzer.onCurrentDecisionLevelLiteral(q);
440  1444445589 } else if (voc.getLevel(q) > 0) {
441    // ajoute les variables depuis le niveau de d?cision 0
442  1430091758 outLearnt.push(q ^ 1);
443  1430091758 outBtlevel = Math.max(outBtlevel, voc.getLevel(q));
444    }
445    }
446    }
447   
448    // select next reason to look at
449  1836803003 do {
450    p = trail.last();
451    // System.err.print((Clause.lastid()+1)+"
452    // "+((Clause)confl).getId()+" ");
453    confl = voc.getReason(p);
454    // System.err.println(((Clause)confl).getId());
455    // assert(confl != null) || counter == 1;
456    undoOne();
457    } while (!seen[p >> 1]);
458    // seen[p.var] indique que p se trouve dans outLearnt ou dans
459    // le dernier niveau de d?cision
460  1836803003 } while (analyzer.clauseNonAssertive(confl));
461   
462  182717725 outLearnt.set(0, p ^ 1);
463  182717725 simplifier.simplify(outLearnt);
464   
465  182717725 Constr c = dsfactory.createUnregisteredClause(outLearnt);
466  182717725 slistener.learn(c);
467   
468  182717725 outLearntRef.obj = c;
469   
470  182717725 assert outBtlevel > -1;
471  182717725 return outBtlevel;
472    }
473   
 
474    interface ISimplifier extends Serializable {
475    void simplify(IVecInt outLearnt);
476    }
477   
478    public static final ISimplifier NO_SIMPLIFICATION = new ISimplifier() {
479    /**
480    *
481    */
482    private static final long serialVersionUID = 1L;
483   
 
484  144329993 toggle public void simplify(IVecInt outLearnt) {
485    }
486   
 
487  0 toggle @Override
488    public String toString() {
489  0 return "No reason simplification"; //$NON-NLS-1$
490    }
491    };
492   
493    public final ISimplifier SIMPLE_SIMPLIFICATION = new ISimplifier() {
494    /**
495    *
496    */
497    private static final long serialVersionUID = 1L;
498   
 
499  18170400 toggle public void simplify(IVecInt outLearnt) {
500  18170400 simpleSimplification(outLearnt);
501    }
502   
 
503  0 toggle @Override
504    public String toString() {
505  0 return "Simple reason simplification"; //$NON-NLS-1$
506    }
507    };
508   
509    public final ISimplifier EXPENSIVE_SIMPLIFICATION = new ISimplifier() {
510   
511    /**
512    *
513    */
514    private static final long serialVersionUID = 1L;
515   
 
516  20217332 toggle public void simplify(IVecInt outLearnt) {
517  20217332 expensiveSimplification(outLearnt);
518    }
519   
 
520  0 toggle @Override
521    public String toString() {
522  0 return "Expensive reason simplification"; //$NON-NLS-1$
523    }
524    };
525   
526    private ISimplifier simplifier = NO_SIMPLIFICATION;
527   
528    /**
529    * Setup the reason simplification strategy.
530    * By default, there is no reason simplification.
531    * NOTE THAT REASON SIMPLIFICATION IS ONLY ALLOWED FOR WL
532    * CLAUSAL data structures. USING REASON SIMPLIFICATION
533    * ON CB CLAUSES, CARDINALITY CONSTRAINTS OR PB CONSTRAINTS
534    * MIGHT RESULT IN INCORRECT RESULTS.
535    *
536    * @param simp the name of the simplifier (one of NO_SIMPLIFICATION, SIMPLE_SIMPLIFICATION, EXPENSIVE_SIMPLIFICATION).
537    */
 
538  0 toggle public void setSimplifier(String simp) {
539  0 Field f;
540  0 try {
541  0 f = Solver.class.getDeclaredField(simp);
542  0 simplifier = (ISimplifier) f.get(this);
543    } catch (Exception e) {
544  0 e.printStackTrace();
545  0 simplifier = NO_SIMPLIFICATION;
546    }
547    }
548   
549    /**
550    * Setup the reason simplification strategy.
551    * By default, there is no reason simplification.
552    * NOTE THAT REASON SIMPLIFICATION IS ONLY ALLOWED FOR WL
553    * CLAUSAL data structures. USING REASON SIMPLIFICATION
554    * ON CB CLAUSES, CARDINALITY CONSTRAINTS OR PB CONSTRAINTS
555    * MIGHT RESULT IN INCORRECT RESULTS.
556    *
557    * @param simp
558    */
 
559  11 toggle public void setSimplifier(ISimplifier simp) {
560  11 simplifier = simp;
561    }
562   
563    // Taken from MiniSAT 1.14: Simplify conflict clause (a little):
 
564  18170400 toggle private void simpleSimplification(IVecInt outLearnt) {
565  18170400 int i, j;
566  18170400 final boolean[] seen = mseen;
567  424708347 for (i = j = 1; i < outLearnt.size(); i++) {
568  406537947 IConstr r = voc.getReason(outLearnt.get(i));
569  406537947 if (r == null) {
570  149530649 outLearnt.moveTo(j++, i);
571    } else {
572  257007298 assert WLClause.class.isAssignableFrom(r.getClass());
573  257007298 assert r.get(0) == neg(outLearnt.get(i));
574  538282038 for (int k = 1; k < r.size(); k++)
575  534112670 if (!seen[r.get(k) >> 1] && (voc.getLevel(r.get(k)) != 0)) {
576  252837930 outLearnt.moveTo(j++, i);
577  252837930 break;
578    }
579    }
580    }
581  18170400 outLearnt.shrink(i - j);
582  18170400 stats.reducedliterals += (i - j);
583    }
584   
585    private final IVecInt analyzetoclear = new VecInt();
586   
587    private final IVecInt analyzestack = new VecInt();
588   
589    // Taken from MiniSAT 1.14
 
590  20217332 toggle private void expensiveSimplification(IVecInt outLearnt) {
591    // Simplify conflict clause (a lot):
592    //
593  20217332 int i, j;
594    // (maintain an abstraction of levels involved in conflict)
595  20217332 analyzetoclear.clear();
596  20217332 outLearnt.copyTo(analyzetoclear);
597  465143177 for (i = 1, j = 1; i < outLearnt.size(); i++)
598  444925845 if (voc.getReason(outLearnt.get(i)) == null
599    || !analyzeRemovable(outLearnt.get(i)))
600  439626289 outLearnt.moveTo(j++, i);
601  20217332 outLearnt.shrink(i - j);
602  20217332 stats.reducedliterals += (i - j);
603    }
604   
605    // Check if 'p' can be removed. 'min_level' is used to abort early if
606    // visiting literals at a level that cannot be removed.
607    //
 
608  253682021 toggle private boolean analyzeRemovable(int p) {
609  253682021 assert voc.getReason(p) != null;
610  253682021 analyzestack.clear();
611  253682021 analyzestack.push(p);
612  253682021 final boolean[] seen = mseen;
613  253682021 int top = analyzetoclear.size();
614  378518240 while (analyzestack.size() > 0) {
615  373218684 int q = analyzestack.last();
616  373218684 assert voc.getReason(q) != null;
617  373218684 Constr c = voc.getReason(q);
618  373218684 assert WLClause.class.isAssignableFrom(c.getClass());
619  373218684 analyzestack.pop();
620  373218684 assert c.get(0) == neg(q);
621  1581939042 for (int i = 1; i < c.size(); i++) {
622  1457102823 int l = c.get(i);
623  1457102823 if (!seen[var(l)] && voc.getLevel(l) != 0) {
624  660426667 if (voc.getReason(l) == null) {
625  660174179 for (int j = top; j < analyzetoclear.size(); j++)
626  411791714 seen[analyzetoclear.get(j) >> 1] = false;
627  248382465 analyzetoclear.shrink(analyzetoclear.size() - top);
628  248382465 return false;
629    }
630  412044202 seen[l >> 1] = true;
631  412044202 analyzestack.push(l);
632  412044202 analyzetoclear.push(l);
633    }
634    }
635    }
636   
637  5299556 return true;
638    }
639   
640    /**
641    * decode the internal representation of a literal into Dimacs format.
642    *
643    * @param p
644    * the literal in internal representation
645    * @return the literal in dimacs representation
646    */
 
647    toggle public static int decode2dimacs(int p) {
648    return ((p & 1) == 0 ? 1 : -1) * (p >> 1);
649    }
650   
651    /**
652    *
653    */
 
654    toggle protected void undoOne() {
655    // recupere le dernier litteral affecte
656    int p = trail.last();
657    assert p > 1;
658    assert voc.getLevel(p) >= 0;
659    int x = p >> 1;
660    // desaffecte la variable
661    voc.unassign(p);
662    voc.setReason(p, null);
663    voc.setLevel(p, -1);
664    // met a jour l'heuristique
665    order.undo(x);
666    // depile le litteral des affectations
667    trail.pop();
668    // met a jour les contraintes apres desaffectation du litteral :
669    // normalement, il n'y a rien a faire ici pour les prouveurs de type
670    // Chaff??
671    IVec<Undoable> undos = voc.undos(p);
672    assert undos != null;
673    while (undos.size() > 0) {
674    undos.last().undo(p);
675    undos.pop();
676    }
677    }
678   
679    /**
680    * Propagate activity to a constraint
681    *
682    * @param confl
683    * a constraint
684    */
 
685  168735687 toggle public void claBumpActivity(Constr confl) {
686  168735687 confl.incActivity(claInc);
687  168735687 if (confl.getActivity() > CLAUSE_RESCALE_BOUND)
688  83474 claRescalActivity();
689    // for (int i = 0; i < confl.size(); i++) {
690    // varBumpActivity(confl.get(i));
691    // }
692    }
693   
 
694  1734576741 toggle public void varBumpActivity(int p) {
695  1734576741 order.updateVar(p);
696    }
697   
 
698  83474 toggle private void claRescalActivity() {
699  7330814 for (int i = 0; i < learnts.size(); i++) {
700  7247340 learnts.get(i).rescaleBy(CLAUSE_RESCALE_FACTOR);
701    }
702  83474 claInc *= CLAUSE_RESCALE_FACTOR;
703    }
704   
705    /**
706    * @return null if not conflict is found, else a conflicting constraint.
707    */
 
708  450983468 toggle public Constr propagate() {
709    while (qhead < trail.size()) {
710    stats.propagations++;
711    int p = trail.get(qhead++);
712    slistener.propagating(decode2dimacs(p));
713    order.assignLiteral(p);
714    // p is the literal to propagate
715    // Moved original MiniSAT code to dsfactory to avoid
716    // watches manipulation in counter Based clauses for instance.
717    assert p > 1;
718    IVec<Propagatable> constrs = dsfactory.getWatchesFor(p);
719   
720    final int size = constrs.size();
721    for (int i = 0; i < size; i++) {
722  181623279 stats.inspects++;
723  181623279 if (!constrs.get(i).propagate(this, p)) {
724    // Constraint is conflicting: copy remaining watches to
725    // watches[p]
726    // and return constraint
727  184000433 dsfactory.conflictDetectedInWatchesFor(p, i);
728  184000433 qhead = trail.size(); // propQ.clear();
729    // FIXME enlever le transtypage
730  184000433 return (Constr) constrs.get(i);
731    }
732    }
733    }
734  266983035 return null;
735    }
736   
 
737  183999350 toggle void record(Constr constr) {
738  183999350 constr.assertConstraint(this);
739  183999350 slistener.adding(decode2dimacs(constr.get(0)));
740  183999350 if (constr.size() == 1) {
741  4593 stats.learnedliterals++;
742    } else {
743  183994757 learner.learns(constr);
744    }
745    }
746   
747    /**
748    * @return false ssi conflit imm?diat.
749    */
 
750  266952775 toggle public boolean assume(int p) {
751    // Precondition: assume propagation queue is empty
752  266952775 assert trail.size() == qhead;
753  266952775 trailLim.push(trail.size());
754  266952775 return enqueue(p);
755    }
756   
757    /**
758    * Revert to the state before the last push()
759    */
 
760  266831296 toggle private void cancel() {
761    // assert trail.size() == qhead || !undertimeout;
762  266831296 int decisionvar = trail.unsafeGet(trailLim.last());
763  266831296 slistener.backtracking(decode2dimacs(decisionvar));
764  661650948 for (int c = trail.size() - trailLim.last(); c > 0; c--) {
765  394819652 undoOne();
766    }
767  266831296 trailLim.pop();
768    }
769   
770    /**
771    * Restore literals
772    */
 
773  4 toggle private void cancelLearntLiterals() {
774    // assert trail.size() == qhead || !undertimeout;
775   
776  8 for (int c = trail.size() - rootLevel; c > 0; c--) {
777  4 undoOne();
778    }
779  4 qhead = trail.size();
780    }
781   
782    /**
783    * Cancel several levels of assumptions
784    *
785    * @param level
786    */
 
787  184029739 toggle protected void cancelUntil(int level) {
788  450861035 while (decisionLevel() > level) {
789  266831296 cancel();
790    }
791  184029739 qhead = trail.size();
792    }
793   
794    private final Handle<Constr> learntConstraint = new Handle<Constr>();
795   
796    private boolean[] fullmodel;
797   
 
798  28993 toggle Lbool search(long nofConflicts) {
799  28993 assert rootLevel == decisionLevel();
800  28993 stats.starts++;
801  28993 int conflictC = 0;
802   
803    // varDecay = 1 / params.varDecay;
804  28993 order.setVarDecay(1 / params.getVarDecay());
805  28993 claDecay = 1 / params.getClaDecay();
806   
807  28993 do {
808  450980979 slistener.beginLoop();
809    // propage les clauses unitaires
810  450980979 Constr confl = propagate();
811  450980979 assert trail.size() == qhead;
812   
813  450980979 if (confl == null) {
814    // No conflict found
815    // simpliFYDB() prevents a correct use of
816    // constraints removal.
817    // if (decisionLevel() == 0) {
818    // // Simplify the set of problem clause
819    // // iff rootLevel==0
820    // stats.rootSimplifications++;
821    // boolean ret = simplifyDB();
822    // assert ret;
823    // }
824    // was learnts.size() - nAssigns() > nofLearnts
825    // if (nofLearnts.obj >= 0 && learnts.size() > nofLearnts.obj) {
826  266980548 assert nAssigns() <= voc.realnVars();
827  266980548 if (nAssigns() == voc.realnVars()) {
828  1267 slistener.solutionFound();
829  1267 modelFound();
830  1267 return Lbool.TRUE;
831    }
832  266979281 if (conflictC >= nofConflicts) {
833    // Reached bound on number of conflicts
834    // Force a restart
835  26534 cancelUntil(rootLevel);
836  26534 return Lbool.UNDEFINED;
837    }
838  266952747 if (needToReduceDB) {
839  3 reduceDB();
840  3 needToReduceDB = false;
841    // Runtime.getRuntime().gc();
842    }
843    // New variable decision
844  266952747 stats.decisions++;
845  266952747 int p = order.select();
846  266952747 assert p > 1;
847  266952747 slistener.assuming(decode2dimacs(p));
848  266952747 boolean ret = assume(p);
849  266952747 assert ret;
850    } else {
851    // un conflit apparait
852  184000431 stats.conflicts++;
853  184000431 conflictC++;
854  184000431 slistener.conflictFound();
855  184000431 freeMem.newConflict();
856  184000431 if (decisionLevel() == rootLevel) {
857    // on est a la racine, la formule est inconsistante
858  955 return Lbool.FALSE;
859    }
860    // analyse la cause du conflit
861  183999476 assert confl != null;
862  183999476 int backtrackLevel = analyze(confl, learntConstraint);
863  183999476 assert backtrackLevel < decisionLevel();
864  183999476 cancelUntil(Math.max(backtrackLevel, rootLevel));
865  183999476 assert (decisionLevel() >= rootLevel)
866    && (decisionLevel() >= backtrackLevel);
867  183999476 if (learntConstraint.obj == null) {
868  126 return Lbool.FALSE;
869    }
870  183999350 record(learntConstraint.obj);
871  183999350 learntConstraint.obj = null;
872  183999350 decayActivities();
873    }
874  450952097 } while (undertimeout);
875  111 return Lbool.UNDEFINED; // timeout occured
876    }
877   
878    /**
879    *
880    */
 
881  1267 toggle void modelFound() {
882  1267 model = new int[trail.size()];
883  1267 fullmodel = new boolean[nVars()];
884  1267 int index = 0;
885  494273 for (int i = 1; i <= voc.nVars(); i++) {
886  493006 if (voc.belongsToPool(i)) {
887  493000 int p = voc.getFromPool(i);
888  493000 if (!voc.isUnassigned(p)) {
889  493000 model[index++] = voc.isSatisfied(p) ? i : -i;
890  493000 fullmodel[i - 1] = voc.isSatisfied(p);
891    }
892    }
893    }
894  1267 assert index == model.length;
895  1267 cancelUntil(rootLevel);
896    }
897   
 
898  0 toggle public boolean model(int var) {
899  0 if (var <= 0 || var > nVars()) {
900  0 throw new IllegalArgumentException(
901    "Use a valid Dimacs var id as argument!"); //$NON-NLS-1$
902    }
903  0 if (fullmodel == null) {
904  0 throw new UnsupportedOperationException(
905    "Call the solve method first!!!"); //$NON-NLS-1$
906    }
907  0 return fullmodel[var - 1];
908    }
909   
910    /**
911    *
912    */
 
913  3 toggle protected void reduceDB() {
914  3 reduceDB(claInc / learnts.size());
915    }
916   
 
917  4 toggle public void clearLearntClauses() {
918  4 for (Constr c : learnts)
919  0 c.remove();
920  4 learnts.clear();
921    }
922   
 
923  3 toggle protected void reduceDB(double lim) {
924  3 int i, j;
925  3 sortOnActivity();
926  3 stats.reduceddb++;
927  30262 for (i = j = 0; i < learnts.size() / 2; i++) {
928  30259 Constr c = learnts.get(i);
929  30259 if (c.locked()) {
930  13 learnts.set(j++, learnts.get(i));
931    } else {
932  30246 c.remove();
933    }
934    }
935  30263 for (; i < learnts.size(); i++) {
936    // Constr c = learnts.get(i);
937    // if (!c.locked() && (c.getActivity() < lim)) {
938    // c.remove();
939    // } else {
940  30260 learnts.set(j++, learnts.get(i));
941    // }
942    }
943  3 System.out.println("c cleaning " + (learnts.size() - j) //$NON-NLS-1$
944    + " clauses out of " + learnts.size() + " for limit " + lim); //$NON-NLS-1$ //$NON-NLS-2$
945  3 learnts.shrinkTo(j);
946    }
947   
948    /**
949    * @param learnts
950    */
 
951  3 toggle private void sortOnActivity() {
952  3 learnts.sort(comparator);
953    }
954   
955    /**
956    *
957    */
 
958  183999350 toggle protected void decayActivities() {
959  183999350 order.varDecayActivity();
960  183999350 claDecayActivity();
961    }
962   
963    /**
964    *
965    */
 
966  183999350 toggle private void claDecayActivity() {
967  183999350 claInc *= claDecay;
968    }
969   
970    /**
971    * @return true iff the set of constraints is satisfiable, else false.
972    */
 
973  2446 toggle public boolean isSatisfiable() throws TimeoutException {
974  2446 return isSatisfiable(VecInt.EMPTY);
975    }
976   
977    private double timebegin = 0;
978   
979    private boolean needToReduceDB;
980   
981    private ConflictTimer freeMem;
982   
 
983  2462 toggle public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
984  2462 Lbool status = Lbool.UNDEFINED;
985   
986  2462 order.init();
987  2462 learner.init();
988  2462 restarter.init(params);
989  2462 timebegin = System.currentTimeMillis();
990  2462 slistener.start();
991  2462 model = null; // forget about previous model
992  2462 fullmodel = null;
993   
994    // propagate constraints
995  2462 if (propagate() != null) {
996  0 slistener.end(Lbool.FALSE);
997  0 cancelUntil(0);
998  0 return false;
999    }
1000   
1001    // push incremental assumptions
1002  2462 for (int q : assumps) {
1003  20 if (!assume(voc.getFromPool(q)) || (propagate() != null)) {
1004  3 slistener.end(Lbool.FALSE);
1005  3 cancelUntil(0);
1006  3 return false;
1007    }
1008    }
1009  2459 rootLevel = decisionLevel();
1010   
1011  2459 TimerTask stopMe = new TimerTask() {
 
1012  111 toggle @Override
1013    public void run() {
1014  111 undertimeout = false;
1015    }
1016    };
1017  2459 undertimeout = true;
1018  2459 Timer timer = new Timer(true);
1019  2459 timer.schedule(stopMe, timeout);
1020  2459 needToReduceDB = false;
1021   
1022  2459 final long memorybound = Runtime.getRuntime().freeMemory() / 10;
1023  2459 freeMem = new ConflictTimer(500) {
1024    private static final long serialVersionUID = 1L;
 
1025  367750 toggle @Override
1026    void run() {
1027  367750 long freemem = Runtime.getRuntime().freeMemory();
1028    // System.out.println("c Free memory "+freemem);
1029  367750 if (freemem < memorybound) {
1030    // Reduce the set of learnt clauses
1031  3 needToReduceDB = true;
1032    }
1033    }
1034    };
1035    // Solve
1036  31452 while ((status == Lbool.UNDEFINED) && undertimeout) {
1037  28993 status = search(restarter.nextRestartNumberOfConflict());
1038  28993 System.out.println("c speed "+(stats.decisions/((System.currentTimeMillis()-timebegin)/1000))+" dec/s, "+stats.starts+"/"+stats.conflicts);
1039  28993 restarter.onRestart();
1040    }
1041   
1042  2459 cancelUntil(0);
1043  2459 timer.cancel();
1044  2459 slistener.end(status);
1045  2459 if (!undertimeout) {
1046  111 throw new TimeoutException(" Timeout (" + timeout + "s) exceeded"); //$NON-NLS-1$//$NON-NLS-2$
1047    }
1048  2348 return status == Lbool.TRUE;
1049    }
1050   
 
1051  0 toggle public SolverStats getStats() {
1052  0 return stats;
1053    }
1054   
 
1055  204 toggle public IOrder<L> getOrder() {
1056  204 return order;
1057    }
1058   
 
1059  4 toggle public void setOrder(IOrder<L> h) {
1060  4 order = h;
1061  4 order.setLits(voc);
1062    }
1063   
 
1064  1140 toggle public L getVocabulary() {
1065  1140 return voc;
1066    }
1067   
 
1068  5008 toggle public void reset() {
1069    // FIXME verify that cleanup is OK
1070  5008 voc.resetPool();
1071  5008 dsfactory.reset();
1072  5008 constrs.clear();
1073  5008 learnts.clear();
1074  5008 stats.reset();
1075    }
1076   
 
1077  1319 toggle public int nVars() {
1078  1319 return voc.nVars();
1079    }
1080   
1081    /**
1082    * @param constr
1083    * a constraint implementing the Constr interface.
1084    * @return a reference to the constraint for external use.
1085    */
 
1086  5693058 toggle protected IConstr addConstr(Constr constr) {
1087  5693058 if (constr != null) {
1088  5092579 constrs.push(constr);
1089    }
1090  5693058 return constr;
1091    }
1092   
 
1093  2412 toggle public DataStructureFactory<L> getDSFactory() {
1094  2412 return dsfactory;
1095    }
1096   
 
1097  0 toggle public IVecInt getOutLearnt() {
1098  0 return outLearnt;
1099    }
1100   
1101    /**
1102    * returns the ith constraint in the solver.
1103    *
1104    * @param i
1105    * the constraint number (begins at 0)
1106    * @return the ith constraint
1107    */
 
1108  1 toggle public IConstr getIthConstr(int i) {
1109  1 return constrs.get(i);
1110    }
1111   
1112    /*
1113    * (non-Javadoc)
1114    *
1115    * @see org.sat4j.specs.ISolver#printStat(java.io.PrintStream,
1116    * java.lang.String)
1117    */
 
1118  0 toggle public void printStat(PrintStream out, String prefix) {
1119  0 printStat(new PrintWriter(out), prefix);
1120    }
1121   
 
1122  0 toggle public void printStat(PrintWriter out, String prefix) {
1123  0 stats.printStat(out, prefix);
1124  0 double cputime = (System.currentTimeMillis() - timebegin) / 1000;
1125  0 out.println(prefix + "speed (decisions/second)\t: " + stats.decisions //$NON-NLS-1$
1126    / cputime);
1127  0 order.printStat(out, prefix);
1128    }
1129   
1130    /*
1131    * (non-Javadoc)
1132    *
1133    * @see java.lang.Object#toString()
1134    */
 
1135  0 toggle public String toString(String prefix) {
1136  0 StringBuilder stb = new StringBuilder();
1137  0 Object[] objs = { analyzer, dsfactory, learner, params, order,
1138    simplifier, restarter };
1139    // stb.append(prefix);
1140  0 stb.append("--- Begin Solver configuration ---"); //$NON-NLS-1$
1141  0 stb.append("\n"); //$NON-NLS-1$
1142  0 for (Object o : objs) {
1143  0 stb.append(prefix);
1144  0 stb.append(o.toString());
1145  0 stb.append("\n"); //$NON-NLS-1$
1146    }
1147  0 stb.append(prefix);
1148  0 stb.append("--- End Solver configuration ---"); //$NON-NLS-1$
1149  0 return stb.toString();
1150    }
1151   
1152    /*
1153    * (non-Javadoc)
1154    *
1155    * @see java.lang.Object#toString()
1156    */
 
1157  0 toggle @Override
1158    public String toString() {
1159  0 return toString(""); //$NON-NLS-1$
1160    }
1161   
 
1162  0 toggle public int getTimeout() {
1163  0 return (int)(timeout/1000);
1164    }
1165   
 
1166  1672 toggle public void setExpectedNumberOfClauses(int nb) {
1167  1672 constrs.ensure(nb);
1168    }
1169   
 
1170  0 toggle public Map<String, Number> getStat() {
1171  0 return stats.toMap();
1172    }
1173   
 
1174  0 toggle public int[] findModel() throws TimeoutException {
1175  0 if (isSatisfiable()) {
1176  0 return model();
1177    }
1178  0 return null;
1179    }
1180   
 
1181  0 toggle public int[] findModel(IVecInt assumps) throws TimeoutException {
1182  0 if (isSatisfiable(assumps)) {
1183  0 return model();
1184    }
1185  0 return null;
1186    }
1187   
1188    }
1189   
 
1190    class ActivityComparator implements Comparator<Constr>, Serializable {
1191   
1192    private static final long serialVersionUID = 1L;
1193   
1194    /*
1195    * (non-Javadoc)
1196    *
1197    * @see java.util.Comparator#compare(java.lang.Object, java.lang.Object)
1198    */
 
1199  1253454 toggle public int compare(Constr c1, Constr c2) {
1200  1253454 return (int) Math.round(c1.getActivity() - c2.getActivity());
1201    }
1202    }
1203   
 
1204    abstract class ConflictTimer implements Serializable {
1205   
1206    private int counter;
1207    private final int bound;
1208   
 
1209  2459 toggle ConflictTimer(final int bound) {
1210  2459 this.bound = bound;
1211  2459 counter = 0;
1212    }
1213   
 
1214  0 toggle void reset() {
1215  0 counter = 0;
1216    }
1217   
 
1218  184000431 toggle void newConflict() {
1219  184000431 counter++;
1220  184000431 if (counter==bound) {
1221  367750 run();
1222  367750 counter = 0;
1223    }
1224    }
1225   
1226    abstract void run();
1227    }
 
CloverReport generated by Clover Code Coverage v2.0a5
mer. juin 27 2007 07:27:33 CEST.		   Beta Testers License registered to clover-support@cenqua.com. This license of Clover2 is provided for beta testing only. You have 5 day(s) before your Beta Tester License expires.