Clover coverage report -
Coverage timestamp: jeu. juin 15 2006 08:24:33 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 1 064   Methods: 71
NCLOC: 650   Classes: 3
 
 Source file Conditionals Statements Methods TOTAL
Solver.java 87% 86,4% 80,3% 85,7%
coverage coverage
 1    /*
 2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004 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 java.io.PrintStream;
 29    import java.io.PrintWriter;
 30    import java.io.Serializable;
 31    import java.math.BigInteger;
 32    import java.util.Comparator;
 33    import java.util.Map;
 34    import java.util.Timer;
 35    import java.util.TimerTask;
 36   
 37    import org.sat4j.core.Vec;
 38    import org.sat4j.core.VecInt;
 39    import org.sat4j.specs.ContradictionException;
 40    import org.sat4j.specs.IConstr;
 41    import org.sat4j.specs.ISolver;
 42    import org.sat4j.specs.IVec;
 43    import org.sat4j.specs.IVecInt;
 44    import org.sat4j.specs.TimeoutException;
 45   
 46    /**
 47    * @author leberre
 48    */
 49    public class Solver implements ISolver, UnitPropagationListener,
 50    ActivityListener, Learner, Serializable {
 51   
 52    private static final long serialVersionUID = 1L;
 53   
 54    private static final double CLAUSE_RESCALE_FACTOR = 1e-20;
 55   
 56    private static final double CLAUSE_RESCALE_BOUND = 1 / CLAUSE_RESCALE_FACTOR;
 57   
 58    /**
 59    * List des contraintes du probl?me.
 60    */
 61    private final IVec<Constr> constrs = new Vec<Constr>(); // Constr
 62   
 63    // vector
 64   
 65    /**
 66    * Liste des clauses apprises.
 67    */
 68    private final IVec<Constr> learnts = new Vec<Constr>(); // Clause
 69   
 70    // vector
 71   
 72    /**
 73    * incr?ment pour l'activit? des clauses.
 74    */
 75    private double claInc = 1.0;
 76   
 77    /**
 78    * decay factor pour l'activit? des clauses.
 79    */
 80    private double claDecay = 1.0;
 81   
 82    /**
 83    * Queue de propagation
 84    */
 85    // private final IntQueue propQ = new IntQueue(); // Lit
 86    // head of the queue in trail ... (taken from MiniSAT 1.14)
 87    private int qhead = 0;
 88   
 89    // queue
 90   
 91    /**
 92    * affectation en ordre chronologique
 93    */
 94    protected final IVecInt trail = new VecInt(); // lit
 95   
 96    // vector
 97   
 98    /**
 99    * indice des s?parateurs des diff?rents niveau de d?cision dans trail
 100    */
 101    protected final IVecInt trailLim = new VecInt(); // int
 102   
 103    // vector
 104   
 105    /**
 106    * S?pare les hypoth?ses incr?mentale et recherche
 107    */
 108    protected int rootLevel;
 109   
 110    private int[] model = null;
 111   
 112    protected ILits voc;
 113   
 114    private IOrder order;
 115   
 116    private final Comparator<Constr> comparator = new ActivityComparator();
 117   
 118    private final SolverStats stats = new SolverStats();
 119   
 120    private final LearningStrategy learner;
 121   
 122    protected final AssertingClauseGenerator analyzer;
 123   
 124    private boolean undertimeout;
 125   
 126    private int timeout = Integer.MAX_VALUE;
 127   
 128    protected DataStructureFactory dsfactory;
 129   
 130    private final SearchParams params;
 131   
 132    private final IVecInt __dimacs_out = new VecInt();
 133   
 134    private SearchListener slistener = new NullSearchListener();
 135   
 136  5686082 protected IVecInt dimacs2internal(IVecInt in) {
 137  5686082 if (voc.nVars() == 0) {
 138  0 throw new RuntimeException(
 139    "Please set the number of variables (solver.newVar() or solver.newVar(maxvar)) before adding constraints!");
 140    }
 141  5686082 __dimacs_out.clear();
 142  5686082 __dimacs_out.ensure(in.size());
 143  5686082 for (int i = 0; i < in.size(); i++) {
 144    assert (in.get(i) != 0) && (Math.abs(in.get(i)) <= voc.nVars());
 145  24248988 __dimacs_out.unsafePush(voc.getFromPool(in.get(i)));
 146    }
 147  5686082 return __dimacs_out;
 148    }
 149   
 150    /**
 151    * creates a Solver without LearningListener. A learningListener must be
 152    * added to the solver, else it won't backtrack!!! A data structure factory
 153    * must be provided, else it won't work either.
 154    *
 155    * @param acg
 156    * an asserting clause generator
 157    */
 158   
 159  1703 public Solver(AssertingClauseGenerator acg, LearningStrategy learner,
 160    DataStructureFactory dsf, IOrder order) {
 161  1703 this(acg, learner, dsf, new SearchParams(), order);
 162    }
 163   
 164  2506 public Solver(AssertingClauseGenerator acg, LearningStrategy learner,
 165    DataStructureFactory dsf, SearchParams params, IOrder order) {
 166  2506 analyzer = acg;
 167  2506 this.learner = learner;
 168  2506 this.order = order;
 169  2506 this.params = params;
 170  2506 setDataStructureFactory(dsf);
 171    }
 172   
 173    /**
 174    * Change the internatal representation of the contraints.
 175    *
 176    * Note that the heuristics must be changed prior to calling that method.
 177    *
 178    * @param dsf the internal factory
 179    */
 180  2506 public void setDataStructureFactory(DataStructureFactory dsf) {
 181  2506 dsfactory = dsf;
 182  2506 dsfactory.setUnitPropagationListener(this);
 183  2506 dsfactory.setLearner(this);
 184  2506 voc = dsf.getVocabulary();
 185  2506 order.setLits(voc);
 186    }
 187   
 188  0 public void setSearchListener(SearchListener sl) {
 189  0 slistener = sl;
 190    }
 191   
 192  2375 public void setTimeout(int t) {
 193  2375 timeout = t;
 194    }
 195   
 196  452570238 protected int nAssigns() {
 197  452570238 return trail.size();
 198    }
 199   
 200  2427 public int nConstraints() {
 201  2427 return constrs.size();
 202    }
 203   
 204  3685182 public void learn(Constr c) {
 205    // slistener.learn(c);
 206  3685182 learnts.push(c);
 207  3685181 c.setLearnt();
 208  3685181 c.register();
 209  3685181 stats.learnedclauses++;
 210  3685181 switch (c.size()) {
 211  3554 case 2:
 212  3554 stats.learnedbinaryclauses++;
 213  3554 break;
 214  4183 case 3:
 215  4183 stats.learnedternaryclauses++;
 216  4183 break;
 217  3677444 default:
 218    ; // do nothing
 219    }
 220    }
 221   
 222  1230076436 public int decisionLevel() {
 223  1230076436 return trailLim.size();
 224    }
 225   
 226  666634 public int newVar() {
 227  666634 int index = voc.nVars() + 1;
 228  666634 voc.ensurePool(index);
 229  666618 seen = new boolean[index + 1];
 230  666618 trail.ensure(index);
 231  666617 trailLim.ensure(index);
 232  666615 order.newVar();
 233  666615 return index;
 234    }
 235   
 236  1677 public int newVar(int howmany) {
 237  1677 voc.ensurePool(howmany);
 238  1677 order.newVar(howmany);
 239  1677 seen = new boolean[howmany + 1];
 240  1677 trail.ensure(howmany);
 241  1677 trailLim.ensure(howmany);
 242  1677 return voc.nVars();
 243    }
 244   
 245  4007801 public IConstr addClause(IVecInt literals) throws ContradictionException {
 246  4007801 IVecInt vlits = dimacs2internal(literals);
 247  4007801 return addConstr(dsfactory.createClause(vlits));
 248    }
 249   
 250  4 public boolean removeConstr(IConstr co) {
 251  4 if (co == null) {
 252  0 throw new UnsupportedOperationException(
 253    "Reference to the constraint to remove needed!"); //$NON-NLS-1$
 254    }
 255  4 Constr c = (Constr) co;
 256  4 c.remove();
 257  4 constrs.remove(c);
 258  4 clearLearntClauses();
 259  4 cancelLearntLiterals();
 260  4 return true;
 261    }
 262   
 263  1678268 public IConstr addPseudoBoolean(IVecInt literals, IVec<BigInteger> coeffs,
 264    boolean moreThan, BigInteger degree) throws ContradictionException {
 265  1678268 IVecInt vlits = dimacs2internal(literals);
 266    assert vlits.size() == literals.size();
 267    assert literals.size() == coeffs.size();
 268  1678268 return addConstr(dsfactory.createPseudoBooleanConstraint(vlits, coeffs,
 269    moreThan, degree));
 270    }
 271   
 272  0 public void addAllClauses(IVec<IVecInt> clauses)
 273    throws ContradictionException {
 274  0 for (IVecInt clause : clauses) {
 275  0 addClause(clause);
 276    }
 277    }
 278   
 279  13 public IConstr addAtMost(IVecInt literals, int degree)
 280    throws ContradictionException {
 281  13 int n = literals.size();
 282  13 IVecInt opliterals = new VecInt(n);
 283  13 for (int p : literals) {
 284  39 opliterals.push(-p);
 285    }
 286  13 return addAtLeast(opliterals, n - degree);
 287    }
 288   
 289  13 public IConstr addAtLeast(IVecInt literals, int degree)
 290    throws ContradictionException {
 291  13 IVecInt vlits = dimacs2internal(literals);
 292  13 return addConstr(dsfactory.createCardinalityConstraint(vlits, degree));
 293    }
 294   
 295  0 @SuppressWarnings("unchecked")
 296    public boolean simplifyDB() {
 297    // aucune raison de recommencer un propagate?
 298    // if (propagate() != null) {
 299    // // Un conflit est d?couvert, la base est inconsistante
 300    // return false;
 301    // }
 302   
 303    // Simplifie la base de clauses apres la premiere propagation des
 304    // clauses unitaires
 305  0 IVec<Constr>[] cs = new IVec[] { constrs, learnts };
 306  0 for (int type = 0; type < 2; type++) {
 307  0 int j = 0;
 308  0 for (int i = 0; i < cs[type].size(); i++) {
 309  0 if (cs[type].get(i).simplify()) {
 310    // enleve les contraintes satisfaites de la base
 311  0 cs[type].get(i).remove();
 312    } else {
 313  0 cs[type].moveTo(j++, i);
 314    }
 315    }
 316  0 cs[type].shrinkTo(j);
 317    }
 318  0 return true;
 319    }
 320   
 321    /**
 322    * Si un mod?le est trouv?, ce vecteur contient le mod?le.
 323    *
 324    * @return un mod?le de la formule.
 325    */
 326  43 public int[] model() {
 327  43 if (model == null) {
 328  2 throw new UnsupportedOperationException(
 329    "Call the solve method first!!!"); //$NON-NLS-1$
 330    }
 331  41 int[] nmodel = new int[model.length];
 332  41 System.arraycopy(model, 0, nmodel, 0, model.length);
 333  41 return nmodel;
 334    }
 335   
 336    /**
 337    * Satisfait un litt?ral
 338    *
 339    * @param p
 340    * le litt?ral
 341    * @return true si tout se passe bien, false si un conflit appara?t.
 342    */
 343  226281838 public boolean enqueue(int p) {
 344  226281838 return enqueue(p, null);
 345    }
 346   
 347    /**
 348    * Put the literal on the queue of assignments to be done.
 349    *
 350    * @param p
 351    * the literal.
 352    * @param from
 353    * the reason to propagate that literal, else null
 354    * @return true if the asignment can be made, false if a conflict is
 355    * detected.
 356    */
 357    public boolean enqueue(int p, Constr from) {
 358    assert p > 1;
 359    if (voc.isSatisfied(p)) {
 360    // literal is already satisfied. Skipping.
 361    return true;
 362    }
 363    if (voc.isFalsified(p)) {
 364    // conflicting enqueued assignment
 365  97364091 return false;
 366    }
 367    // new fact, store it
 368    voc.satisfies(p);
 369    voc.setLevel(p, decisionLevel());
 370    voc.setReason(p, from);
 371    trail.push(p);
 372    return true;
 373    }
 374   
 375    private boolean[] seen = new boolean[0];
 376   
 377    private final IVecInt preason = new VecInt();
 378   
 379    private final IVecInt outLearnt = new VecInt();
 380   
 381  139271668 public int analyze(Constr confl, Handle<Constr> outLearntRef) {
 382    assert confl != null;
 383  139271668 outLearnt.clear();
 384   
 385    assert outLearnt.size() == 0;
 386  139271668 for (int i = 0; i < seen.length; i++) {
 387  161161446 seen[i] = false;
 388    }
 389   
 390  139271668 analyzer.initAnalyze();
 391  139271668 int p = ILits.UNDEFINED;
 392   
 393  139271668 outLearnt.push(ILits.UNDEFINED);
 394    // reserve de la place pour le litteral falsifie
 395  139271668 int outBtlevel = 0;
 396   
 397  139271668 do {
 398  1405902673 preason.clear();
 399    assert confl != null;
 400  1405902673 confl.calcReason(p, preason);
 401  1405902673 if (confl.learnt())
 402  131631491 claBumpActivity(confl);
 403    // Trace reason for p
 404  1405902673 for (int j = 0; j < preason.size(); j++) {
 405  34029768 int q = preason.get(j);
 406  34029768 order.updateVar(q);
 407  34029768 if (!seen[q >> 1]) {
 408    // order.updateVar(q); // MINISAT
 409  862186952 seen[q >> 1] = true;
 410  862186952 if (voc.getLevel(q) == decisionLevel()) {
 411  1405902673 analyzer.onCurrentDecisionLevelLiteral(q);
 412    } else if (voc.getLevel(q) > 0) {
 413    // ajoute les variables depuis le niveau de d?cision 0
 414    outLearnt.push(q ^ 1);
 415    outBtlevel = Math.max(outBtlevel, voc.getLevel(q));
 416    }
 417    }
 418    }
 419   
 420    // select next reason to look at
 421  1405902673 do {
 422    p = trail.last();
 423    // System.err.print((Clause.lastid()+1)+"
 424    // "+((Clause)confl).getId()+" ");
 425    confl = voc.getReason(p);
 426    // System.err.println(((Clause)confl).getId());
 427    // assert(confl != null) || counter == 1;
 428    undoOne();
 429    } while (!seen[p >> 1]);
 430    // seen[p.var] indique que p se trouve dans outLearnt ou dans
 431    // le dernier niveau de d?cision
 432  1405902673 } while (analyzer.clauseNonAssertive(confl));
 433   
 434  139271668 outLearnt.set(0, p ^ 1);
 435  139271668 simplifier.simplify(outLearnt);
 436   
 437  139271668 Constr c = dsfactory.createUnregisteredClause(outLearnt);
 438  139271665 slistener.learn(c);
 439   
 440  139271665 outLearntRef.obj = c;
 441   
 442    assert outBtlevel > -1;
 443  139271665 return outBtlevel;
 444    }
 445   
 446    interface ISimplifier extends Serializable {
 447    void simplify(IVecInt outLearnt);
 448    }
 449   
 450    public static final ISimplifier NO_SIMPLIFICATION = new ISimplifier() {
 451    /**
 452    *
 453    */
 454    private static final long serialVersionUID = 1L;
 455   
 456  118535977 public void simplify(IVecInt outLearnt) {
 457    }
 458   
 459  0 @Override
 460    public String toString() {
 461  0 return "No reason simplification"; //$NON-NLS-1$
 462    }
 463    };
 464   
 465    public final ISimplifier SIMPLE_SIMPLIFICATION = new ISimplifier() {
 466    /**
 467    *
 468    */
 469    private static final long serialVersionUID = 1L;
 470   
 471  20735691 public void simplify(IVecInt outLearnt) {
 472  20735691 simpleSimplification(outLearnt);
 473    }
 474   
 475  0 @Override
 476    public String toString() {
 477  0 return "Simple reason simplification"; //$NON-NLS-1$
 478    }
 479    };
 480   
 481   
 482    private ISimplifier simplifier = NO_SIMPLIFICATION;
 483   
 484  7 public void setSimplifier(ISimplifier simp) {
 485  7 simplifier = simp;
 486    }
 487   
 488    // Taken from MiniSAT 1.14: Simplify conflict clause (a little):
 489  20735691 private void simpleSimplification(IVecInt outLearnt) {
 490  20735691 int i, j;
 491   
 492  20735691 for (i = j = 1; i < outLearnt.size(); i++) {
 493  461530896 IConstr r = voc.getReason(outLearnt.get(i));
 494  461530896 if (r == null) {
 495  162354196 outLearnt.moveTo(j++, i);
 496    } else {
 497  299176700 for (int k = 1; k < r.size(); k++)
 498  611466438 if (!seen[r.get(k) >> 1] && (voc.getLevel(r.get(k)) != 0)) {
 499  294682666 outLearnt.moveTo(j++, i);
 500  294682666 break;
 501    }
 502    }
 503    }
 504  20735691 outLearnt.shrink(i - j);
 505  20735691 stats.reducedliterals += (i - j);
 506    }
 507   
 508    /**
 509    * decode the internal representation of a literal into Dimacs format.
 510    *
 511    * @param p
 512    * the literal in internal representation
 513    * @return the literal in dimacs representation
 514    */
 515    public static int decode2dimacs(int p) {
 516    return ((p & 1) == 0 ? 1 : -1) * (p >> 1);
 517    }
 518   
 519    /**
 520    *
 521    */
 522    protected void undoOne() {
 523    // recupere le dernier litteral affecte
 524    int p = trail.last();
 525    assert p > 1;
 526    assert voc.getLevel(p) >= 0;
 527    int x = p >> 1;
 528    // desaffecte la variable
 529    voc.unassign(p);
 530    voc.setReason(p, null);
 531    voc.setLevel(p, -1);
 532    // met a jour l'heuristique
 533    order.undo(x);
 534    // depile le litteral des affectations
 535    trail.pop();
 536    // met a jour les contraintes apres desaffectation du litteral :
 537    // normalement, il n'y a rien a faire ici pour les prouveurs de type
 538    // Chaff??
 539    IVec<Undoable> undos = voc.undos(p);
 540    assert undos != null;
 541  1818595279 while (undos.size() > 0) {
 542    undos.last().undo(p);
 543    undos.pop();
 544    }
 545    }
 546   
 547    /**
 548    * Propagate activity to a constraint
 549    *
 550    * @param confl
 551    * a constraint
 552    */
 553  131631491 public void claBumpActivity(Constr confl) {
 554  131631491 confl.incActivity(claInc);
 555  131631491 if (confl.getActivity() > CLAUSE_RESCALE_BOUND)
 556  2967 claRescalActivity();
 557    // for (int i = 0; i < confl.size(); i++) {
 558    // varBumpActivity(confl.get(i));
 559    // }
 560    }
 561   
 562    public void varBumpActivity(int p) {
 563    order.updateVar(p);
 564    }
 565   
 566  2967 private void claRescalActivity() {
 567  2967 for (int i = 0; i < learnts.size(); i++) {
 568  1444529 learnts.get(i).rescaleBy(CLAUSE_RESCALE_FACTOR);
 569    }
 570  2967 claInc *= CLAUSE_RESCALE_FACTOR;
 571    }
 572   
 573    /**
 574    * @return null if not conflict is found, else a conflicting constraint.
 575    */
 576  366079328 public Constr propagate() {
 577  366079328 while (qhead < trail.size()) {
 578    stats.propagations++;
 579    int p = trail.get(qhead++);
 580    slistener.propagating(decode2dimacs(p));
 581    // p is the literal to propagate
 582    // Moved original MiniSAT code to dsfactory to avoid
 583    // watches manipulation in counter Based clauses for instance.
 584    assert p > 1;
 585    IVec<Propagatable> constrs = dsfactory.getWatchesFor(p);
 586   
 587    for (int i = 0; i < constrs.size(); i++) {
 588  212656638 stats.inspects++;
 589  212656638 if (!constrs.get(i).propagate(this, p)) {
 590    // Constraint is conflicting: copy remaining watches to
 591    // watches[p]
 592    // and return constraint
 593  139791756 dsfactory.conflictDetectedInWatchesFor(p, i);
 594  139791756 qhead = trail.size(); // propQ.clear();
 595    // FIXME enlever le transtypage
 596  139791756 return (Constr) constrs.get(i);
 597    }
 598    }
 599    }
 600  226287571 return null;
 601    }
 602   
 603  139790674 void record(Constr constr) {
 604  139790674 constr.setLearnt();
 605  139790674 constr.assertConstraint(this);
 606  139790674 slistener.adding(decode2dimacs(constr.get(0)));
 607  139790674 if (constr.size() == 1) {
 608  4429 stats.learnedliterals++;
 609    } else {
 610  139786245 learner.learns(constr);
 611    }
 612    }
 613   
 614    /**
 615    * @return false ssi conflit imm?diat.
 616    */
 617  226281197 public boolean assume(int p) {
 618    // Precondition: assume propagation queue is empty
 619    assert trail.size() == qhead;
 620  226281197 trailLim.push(trail.size());
 621  226281197 return enqueue(p);
 622    }
 623   
 624    /**
 625    * Revert to the state before the last push()
 626    */
 627  226158886 private void cancel() {
 628    // assert trail.size() == qhead || !undertimeout;
 629  226158886 int decisionvar = trail.unsafeGet(trailLim.last());
 630  226158886 slistener.backtracking(decode2dimacs(decisionvar));
 631  226158886 for (int c = trail.size() - trailLim.last(); c > 0; c--) {
 632  342418259 undoOne();
 633    }
 634  226158886 trailLim.pop();
 635    }
 636   
 637    /**
 638    * Restore literals
 639    */
 640  4 private void cancelLearntLiterals() {
 641    // assert trail.size() == qhead || !undertimeout;
 642   
 643  4 for (int c = trail.size() - rootLevel; c > 0; c--) {
 644  4 undoOne();
 645    }
 646  4 qhead = trail.size();
 647    }
 648   
 649    /**
 650    * Cancel several levels of assumptions
 651    *
 652    * @param level
 653    */
 654  139797172 protected void cancelUntil(int level) {
 655  139797172 while (decisionLevel() > level) {
 656  226158886 cancel();
 657    }
 658  139797172 qhead = trail.size();
 659    }
 660   
 661    private final Handle<Constr> learntConstraint = new Handle<Constr>();
 662   
 663    private boolean[] fullmodel;
 664   
 665  5124 Lbool search(long nofConflicts, Handle<Long> nofLearnts) {
 666    assert rootLevel == decisionLevel();
 667  5124 stats.starts++;
 668  5124 int conflictC = 0;
 669   
 670    // varDecay = 1 / params.varDecay;
 671  5124 order.setVarDecay(1 / params.getVarDecay());
 672  5124 claDecay = 1 / params.getClaDecay();
 673   
 674  5124 do {
 675  366076874 slistener.beginLoop();
 676    // propage les clauses unitaires
 677  366076874 Constr confl = propagate();
 678    assert trail.size() == qhead;
 679   
 680  366076873 if (confl == null) {
 681    // No conflict found
 682    // simpliFYDB() prevents a correct use of
 683    // constraints removal.
 684    // if (decisionLevel() == 0) {
 685    // // Simplify the set of problem clause
 686    // // iff rootLevel==0
 687    // stats.rootSimplifications++;
 688    // boolean ret = simplifyDB();
 689    // assert ret;
 690    // }
 691    // was learnts.size() - nAssigns() > nofLearnts
 692    // if (nofLearnts.obj >= 0 && learnts.size() > nofLearnts.obj) {
 693    assert nAssigns() <= voc.realnVars();
 694  226285119 if (nAssigns() == voc.realnVars()) {
 695  1250 slistener.solutionFound();
 696  1250 modelFound();
 697  1250 return Lbool.TRUE;
 698    }
 699  226283869 if (conflictC >= nofConflicts) {
 700    // Reached bound on number of conflicts
 701    // Force a restart
 702  2700 cancelUntil(rootLevel);
 703  2700 return Lbool.UNDEFINED;
 704    }
 705  226281169 if (needToReduceDB) {
 706  490 reduceDB();
 707  490 needToReduceDB = false;
 708    }
 709    // New variable decision
 710  226281169 stats.decisions++;
 711  226281169 int p = order.select();
 712    assert p > 1;
 713  226281169 slistener.assuming(decode2dimacs(p));
 714  226281169 boolean ret = assume(p);
 715    assert ret;
 716    } else {
 717    // un conflit apparait
 718  139791754 stats.conflicts++;
 719  139791754 conflictC++;
 720  139791754 slistener.conflictFound();
 721  139791754 if (decisionLevel() == rootLevel) {
 722    // on est a la racine, la formule est inconsistante
 723  951 return Lbool.FALSE;
 724    }
 725   
 726    // analyse la cause du conflit
 727    assert confl != null;
 728  139790803 int backtrackLevel = analyze(confl, learntConstraint);
 729    assert backtrackLevel < decisionLevel();
 730  139790800 cancelUntil(Math.max(backtrackLevel, rootLevel));
 731    assert (decisionLevel() >= rootLevel)
 732    && (decisionLevel() >= backtrackLevel);
 733  139790800 if (learntConstraint.obj == null) {
 734  126 return Lbool.FALSE;
 735    }
 736  139790674 record(learntConstraint.obj);
 737  139790673 learntConstraint.obj = null;
 738  139790673 decayActivities();
 739    }
 740  366071842 } while (undertimeout);
 741  92 return Lbool.UNDEFINED; // timeout occured
 742    }
 743   
 744    /**
 745    *
 746    */
 747  1250 void modelFound() {
 748  1250 model = new int[trail.size()];
 749  1250 fullmodel = new boolean[nVars()];
 750  1250 int index = 0;
 751  1250 for (int i = 1; i <= voc.nVars(); i++) {
 752  472643 if (voc.belongsToPool(i)) {
 753  472637 int p = voc.getFromPool(i);
 754  472637 if (!voc.isUnassigned(p)) {
 755  472637 model[index++] = voc.isSatisfied(p) ? i : -i;
 756  472637 fullmodel[i - 1] = voc.isSatisfied(p);
 757    }
 758    }
 759    }
 760    assert index == model.length;
 761  1250 cancelUntil(rootLevel);
 762    }
 763   
 764  0 public boolean model(int var) {
 765  0 if (var <= 0 || var > nVars()) {
 766  0 throw new IllegalArgumentException(
 767    "Use a valid Dimacs var id as argument!"); //$NON-NLS-1$
 768    }
 769  0 if (fullmodel == null) {
 770  0 throw new UnsupportedOperationException(
 771    "Call the solve method first!!!"); //$NON-NLS-1$
 772    }
 773  0 return fullmodel[var - 1];
 774    }
 775   
 776    /**
 777    *
 778    */
 779  490 protected void reduceDB() {
 780  490 reduceDB(claInc / learnts.size());
 781    }
 782   
 783  4 protected void clearLearntClauses() {
 784  4 reduceDB(Double.MAX_VALUE);
 785    }
 786   
 787  494 protected void reduceDB(double lim) {
 788  494 int i, j;
 789  494 sortOnActivity();
 790  494 stats.reduceddb++;
 791  494 for (i = j = 0; i < learnts.size() / 2; i++) {
 792  692708 Constr c = learnts.get(i);
 793  692708 if (c.locked()) {
 794  3058 learnts.set(j++, learnts.get(i));
 795    } else {
 796  689650 c.remove();
 797    }
 798    }
 799  494 for (; i < learnts.size(); i++) {
 800    // Constr c = learnts.get(i);
 801    // if (!c.locked() && (c.getActivity() < lim)) {
 802    // c.remove();
 803    // } else {
 804  692946 learnts.set(j++, learnts.get(i));
 805    // }
 806    }
 807  494 System.out.println("c cleaning " + (learnts.size() - j) //$NON-NLS-1$
 808    + " clauses out of " + learnts.size() + " for limit " + lim); //$NON-NLS-1$ //$NON-NLS-2$
 809  494 learnts.shrinkTo(j);
 810    }
 811   
 812    /**
 813    * @param learnts
 814    */
 815  494 private void sortOnActivity() {
 816  494 learnts.sort(comparator);
 817    }
 818   
 819    /**
 820    *
 821    */
 822  139790673 protected void decayActivities() {
 823  139790673 order.varDecayActivity();
 824  139790673 claDecayActivity();
 825    }
 826   
 827    /**
 828    *
 829    */
 830  139790673 private void claDecayActivity() {
 831  139790673 claInc *= claDecay;
 832    }
 833   
 834    /**
 835    * @return true iff the set of constraints is satisfiable, else false.
 836    */
 837  2411 public boolean isSatisfiable() throws TimeoutException {
 838  2411 return isSatisfiable(VecInt.EMPTY);
 839    }
 840   
 841    private double timebegin = 0;
 842   
 843    private boolean needToReduceDB;
 844   
 845  2427 public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
 846  2427 Lbool status = Lbool.UNDEFINED;
 847  2427 double nofConflicts = params.initConflictBound;
 848  2427 double nofLearnts = nConstraints()
 849    * params.initLearntBoundConstraintFactor;
 850    // nofLearnts = Math.min(nofLearnts,10000);
 851  2427 order.init();
 852  2427 learner.init();
 853  2427 timebegin = System.currentTimeMillis();
 854  2427 slistener.start();
 855  2427 model = null; // forget about previous model
 856  2427 fullmodel = null;
 857   
 858    // propagate constraints
 859  2427 if (propagate() != null) {
 860  0 slistener.end(Lbool.FALSE);
 861  0 cancelUntil(0);
 862  0 return false;
 863    }
 864   
 865    // push incremental assumptions
 866  2427 for (int q : assumps) {
 867  20 if (!assume(voc.getFromPool(q)) || (propagate() != null)) {
 868  3 slistener.end(Lbool.FALSE);
 869  3 cancelUntil(0);
 870  3 return false;
 871    }
 872    }
 873    // StringBuffer stb = new StringBuffer();
 874    // stb.append("%RESA ");
 875    // stb.append(nVars());
 876    // stb.append(" ");
 877    // stb.append(nConstraints());
 878    // while(stb.length()<255) {
 879    // stb.append(' ');
 880    // }
 881    // System.err.println(stb);
 882  2424 rootLevel = decisionLevel();
 883   
 884  2424 TimerTask stopMe = new TimerTask() {
 885  92 @Override
 886    public void run() {
 887  92 undertimeout = false;
 888    }
 889    };
 890  2424 undertimeout = true;
 891  2424 Timer timer = new Timer(true);
 892  2424 timer.schedule(stopMe, timeout * 1000L);
 893  2424 needToReduceDB = false;
 894   
 895  2424 TimerTask freeMem = new TimerTask() {
 896  5754 @Override
 897    public void run() {
 898  5754 long freemem = Runtime.getRuntime().freeMemory();
 899    // System.out.println("c Free memory "+freemem);
 900  5754 if (freemem < 5000000) {
 901    // Reduce the set of learnt clauses
 902  530 needToReduceDB = true;
 903    }
 904    }
 905    };
 906  2424 timer.schedule(freeMem, 30000L, 5000L);
 907   
 908  2424 Handle<Long> hnofLearnts = new Handle<Long>();
 909  2424 hnofLearnts.obj = Math.round(nofLearnts);
 910   
 911    // Solve
 912  2424 while ((status == Lbool.UNDEFINED) && undertimeout) {
 913  5124 status = search(Math.round(nofConflicts), hnofLearnts);
 914  5119 nofConflicts *= params.conflictBoundIncFactor;
 915    // order.mirror(stats.starts);
 916    }
 917   
 918  2419 cancelUntil(0);
 919  2419 timer.cancel();
 920  2419 if (!undertimeout) {
 921  92 throw new TimeoutException(" Timeout (" + timeout + "s) exceeded"); //$NON-NLS-1$//$NON-NLS-2$
 922    }
 923  2327 slistener.end(status);
 924  2327 return status == Lbool.TRUE;
 925    }
 926   
 927  0 public SolverStats getStats() {
 928  0 return stats;
 929    }
 930   
 931  102 public IOrder getOrder() {
 932  102 return order;
 933    }
 934   
 935  104 public void setOrder(IOrder h) {
 936  104 order = h;
 937  104 order.setLits(voc);
 938    }
 939   
 940  1137 public ILits getVocabulary() {
 941  1137 return voc;
 942    }
 943   
 944  2490 public void reset() {
 945    // FIXME verify that cleanup is OK
 946  2490 voc.resetPool();
 947  2490 dsfactory.reset();
 948  2490 constrs.clear();
 949  2490 learnts.clear();
 950  2490 stats.reset();
 951    }
 952   
 953  1302 public int nVars() {
 954  1302 return voc.nVars();
 955    }
 956   
 957    /**
 958    * @param constr
 959    * a constraint implementing the Constr interface.
 960    * @return a reference to the constraint for external use.
 961    */
 962  5685966 protected IConstr addConstr(Constr constr) {
 963  5685966 if (constr != null) {
 964  5085487 constrs.push(constr);
 965    }
 966  5685966 return constr;
 967    }
 968   
 969  2404 public DataStructureFactory getDSFactory() {
 970  2404 return dsfactory;
 971    }
 972   
 973  0 public IVecInt getOutLearnt() {
 974  0 return outLearnt;
 975    }
 976   
 977    /**
 978    * returns the ith constraint in the solver.
 979    *
 980    * @param i
 981    * the constraint number (begins at 0)
 982    * @return the ith constraint
 983    */
 984  1 public IConstr getIthConstr(int i) {
 985  1 return constrs.get(i);
 986    }
 987   
 988    /*
 989    * (non-Javadoc)
 990    *
 991    * @see org.sat4j.specs.ISolver#printStat(java.io.PrintStream,
 992    * java.lang.String)
 993    */
 994  0 public void printStat(PrintStream out, String prefix) {
 995  0 printStat(new PrintWriter(out), prefix);
 996    }
 997   
 998  0 public void printStat(PrintWriter out, String prefix) {
 999  0 stats.printStat(out, prefix);
 1000  0 double cputime = (System.currentTimeMillis() - timebegin) / 1000;
 1001  0 out.println(prefix + "speed (decisions/second)\t: " + stats.decisions //$NON-NLS-1$
 1002    / cputime);
 1003  0 order.printStat(out, prefix);
 1004    }
 1005   
 1006    /*
 1007    * (non-Javadoc)
 1008    *
 1009    * @see java.lang.Object#toString()
 1010    */
 1011  0 public String toString(String prefix) {
 1012  0 StringBuilder stb = new StringBuilder();
 1013  0 Object[] objs = { analyzer, dsfactory, learner, params, order,
 1014    simplifier };
 1015  0 stb.append(prefix);
 1016  0 stb.append("--- Begin Solver configuration ---"); //$NON-NLS-1$
 1017  0 stb.append("\n"); //$NON-NLS-1$
 1018  0 for (Object o : objs) {
 1019  0 stb.append(prefix);
 1020  0 stb.append(o.toString());
 1021  0 stb.append("\n"); //$NON-NLS-1$
 1022    }
 1023  0 stb.append(prefix);
 1024  0 stb.append("--- End Solver configuration ---"); //$NON-NLS-1$
 1025  0 return stb.toString();
 1026    }
 1027   
 1028    /*
 1029    * (non-Javadoc)
 1030    *
 1031    * @see java.lang.Object#toString()
 1032    */
 1033  0 @Override
 1034    public String toString() {
 1035  0 return toString(""); //$NON-NLS-1$
 1036    }
 1037   
 1038  0 public int getTimeout() {
 1039  0 return timeout;
 1040    }
 1041   
 1042  1663 public void setExpectedNumberOfClauses(int nb) {
 1043  1663 constrs.ensure(nb);
 1044    }
 1045   
 1046  0 public Map<String, Number> getStat() {
 1047  0 return stats.toMap();
 1048    }
 1049   
 1050    }
 1051   
 1052    class ActivityComparator implements Comparator<Constr>, Serializable {
 1053   
 1054    private static final long serialVersionUID = 1L;
 1055   
 1056    /*
 1057    * (non-Javadoc)
 1058    *
 1059    * @see java.util.Comparator#compare(java.lang.Object, java.lang.Object)
 1060    */
 1061  22355990 public int compare(Constr c1, Constr c2) {
 1062  22355990 return (int) Math.round(c1.getActivity() - c2.getActivity());
 1063    }
 1064    }
 
CloverReport generated by Clover Code Coverage v1.3.9
jeu. juin 15 2006 08:24:39 CEST.		   Open Source License registered to the OpenSAT Project. This license of Clover is provided to support the development of OpenSAT only.