1 /*++ 2 Copyright (c) 2011 Microsoft Corporation 3 4 Module Name: 5 6 sat_solver.cpp 7 8 Abstract: 9 10 SAT solver main class. 11 12 Author: 13 14 Leonardo de Moura (leonardo) 2011-05-21. 15 16 Revision History: 17 18 --*/ 19 20 21 #include "sat/sat_solver.h" 22 23 #define ENABLE_TERNARY true 24 25 namespace sat { 26 27 // ----------------------- 28 // 29 // GC 30 // 31 // ----------------------- 32 should_gc() const33 bool solver::should_gc() const { 34 return 35 m_conflicts_since_gc > m_gc_threshold && 36 (m_config.m_gc_strategy != GC_DYN_PSM || at_base_lvl()); 37 } 38 do_gc()39 void solver::do_gc() { 40 if (!should_gc()) return; 41 TRACE("sat", tout << m_conflicts_since_gc << " " << m_gc_threshold << "\n";); 42 unsigned gc = m_stats.m_gc_clause; 43 m_conflicts_since_gc = 0; 44 m_gc_threshold += m_config.m_gc_increment; 45 IF_VERBOSE(10, verbose_stream() << "(sat.gc)\n";); 46 CASSERT("sat_gc_bug", check_invariant()); 47 switch (m_config.m_gc_strategy) { 48 case GC_GLUE: 49 gc_glue(); 50 break; 51 case GC_PSM: 52 gc_psm(); 53 break; 54 case GC_GLUE_PSM: 55 gc_glue_psm(); 56 break; 57 case GC_PSM_GLUE: 58 gc_psm_glue(); 59 break; 60 case GC_DYN_PSM: 61 if (!m_assumptions.empty()) { 62 gc_glue_psm(); 63 break; 64 } 65 if (!at_base_lvl()) 66 return; 67 gc_dyn_psm(); 68 break; 69 default: 70 UNREACHABLE(); 71 break; 72 } 73 if (m_ext) m_ext->gc(); 74 if (gc > 0 && should_defrag()) { 75 defrag_clauses(); 76 } 77 CASSERT("sat_gc_bug", check_invariant()); 78 } 79 80 /** 81 \brief Lex on (glue, size) 82 */ 83 struct glue_lt { operator ()sat::glue_lt84 bool operator()(clause const * c1, clause const * c2) const { 85 if (c1->glue() < c2->glue()) return true; 86 return c1->glue() == c2->glue() && c1->size() < c2->size(); 87 } 88 }; 89 90 /** 91 \brief Lex on (psm, size) 92 */ 93 struct psm_lt { operator ()sat::psm_lt94 bool operator()(clause const * c1, clause const * c2) const { 95 if (c1->psm() < c2->psm()) return true; 96 return c1->psm() == c2->psm() && c1->size() < c2->size(); 97 } 98 }; 99 100 /** 101 \brief Lex on (glue, psm, size) 102 */ 103 struct glue_psm_lt { operator ()sat::glue_psm_lt104 bool operator()(clause const * c1, clause const * c2) const { 105 if (c1->glue() < c2->glue()) return true; 106 if (c1->glue() > c2->glue()) return false; 107 if (c1->psm() < c2->psm()) return true; 108 if (c1->psm() > c2->psm()) return false; 109 return c1->size() < c2->size(); 110 } 111 }; 112 113 /** 114 \brief Lex on (psm, glue, size) 115 */ 116 struct psm_glue_lt { operator ()sat::psm_glue_lt117 bool operator()(clause const * c1, clause const * c2) const { 118 if (c1->psm() < c2->psm()) return true; 119 if (c1->psm() > c2->psm()) return false; 120 if (c1->glue() < c2->glue()) return true; 121 if (c1->glue() > c2->glue()) return false; 122 return c1->size() < c2->size(); 123 } 124 }; 125 gc_glue()126 void solver::gc_glue() { 127 std::stable_sort(m_learned.begin(), m_learned.end(), glue_lt()); 128 gc_half("glue"); 129 } 130 gc_psm()131 void solver::gc_psm() { 132 save_psm(); 133 std::stable_sort(m_learned.begin(), m_learned.end(), psm_lt()); 134 gc_half("psm"); 135 } 136 gc_glue_psm()137 void solver::gc_glue_psm() { 138 save_psm(); 139 std::stable_sort(m_learned.begin(), m_learned.end(), glue_psm_lt()); 140 gc_half("glue-psm"); 141 } 142 gc_psm_glue()143 void solver::gc_psm_glue() { 144 save_psm(); 145 std::stable_sort(m_learned.begin(), m_learned.end(), psm_glue_lt()); 146 gc_half("psm-glue"); 147 } 148 149 /** 150 \brief Compute the psm of all learned clauses. 151 */ save_psm()152 void solver::save_psm() { 153 for (clause* cp : m_learned) { 154 cp->set_psm(psm(*cp)); 155 } 156 } 157 158 /** 159 \brief GC (the second) half of the clauses in the database. 160 */ gc_half(char const * st_name)161 void solver::gc_half(char const * st_name) { 162 TRACE("sat", tout << "gc\n";); 163 unsigned sz = m_learned.size(); 164 unsigned new_sz = sz/2; // std::min(sz/2, m_clauses.size()*2); 165 unsigned j = new_sz; 166 for (unsigned i = new_sz; i < sz; i++) { 167 clause & c = *(m_learned[i]); 168 if (can_delete(c)) { 169 detach_clause(c); 170 del_clause(c); 171 } 172 else { 173 m_learned[j] = &c; 174 j++; 175 } 176 } 177 new_sz = j; 178 m_stats.m_gc_clause += sz - new_sz; 179 m_learned.shrink(new_sz); 180 IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat-gc :strategy " << st_name << " :deleted " << (sz - new_sz) << ")\n";); 181 } 182 can_delete3(literal l1,literal l2,literal l3) const183 bool solver::can_delete3(literal l1, literal l2, literal l3) const { 184 if (value(l1) == l_true && 185 value(l2) == l_false && 186 value(l3) == l_false) { 187 justification const& j = m_justification[l1.var()]; 188 if (j.is_ternary_clause()) { 189 watched w1(l2, l3); 190 watched w2(j.get_literal1(), j.get_literal2()); 191 return w1 != w2; 192 } 193 } 194 return true; 195 } 196 can_delete(clause const & c) const197 bool solver::can_delete(clause const & c) const { 198 if (c.on_reinit_stack()) 199 return false; 200 if (ENABLE_TERNARY && c.size() == 3) { 201 return 202 can_delete3(c[0],c[1],c[2]) && 203 can_delete3(c[1],c[0],c[2]) && 204 can_delete3(c[2],c[0],c[1]); 205 } 206 literal l0 = c[0]; 207 if (value(l0) != l_true) 208 return true; 209 justification const & jst = m_justification[l0.var()]; 210 return !jst.is_clause() || cls_allocator().get_clause(jst.get_clause_offset()) != &c; 211 } 212 213 /** 214 \brief Use gc based on dynamic psm. Clauses are initially frozen. 215 */ gc_dyn_psm()216 void solver::gc_dyn_psm() { 217 TRACE("sat", tout << "gc\n";); 218 // To do gc at scope_lvl() > 0, I will need to use the reinitialization stack, or live with the fact 219 // that I may miss some propagations for reactivated clauses. 220 SASSERT(at_base_lvl()); 221 // compute 222 // d_tk 223 unsigned h = 0; 224 unsigned V_tk = 0; 225 for (bool_var v = 0; v < num_vars(); v++) { 226 if (m_assigned_since_gc[v]) { 227 V_tk++; 228 m_assigned_since_gc[v] = false; 229 } 230 if (m_phase[v] != m_prev_phase[v]) { 231 h++; 232 m_prev_phase[v] = m_phase[v]; 233 } 234 } 235 double d_tk = V_tk == 0 ? static_cast<double>(num_vars() + 1) : static_cast<double>(h)/static_cast<double>(V_tk); 236 if (d_tk < m_min_d_tk) 237 m_min_d_tk = d_tk; 238 TRACE("sat_frozen", tout << "m_min_d_tk: " << m_min_d_tk << "\n";); 239 unsigned frozen = 0; 240 unsigned deleted = 0; 241 unsigned activated = 0; 242 clause_vector::iterator it = m_learned.begin(); 243 clause_vector::iterator it2 = it; 244 clause_vector::iterator end = m_learned.end(); 245 for (; it != end; ++it) { 246 clause & c = *(*it); 247 if (!c.frozen()) { 248 // Active clause 249 if (c.glue() > m_config.m_gc_small_lbd) { 250 // I never delete clauses with small lbd 251 if (c.was_used()) { 252 c.reset_inact_rounds(); 253 } 254 else { 255 c.inc_inact_rounds(); 256 if (c.inact_rounds() > m_config.m_gc_k) { 257 detach_clause(c); 258 del_clause(c); 259 m_stats.m_gc_clause++; 260 deleted++; 261 continue; 262 } 263 } 264 c.unmark_used(); 265 if (psm(c) > static_cast<unsigned>(c.size() * m_min_d_tk)) { 266 // move to frozen; 267 TRACE("sat_frozen", tout << "freezing size: " << c.size() << " psm: " << psm(c) << " " << c << "\n";); 268 detach_clause(c); 269 c.reset_inact_rounds(); 270 c.freeze(); 271 m_num_frozen++; 272 frozen++; 273 } 274 } 275 } 276 else { 277 // frozen clause 278 clause & c = *(*it); 279 if (psm(c) <= static_cast<unsigned>(c.size() * m_min_d_tk)) { 280 c.unfreeze(); 281 m_num_frozen--; 282 activated++; 283 if (!activate_frozen_clause(c)) { 284 // clause was satisfied, reduced to a conflict, unit or binary clause. 285 del_clause(c); 286 continue; 287 } 288 } 289 else { 290 c.inc_inact_rounds(); 291 if (c.inact_rounds() > m_config.m_gc_k) { 292 del_clause(c); 293 m_stats.m_gc_clause++; 294 deleted++; 295 continue; 296 } 297 } 298 } 299 *it2 = *it; 300 ++it2; 301 } 302 m_learned.set_end(it2); 303 IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat-gc :d_tk " << d_tk << " :min-d_tk " << m_min_d_tk << 304 " :frozen " << frozen << " :activated " << activated << " :deleted " << deleted << ")\n";); 305 } 306 307 // return true if should keep the clause, and false if we should delete it. activate_frozen_clause(clause & c)308 bool solver::activate_frozen_clause(clause & c) { 309 TRACE("sat_gc", tout << "reactivating:\n" << c << "\n";); 310 SASSERT(at_base_lvl()); 311 // do some cleanup 312 unsigned sz = c.size(); 313 unsigned j = 0; 314 for (unsigned i = 0; i < sz; i++) { 315 literal l = c[i]; 316 switch (value(l)) { 317 case l_true: 318 return false; 319 case l_false: 320 break; 321 case l_undef: 322 if (i != j) { 323 std::swap(c[i], c[j]); 324 } 325 j++; 326 break; 327 } 328 } 329 TRACE("sat", tout << "after cleanup:\n" << mk_lits_pp(j, c.begin()) << "\n";); 330 unsigned new_sz = j; 331 switch (new_sz) { 332 case 0: 333 if (m_config.m_drat) m_drat.add(); 334 set_conflict(); 335 return false; 336 case 1: 337 assign_unit(c[0]); 338 return false; 339 case 2: 340 mk_bin_clause(c[0], c[1], true); 341 return false; 342 default: 343 shrink(c, sz, new_sz); 344 attach_clause(c); 345 return true; 346 } 347 } 348 349 /** 350 \brief Compute phase saving measure for the given clause. 351 */ psm(clause const & c) const352 unsigned solver::psm(clause const & c) const { 353 unsigned r = 0; 354 for (literal l : c) { 355 if (l.sign() ^ m_phase[l.var()]) { 356 r++; 357 } 358 } 359 return r; 360 } 361 362 /** 363 * Control the size of the reinit-stack. 364 * by agressively garbage collecting lemmas that are not asserting. 365 */ 366 gc_reinit_stack(unsigned num_scopes)367 void solver::gc_reinit_stack(unsigned num_scopes) { 368 return; 369 SASSERT (!at_base_lvl()); 370 unsigned new_lvl = scope_lvl() - num_scopes; 371 ptr_vector<clause> to_gc; 372 unsigned j = m_scopes[new_lvl].m_clauses_to_reinit_lim; 373 unsigned sz = m_clauses_to_reinit.size(); 374 if (sz - j <= 2000) 375 return; 376 for (unsigned i = j; i < sz; ++i) { 377 auto cw = m_clauses_to_reinit[i]; 378 if (cw.is_binary() || is_asserting(new_lvl, cw)) 379 m_clauses_to_reinit[j++] = cw; 380 else 381 to_gc.push_back(cw.get_clause()); 382 } 383 m_clauses_to_reinit.shrink(j); 384 if (to_gc.empty()) 385 return; 386 for (clause* c : to_gc) { 387 SASSERT(c->on_reinit_stack()); 388 c->set_removed(true); 389 c->set_reinit_stack(false); 390 } 391 j = 0; 392 for (unsigned i = 0; i < m_learned.size(); ++i) { 393 clause & c = *(m_learned[i]); 394 if (c.was_removed()) { 395 detach_clause(c); 396 del_clause(c); 397 } 398 else 399 m_learned[j++] = &c; 400 } 401 std::cout << "gc: " << to_gc.size() << " " << m_learned.size() << " -> " << j << "\n"; 402 SASSERT(m_learned.size() - j == to_gc.size()); 403 m_learned.shrink(j); 404 } 405 is_asserting(unsigned new_lvl,clause_wrapper const & cw) const406 bool solver::is_asserting(unsigned new_lvl, clause_wrapper const& cw) const { 407 if (!cw.is_learned()) 408 return true; 409 bool seen_true = false; 410 for (literal lit : cw) { 411 switch (value(lit)) { 412 case l_true: 413 if (lvl(lit) > new_lvl || seen_true) 414 return false; 415 seen_true = true; 416 continue; 417 case l_false: 418 continue; 419 case l_undef: 420 return false; 421 } 422 } 423 return true; 424 } 425 gc_vars(bool_var max_var)426 void solver::gc_vars(bool_var max_var) { 427 init_visited(); 428 m_aux_literals.reset(); 429 auto gc_watch = [&](literal lit) { 430 auto& wl1 = get_wlist(lit); 431 for (auto w : get_wlist(lit)) { 432 if (w.is_binary_clause() && w.get_literal().var() < max_var && !is_visited(w.get_literal())) { 433 m_aux_literals.push_back(w.get_literal()); 434 mark_visited(w.get_literal()); 435 } 436 } 437 wl1.reset(); 438 }; 439 for (unsigned v = max_var; v < num_vars(); ++v) { 440 gc_watch(literal(v, false)); 441 gc_watch(literal(v, true)); 442 } 443 444 for (literal lit : m_aux_literals) { 445 auto& wl2 = get_wlist(~lit); 446 unsigned j = 0; 447 for (auto w2 : wl2) 448 if (!w2.is_binary_clause() || w2.get_literal().var() < max_var) 449 wl2[j++] = w2; 450 wl2.shrink(j); 451 } 452 m_aux_literals.reset(); 453 454 auto gc_clauses = [&](ptr_vector<clause>& clauses) { 455 unsigned j = 0; 456 for (clause* c : clauses) { 457 bool should_remove = false; 458 for (auto lit : *c) 459 should_remove |= lit.var() >= max_var; 460 if (should_remove) { 461 SASSERT(!c->on_reinit_stack()); 462 detach_clause(*c); 463 del_clause(*c); 464 } 465 else { 466 clauses[j++] = c; 467 } 468 } 469 clauses.shrink(j); 470 }; 471 gc_clauses(m_learned); 472 gc_clauses(m_clauses); 473 474 if (m_ext) 475 m_ext->gc_vars(max_var); 476 477 unsigned j = 0; 478 for (literal lit : m_trail) { 479 SASSERT(lvl(lit) == 0); 480 if (lit.var() < max_var) 481 m_trail[j++] = lit; 482 } 483 m_trail.shrink(j); 484 shrink_vars(max_var); 485 } 486 487 #if 0 488 void solver::gc_reinit_stack(unsigned num_scopes) { 489 SASSERT (!at_base_lvl()); 490 collect_clauses_to_gc(num_scopes); 491 for (literal lit : m_watch_literals_to_gc) { 492 mark_members_of_watch_list(lit); 493 shrink_watch_list(lit); 494 } 495 unsigned j = 0; 496 for (clause* c : m_learned) 497 if (!c->was_removed()) 498 m_learned[j++] = c; 499 m_learned.shrink(j); 500 for (clause* c : m_clauses_to_gc) 501 del_clause(*c); 502 m_clauses_to_gc.reset(); 503 } 504 505 void solver::add_to_gc(literal lit, clause_wrapper const& cw) { 506 m_literal2gc_clause.reserve(lit.index()+1); 507 m_literal2gc_clause[lit.index()].push_back(cw); 508 if (!is_visited(lit)) { 509 mark_visited(lit); 510 m_watch_literals_to_gc.push_back(lit); 511 } 512 } 513 514 void solver::add_to_gc(clause_wrapper const& cw) { 515 std::cout << "add-to-gc " << cw << "\n"; 516 if (cw.is_binary()) { 517 add_to_gc(cw[0], cw); 518 add_to_gc(cw[1], clause_wrapper(cw[1], cw[0])); 519 } 520 else if (ENABLE_TERNARY && cw.is_ternary()) { 521 SASSERT(cw.is_learned()); 522 add_to_gc(cw[0], cw); 523 add_to_gc(cw[1], cw); 524 add_to_gc(cw[2], cw); 525 cw.get_clause()->set_removed(true); 526 } 527 else { 528 SASSERT(cw.is_learned()); 529 add_to_gc(cw[0], cw); 530 add_to_gc(cw[1], cw); 531 cw.get_clause()->set_removed(true); 532 } 533 } 534 535 void solver::insert_ternary_to_delete(literal lit, clause_wrapper const& cw) { 536 SASSERT(cw.is_ternary()); 537 SASSERT(lit == cw[0] || lit == cw[1] || lit == cw[2]); 538 literal lit1, lit2; 539 if (cw[0] == lit) 540 lit1 = cw[1], lit2 = cw[2]; 541 else if (cw[1] == lit) 542 lit1 = cw[0], lit2 = cw[2]; 543 else 544 lit1 = cw[0], lit2 = cw[1]; 545 insert_ternary_to_delete(lit1, lit2, true); 546 } 547 548 void solver::insert_ternary_to_delete(literal lit1, literal lit2, bool should_delete) { 549 if (lit1.index() > lit2.index()) 550 std::swap(lit1, lit2); 551 m_ternary_to_delete.push_back(std::tuple(lit1, lit2, should_delete)); 552 } 553 554 bool solver::in_ternary_to_delete(literal lit1, literal lit2) { 555 if (lit1.index() > lit2.index()) 556 std::swap(lit1, lit2); 557 bool found = m_ternary_to_delete.contains(std::make_pair(lit1, lit2)); 558 if (found) std::cout << lit1 << " " << lit2 << "\n"; 559 return found; 560 } 561 562 563 void solver::collect_clauses_to_gc(unsigned num_scopes) { 564 unsigned new_lvl = scope_lvl() - num_scopes; 565 init_visited(); 566 m_watch_literals_to_gc.reset(); 567 unsigned j = m_scopes[new_lvl].m_clauses_to_reinit_lim; 568 for (unsigned i = j, sz = m_clauses_to_reinit.size(); i < sz; ++i) { 569 auto cw = m_clauses_to_reinit[i]; 570 if (is_asserting(new_lvl, cw)) 571 m_clauses_to_reinit[j++] = cw; 572 else 573 add_to_gc(cw); 574 } 575 m_clauses_to_reinit.shrink(j); 576 SASSERT(m_clauses_to_reinit.size() >= j); 577 } 578 579 void solver::mark_members_of_watch_list(literal lit) { 580 init_visited(); 581 m_ternary_to_delete.reset(); 582 for (auto const& cw : m_literal2gc_clause[lit.index()]) { 583 SASSERT(!cw.is_binary() || lit == cw[0]); 584 SASSERT(cw.is_binary() || cw.was_removed()); 585 if (cw.is_binary()) 586 mark_visited(cw[1]); 587 else if (ENABLE_TERNARY && cw.is_ternary()) 588 insert_ternary_to_delete(lit, cw); 589 } 590 } 591 592 void solver::shrink_watch_list(literal lit) { 593 auto& wl = get_wlist((~lit).index()); 594 unsigned j = 0, sz = wl.size(), end = sz; 595 for (unsigned i = 0; i < end; ++i) { 596 auto w = wl[i]; 597 if (w.is_binary_clause() && !is_visited(w.get_literal())) 598 wl[j++] = w; 599 else if (ENABLE_TERNARY && w.is_ternary_clause()) 600 insert_ternary_to_delete(w.literal1(), w.literal2(), false); 601 else if (w.is_clause() && !get_clause(w).was_removed()) 602 wl[j++] = w; 603 else if (w.is_ext_constraint()) 604 wl[j++] = w; 605 } 606 #if 0 607 std::sort(m_ternary_to_delete.begin(), m_ternary_to_delete.end()); 608 int prev = -1; 609 unsigned k = 0; 610 std::tuple<literal, literal, bool> p = tuple(null_literal, null_literal, false); 611 for (unsigned i = 0; i < m_ternary_to_delete.size(); ++i) { 612 auto const& t = m_ternary_to_delete[i]; 613 } 614 #endif 615 std::cout << "gc-watch-list " << lit << " " << wl.size() << " -> " << j << "\n"; 616 wl.shrink(j); 617 m_literal2gc_clause[lit.index()].reset(); 618 } 619 620 621 #endif 622 623 } 624