backends/minisat/simp/SimpSolver.C

   1 /************************************************************************************[SimpSolver.C]
   2 MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
   3
   4 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
   5 associated documentation files (the "Software"), to deal in the Software without restriction,
   6 including without limitation the rights to use, copy, modify, merge, publish, distribute,
   7 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
   8 furnished to do so, subject to the following conditions:
   9
  10 The above copyright notice and this permission notice shall be included in all copies or
  11 substantial portions of the Software.
  12
  13 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
  14 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
  15 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
  16 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
  17 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
  18 **************************************************************************************************/
  19
  20 #include "Sort.h"
  21 #include "SimpSolver.h"
  22
  23
  24 //=================================================================================================
  25 // Constructor/Destructor:
  26
  27
  28 SimpSolver::SimpSolver() :
  29     grow               (0)
  30   , asymm_mode         (false)
  31   , redundancy_check   (false)
  32   , merges             (0)
  33   , asymm_lits         (0)
  34   , remembered_clauses (0)
  35   , elimorder          (1)
  36   , use_simplification (true)
  37   , elim_heap          (ElimLt(n_occ))
  38   , bwdsub_assigns     (0)
  39 {
  40     vec<Lit> dummy(1,lit_Undef);
  41     bwdsub_tmpunit   = Clause::Clause_new(dummy);
  42     remove_satisfied = false;
  43 }
  44
  45
  46 SimpSolver::~SimpSolver()
  47 {
  48     free(bwdsub_tmpunit);
  49
  50     // NOTE: elimtable.size() might be lower than nVars() at the moment
  51     for (int i = 0; i < elimtable.size(); i++)
  52         for (int j = 0; j < elimtable[i].eliminated.size(); j++)
  53             free(elimtable[i].eliminated[j]);
  54 }
  55
  56
  57 Var SimpSolver::newVar(bool sign, bool dvar) {
  58     Var v = Solver::newVar(sign, dvar);
  59
  60     if (use_simplification){
  61         n_occ    .push(0);
  62         n_occ    .push(0);
  63         occurs   .push();
  64         frozen   .push((char)false);
  65         touched  .push(0);
  66         elim_heap.insert(v);
  67         elimtable.push();
  68     }
  69     return v; }
  70
  71
  72
  73 bool SimpSolver::solve(const vec<Lit>& assumps, bool do_simp, bool turn_off_simp) {
  74     vec<Var> extra_frozen;
  75     bool     result = true;
  76
  77     do_simp &= use_simplification;
  78
  79     if (do_simp){
  80         // Assumptions must be temporarily frozen to run variable elimination:
  81         for (int i = 0; i < assumps.size(); i++){
  82             Var v = var(assumps[i]);
  83
  84             // If an assumption has been eliminated, remember it.
  85             if (isEliminated(v))
  86                 remember(v);
  87
  88             if (!frozen[v]){
  89                 // Freeze and store.
  90                 setFrozen(v, true);
  91                 extra_frozen.push(v);
  92             } }
  93
  94         result = eliminate(turn_off_simp);
  95     }
  96
  97     if (result)
  98         result = Solver::solve(assumps);
  99
 100     if (result) {
 101         extendModel();
 102 #ifndef NDEBUG
 103         verifyModel();
 104 #endif
 105     }
 106
 107     if (do_simp)
 108         // Unfreeze the assumptions that were frozen:
 109         for (int i = 0; i < extra_frozen.size(); i++)
 110             setFrozen(extra_frozen[i], false);
 111
 112     return result;
 113 }
 114
 115
 116
 117 bool SimpSolver::addClause(vec<Lit>& ps)
 118 {
 119     for (int i = 0; i < ps.size(); i++)
 120         if (isEliminated(var(ps[i])))
 121             remember(var(ps[i]));
 122
 123     int nclauses = clauses.size();
 124
 125     if (redundancy_check && implied(ps))
 126         return true;
 127
 128     if (!Solver::addClause(ps))
 129         return false;
 130
 131     if (use_simplification && clauses.size() == nclauses + 1){
 132         Clause& c = *clauses.last();
 133
 134         subsumption_queue.insert(&c);
 135
 136         for (int i = 0; i < c.size(); i++){
 137             assert(occurs.size() > var(c[i]));
 138             assert(!find(occurs[var(c[i])], &c));
 139
 140             occurs[var(c[i])].push(&c);
 141             n_occ[toInt(c[i])]++;
 142             touched[var(c[i])] = 1;
 143             assert(elimtable[var(c[i])].order == 0);
 144             if (elim_heap.inHeap(var(c[i])))
 145                 elim_heap.increase_(var(c[i]));
 146         }
 147     }
 148
 149     return true;
 150 }
 151
 152
 153 void SimpSolver::removeClause(Clause& c)
 154 {
 155     assert(!c.learnt());
 156
 157     if (use_simplification)
 158         for (int i = 0; i < c.size(); i++){
 159             n_occ[toInt(c[i])]--;
 160             updateElimHeap(var(c[i]));
 161         }
 162
 163     detachClause(c);
 164     c.mark(1);
 165 }
 166
 167
 168 bool SimpSolver::strengthenClause(Clause& c, Lit l)
 169 {
 170     assert(decisionLevel() == 0);
 171     assert(c.mark() == 0);
 172     assert(!c.learnt());
 173     assert(find(watches[toInt(~c[0])], &c));
 174     assert(find(watches[toInt(~c[1])], &c));
 175
 176     // FIX: this is too inefficient but would be nice to have (properly implemented)
 177     // if (!find(subsumption_queue, &c))
 178     subsumption_queue.insert(&c);
 179
 180     // If l is watched, delete it from watcher list and watch a new literal
 181     if (c[0] == l || c[1] == l){
 182         Lit other = c[0] == l ? c[1] : c[0];
 183         if (c.size() == 2){
 184             removeClause(c);
 185             c.strengthen(l);
 186         }else{
 187             c.strengthen(l);
 188             remove(watches[toInt(~l)], &c);
 189
 190             // Add a watch for the correct literal
 191             watches[toInt(~(c[1] == other ? c[0] : c[1]))].push(&c);
 192
 193             // !! this version assumes that remove does not change the order !!
 194             //watches[toInt(~c[1])].push(&c);
 195             clauses_literals -= 1;
 196         }
 197     }
 198     else{
 199         c.strengthen(l);
 200         clauses_literals -= 1;
 201     }
 202
 203     // if subsumption-indexing is active perform the necessary updates
 204     if (use_simplification){
 205         remove(occurs[var(l)], &c);
 206         n_occ[toInt(l)]--;
 207         updateElimHeap(var(l));
 208     }
 209
 210     return c.size() == 1 ? enqueue(c[0]) && propagate() == NULL : true;
 211 }
 212
 213
 214 // Returns FALSE if clause is always satisfied ('out_clause' should not be used).
 215 bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause)
 216 {
 217     merges++;
 218     out_clause.clear();
 219
 220     bool  ps_smallest = _ps.size() < _qs.size();
 221     const Clause& ps =  ps_smallest ? _qs : _ps;
 222     const Clause& qs =  ps_smallest ? _ps : _qs;
 223
 224     for (int i = 0; i < qs.size(); i++){
 225         if (var(qs[i]) != v){
 226             for (int j = 0; j < ps.size(); j++)
 227                 if (var(ps[j]) == var(qs[i])) {
 228                     if (ps[j] == ~qs[i])
 229                         return false;
 230                     else
 231                         goto next;
 232                 }
 233             out_clause.push(qs[i]);
 234         }
 235         next:;
 236     }
 237
 238     for (int i = 0; i < ps.size(); i++)
 239         if (var(ps[i]) != v)
 240             out_clause.push(ps[i]);
 241
 242     return true;
 243 }
 244
 245
 246 // Returns FALSE if clause is always satisfied.
 247 bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v)
 248 {
 249     merges++;
 250
 251     bool  ps_smallest = _ps.size() < _qs.size();
 252     const Clause& ps =  ps_smallest ? _qs : _ps;
 253     const Clause& qs =  ps_smallest ? _ps : _qs;
 254     const Lit* __ps = (const Lit*)ps;
 255     const Lit* __qs = (const Lit*)qs;
 256
 257     for (int i = 0; i < qs.size(); i++){
 258         if (var(__qs[i]) != v){
 259             for (int j = 0; j < ps.size(); j++)
 260                 if (var(__ps[j]) == var(__qs[i])) {
 261                     if (__ps[j] == ~__qs[i])
 262                         return false;
 263                     else
 264                         goto next;
 265                 }
 266         }
 267         next:;
 268     }
 269
 270     return true;
 271 }
 272
 273
 274 void SimpSolver::gatherTouchedClauses()
 275 {
 276     //fprintf(stderr, "Gathering clauses for backwards subsumption\n");
 277     int ntouched = 0;
 278     for (int i = 0; i < touched.size(); i++)
 279         if (touched[i]){
 280             const vec<Clause*>& cs = getOccurs(i);
 281             ntouched++;
 282             for (int j = 0; j < cs.size(); j++)
 283                 if (cs[j]->mark() == 0){
 284                     subsumption_queue.insert(cs[j]);
 285                     cs[j]->mark(2);
 286                 }
 287             touched[i] = 0;
 288         }
 289
 290     //fprintf(stderr, "Touched variables %d of %d yields %d clauses to check\n", ntouched, touched.size(), clauses.size());
 291     for (int i = 0; i < subsumption_queue.size(); i++)
 292         subsumption_queue[i]->mark(0);
 293 }
 294
 295
 296 bool SimpSolver::implied(const vec<Lit>& c)
 297 {
 298     assert(decisionLevel() == 0);
 299
 300     trail_lim.push(trail.size());
 301     for (int i = 0; i < c.size(); i++)
 302         if (value(c[i]) == l_True){
 303             cancelUntil(0);
 304             return false;
 305         }else if (value(c[i]) != l_False){
 306             assert(value(c[i]) == l_Undef);
 307             uncheckedEnqueue(~c[i]);
 308         }
 309
 310     bool result = propagate() != NULL;
 311     cancelUntil(0);
 312     return result;
 313 }
 314
 315
 316 // Backward subsumption + backward subsumption resolution
 317 bool SimpSolver::backwardSubsumptionCheck(bool verbose)
 318 {
 319     int cnt = 0;
 320     int subsumed = 0;
 321     int deleted_literals = 0;
 322     assert(decisionLevel() == 0);
 323
 324     while (subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()){
 325
 326         // Check top-level assignments by creating a dummy clause and placing it in the queue:
 327         if (subsumption_queue.size() == 0 && bwdsub_assigns < trail.size()){
 328             Lit l = trail[bwdsub_assigns++];
 329             (*bwdsub_tmpunit)[0] = l;
 330             bwdsub_tmpunit->calcAbstraction();
 331             assert(bwdsub_tmpunit->mark() == 0);
 332             subsumption_queue.insert(bwdsub_tmpunit); }
 333
 334         Clause&  c = *subsumption_queue.peek(); subsumption_queue.pop();
 335
 336         if (c.mark()) continue;
 337
 338         if (verbose && verbosity >= 2 && cnt++ % 1000 == 0)
 339             reportf("subsumption left: %10d (%10d subsumed, %10d deleted literals)\r", subsumption_queue.size(), subsumed, deleted_literals);
 340
 341         assert(c.size() > 1 || value(c[0]) == l_True);    // Unit-clauses should have been propagated before this point.
 342
 343         // Find best variable to scan:
 344         Var best = var(c[0]);
 345         for (int i = 1; i < c.size(); i++)
 346             if (occurs[var(c[i])].size() < occurs[best].size())
 347                 best = var(c[i]);
 348
 349         // Search all candidates:
 350         vec<Clause*>& _cs = getOccurs(best);
 351         Clause**       cs = (Clause**)_cs;
 352
 353         for (int j = 0; j < _cs.size(); j++)
 354             if (c.mark())
 355                 break;
 356             else if (!cs[j]->mark() && cs[j] != &c){
 357                 Lit l = c.subsumes(*cs[j]);
 358
 359                 if (l == lit_Undef)
 360                     subsumed++, removeClause(*cs[j]);
 361                 else if (l != lit_Error){
 362                     deleted_literals++;
 363
 364                     if (!strengthenClause(*cs[j], ~l))
 365                         return false;
 366
 367                     // Did current candidate get deleted from cs? Then check candidate at index j again:
 368                     if (var(l) == best)
 369                         j--;
 370                 }
 371             }
 372     }
 373
 374     return true;
 375 }
 376
 377
 378 bool SimpSolver::asymm(Var v, Clause& c)
 379 {
 380     assert(decisionLevel() == 0);
 381
 382     if (c.mark() || satisfied(c)) return true;
 383
 384     trail_lim.push(trail.size());
 385     Lit l = lit_Undef;
 386     for (int i = 0; i < c.size(); i++)
 387         if (var(c[i]) != v && value(c[i]) != l_False)
 388             uncheckedEnqueue(~c[i]);
 389         else
 390             l = c[i];
 391
 392     if (propagate() != NULL){
 393         cancelUntil(0);
 394         asymm_lits++;
 395         if (!strengthenClause(c, l))
 396             return false;
 397     }else
 398         cancelUntil(0);
 399
 400     return true;
 401 }
 402
 403
 404 bool SimpSolver::asymmVar(Var v)
 405 {
 406     assert(!frozen[v]);
 407     assert(use_simplification);
 408
 409     vec<Clause*>  pos, neg;
 410     const vec<Clause*>& cls = getOccurs(v);
 411
 412     if (value(v) != l_Undef || cls.size() == 0)
 413         return true;
 414
 415     for (int i = 0; i < cls.size(); i++)
 416         if (!asymm(v, *cls[i]))
 417             return false;
 418
 419     return backwardSubsumptionCheck();
 420 }
 421
 422
 423 void SimpSolver::verifyModel()
 424 {
 425     bool failed = false;
 426     int  cnt    = 0;
 427     // NOTE: elimtable.size() might be lower than nVars() at the moment
 428     for (int i = 0; i < elimtable.size(); i++)
 429         if (elimtable[i].order > 0)
 430             for (int j = 0; j < elimtable[i].eliminated.size(); j++){
 431                 cnt++;
 432                 Clause& c = *elimtable[i].eliminated[j];
 433                 for (int k = 0; k < c.size(); k++)
 434                     if (modelValue(c[k]) == l_True)
 435                         goto next;
 436
 437                 reportf("unsatisfied clause: ");
 438                 printClause(*elimtable[i].eliminated[j]);
 439                 reportf("\n");
 440                 failed = true;
 441             next:;
 442             }
 443
 444     assert(!failed);
 445     reportf("Verified %d eliminated clauses.\n", cnt);
 446 }
 447
 448
 449 bool SimpSolver::eliminateVar(Var v, bool fail)
 450 {
 451     if (!fail && asymm_mode && !asymmVar(v))    return false;
 452
 453     const vec<Clause*>& cls = getOccurs(v);
 454
 455 //  if (value(v) != l_Undef || cls.size() == 0) return true;
 456     if (value(v) != l_Undef) return true;
 457
 458     // Split the occurrences into positive and negative:
 459     vec<Clause*>  pos, neg;
 460     for (int i = 0; i < cls.size(); i++)
 461         (find(*cls[i], Lit(v)) ? pos : neg).push(cls[i]);
 462
 463     // Check if number of clauses decreases:
 464     int cnt = 0;
 465     for (int i = 0; i < pos.size(); i++)
 466         for (int j = 0; j < neg.size(); j++)
 467             if (merge(*pos[i], *neg[j], v) && ++cnt > cls.size() + grow)
 468                 return true;
 469
 470     // Delete and store old clauses:
 471     setDecisionVar(v, false);
 472     elimtable[v].order = elimorder++;
 473     assert(elimtable[v].eliminated.size() == 0);
 474     for (int i = 0; i < cls.size(); i++){
 475         elimtable[v].eliminated.push(Clause::Clause_new(*cls[i]));
 476         removeClause(*cls[i]); }
 477
 478     // Produce clauses in cross product:
 479     int top = clauses.size();
 480     vec<Lit> resolvent;
 481     for (int i = 0; i < pos.size(); i++)
 482         for (int j = 0; j < neg.size(); j++)
 483             if (merge(*pos[i], *neg[j], v, resolvent) && !addClause(resolvent))
 484                 return false;
 485
 486     // DEBUG: For checking that a clause set is saturated with respect to variable elimination.
 487     //        If the clause set is expected to be saturated at this point, this constitutes an
 488     //        error.
 489     if (fail){
 490         reportf("eliminated var %d, %d <= %d\n", v+1, cnt, cls.size());
 491         reportf("previous clauses:\n");
 492         for (int i = 0; i < cls.size(); i++){
 493             printClause(*cls[i]); reportf("\n"); }
 494         reportf("new clauses:\n");
 495         for (int i = top; i < clauses.size(); i++){
 496             printClause(*clauses[i]); reportf("\n"); }
 497         assert(0); }
 498
 499     return backwardSubsumptionCheck();
 500 }
 501
 502
 503 void SimpSolver::remember(Var v)
 504 {
 505     assert(decisionLevel() == 0);
 506     assert(isEliminated(v));
 507
 508     vec<Lit> clause;
 509
 510     // Re-activate variable:
 511     elimtable[v].order = 0;
 512     setDecisionVar(v, true); // Not good if the variable wasn't a decision variable before. Not sure how to fix this right now.
 513
 514     if (use_simplification)
 515         updateElimHeap(v);
 516
 517     // Reintroduce all old clauses which may implicitly remember other clauses:
 518     for (int i = 0; i < elimtable[v].eliminated.size(); i++){
 519         Clause& c = *elimtable[v].eliminated[i];
 520         clause.clear();
 521         for (int j = 0; j < c.size(); j++)
 522             clause.push(c[j]);
 523
 524         remembered_clauses++;
 525         check(addClause(clause));
 526         free(&c);
 527     }
 528
 529     elimtable[v].eliminated.clear();
 530 }
 531
 532
 533 void SimpSolver::extendModel()
 534 {
 535     vec<Var> vs;
 536
 537     // NOTE: elimtable.size() might be lower than nVars() at the moment
 538     for (int v = 0; v < elimtable.size(); v++)
 539         if (elimtable[v].order > 0)
 540             vs.push(v);
 541
 542     sort(vs, ElimOrderLt(elimtable));
 543
 544     for (int i = 0; i < vs.size(); i++){
 545         Var v = vs[i];
 546         Lit l = lit_Undef;
 547
 548         for (int j = 0; j < elimtable[v].eliminated.size(); j++){
 549             Clause& c = *elimtable[v].eliminated[j];
 550
 551             for (int k = 0; k < c.size(); k++)
 552                 if (var(c[k]) == v)
 553                     l = c[k];
 554                 else if (modelValue(c[k]) != l_False)
 555                     goto next;
 556
 557             assert(l != lit_Undef);
 558             model[v] = lbool(!sign(l));
 559             break;
 560
 561         next:;
 562         }
 563
 564         if (model[v] == l_Undef)
 565             model[v] = l_True;
 566     }
 567 }
 568
 569
 570 bool SimpSolver::eliminate(bool turn_off_elim)
 571 {
 572     if (!ok || !use_simplification)
 573         return ok;
 574
 575     // Main simplification loop:
 576     //assert(subsumption_queue.size() == 0);
 577     //gatherTouchedClauses();
 578     while (subsumption_queue.size() > 0 || elim_heap.size() > 0){
 579
 580         //fprintf(stderr, "subsumption phase: (%d)\n", subsumption_queue.size());
 581         if (!backwardSubsumptionCheck(true))
 582             return false;
 583
 584         //fprintf(stderr, "elimination phase:\n (%d)", elim_heap.size());
 585         for (int cnt = 0; !elim_heap.empty(); cnt++){
 586             Var elim = elim_heap.removeMin();
 587
 588             if (verbosity >= 2 && cnt % 100 == 0)
 589                 reportf("elimination left: %10d\r", elim_heap.size());
 590
 591             if (!frozen[elim] && !eliminateVar(elim))
 592                 return false;
 593         }
 594
 595         assert(subsumption_queue.size() == 0);
 596         gatherTouchedClauses();
 597     }
 598
 599     // Cleanup:
 600     cleanUpClauses();
 601     order_heap.filter(VarFilter(*this));
 602
 603 #ifdef INVARIANTS
 604     // Check that no more subsumption is possible:
 605     reportf("Checking that no more subsumption is possible\n");
 606     for (int i = 0; i < clauses.size(); i++){
 607         if (i % 1000 == 0)
 608             reportf("left %10d\r", clauses.size() - i);
 609
 610         assert(clauses[i]->mark() == 0);
 611         for (int j = 0; j < i; j++)
 612             assert(clauses[i]->subsumes(*clauses[j]) == lit_Error);
 613     }
 614     reportf("done.\n");
 615
 616     // Check that no more elimination is possible:
 617     reportf("Checking that no more elimination is possible\n");
 618     for (int i = 0; i < nVars(); i++)
 619         if (!frozen[i]) eliminateVar(i, true);
 620     reportf("done.\n");
 621     checkLiteralCount();
 622 #endif
 623
 624     // If no more simplification is needed, free all simplification-related data structures:
 625     if (turn_off_elim){
 626         use_simplification = false;
 627         touched.clear(true);
 628         occurs.clear(true);
 629         n_occ.clear(true);
 630         subsumption_queue.clear(true);
 631         elim_heap.clear(true);
 632         remove_satisfied = true;
 633     }
 634
 635
 636     return true;
 637 }
 638
 639
 640 void SimpSolver::cleanUpClauses()
 641 {
 642     int      i , j;
 643     vec<Var> dirty;
 644     for (i = 0; i < clauses.size(); i++)
 645         if (clauses[i]->mark() == 1){
 646             Clause& c = *clauses[i];
 647             for (int k = 0; k < c.size(); k++)
 648                 if (!seen[var(c[k])]){
 649                     seen[var(c[k])] = 1;
 650                     dirty.push(var(c[k]));
 651                 } }
 652
 653     for (i = 0; i < dirty.size(); i++){
 654         cleanOcc(dirty[i]);
 655         seen[dirty[i]] = 0; }
 656
 657     for (i = j = 0; i < clauses.size(); i++)
 658         if (clauses[i]->mark() == 1)
 659             free(clauses[i]);
 660         else
 661             clauses[j++] = clauses[i];
 662     clauses.shrink(i - j);
 663 }
 664
 665
 666 //=================================================================================================
 667 // Convert to DIMACS:
 668
 669
 670 void SimpSolver::toDimacs(FILE* f, Clause& c)
 671 {
 672     if (satisfied(c)) return;
 673
 674     for (int i = 0; i < c.size(); i++)
 675         if (value(c[i]) != l_False)
 676             fprintf(f, "%s%d ", sign(c[i]) ? "-" : "", var(c[i])+1);
 677     fprintf(f, "0\n");
 678 }
 679
 680
 681 void SimpSolver::toDimacs(const char* file)
 682 {
 683     assert(decisionLevel() == 0);
 684     FILE* f = fopen(file, "wr");
 685     if (f != NULL){
 686
 687         // Cannot use removeClauses here because it is not safe
 688         // to deallocate them at this point. Could be improved.
 689         int cnt = 0;
 690         for (int i = 0; i < clauses.size(); i++)
 691             if (!satisfied(*clauses[i]))
 692                 cnt++;
 693
 694         fprintf(f, "p cnf %d %d\n", nVars(), cnt);
 695
 696         for (int i = 0; i < clauses.size(); i++)
 697             toDimacs(f, *clauses[i]);
 698
 699         fprintf(stderr, "Wrote %d clauses...\n", clauses.size());
 700     }else
 701         fprintf(stderr, "could not open file %s\n", file);
 702 }