diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index e0c1b1696..faa9b639e 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -1288,7 +1288,6 @@ namespace sat { if (!create_asserting_lemma()) { goto bail_out; } - active2card(); DEBUG_CODE(VERIFY(validate_conflict(m_lemma, m_A));); @@ -1347,6 +1346,7 @@ namespace sat { } bool ba_solver::create_asserting_lemma() { + bool adjusted = false; adjust_conflict_level: int64 bound64 = m_bound; @@ -1354,7 +1354,6 @@ namespace sat { for (bool_var v : m_active_vars) { slack += get_abs_coeff(v); } - m_lemma.reset(); m_lemma.push_back(null_literal); unsigned num_skipped = 0; @@ -1389,26 +1388,32 @@ namespace sat { } } } - if (slack >= 0) { IF_VERBOSE(20, verbose_stream() << "(sat.card slack: " << slack << " skipped: " << num_skipped << ")\n";); return false; } - + if (m_overflow) { + return false; + } if (m_lemma[0] == null_literal) { if (m_lemma.size() == 1) { s().set_conflict(justification()); return false; } + return false; unsigned old_level = m_conflict_lvl; m_conflict_lvl = 0; for (unsigned i = 1; i < m_lemma.size(); ++i) { m_conflict_lvl = std::max(m_conflict_lvl, lvl(m_lemma[i])); } - IF_VERBOSE(10, verbose_stream() << "(sat.backjump :new-level " << m_conflict_lvl << " :old-level " << old_level << ")\n";); + IF_VERBOSE(1, verbose_stream() << "(sat.backjump :new-level " << m_conflict_lvl << " :old-level " << old_level << ")\n";); + adjusted = true; goto adjust_conflict_level; } - return !m_overflow; + if (!adjusted) { + active2card(); + } + return true; } /* diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 3db2908ed..d7b0e0892 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -1153,6 +1153,8 @@ struct sat2goal::imp { } } } + //s.display(std::cout); + //r.display(std::cout); } void add_clause(sat::literal_vector const& lits, expr_ref_vector& lemmas) { diff --git a/src/tactic/portfolio/parallel_tactic.cpp b/src/tactic/portfolio/parallel_tactic.cpp index 9bacbe6a0..4eb2fbbe9 100644 --- a/src/tactic/portfolio/parallel_tactic.cpp +++ b/src/tactic/portfolio/parallel_tactic.cpp @@ -63,12 +63,16 @@ class parallel_tactic : public tactic { unsigned num_units() const { return m_units; } + unsigned cube_size() const { return m_cube.size(); } + solver& get_solver() { return *m_solver; } solver const& get_solver() const { return *m_solver; } params_ref const& params() const { return m_params; } + params_ref& params() { return m_params; } + solver_state* clone(params_ref const& p, expr* cube) { ast_manager& m = m_solver->get_manager(); ast_manager* new_m = alloc(ast_manager, m, !m.proof_mode()); @@ -114,7 +118,7 @@ private: m_conflicts_decay_rate = 75; m_max_conflicts = m_conflicts_lower_bound; m_progress = 0; - m_num_threads = omp_get_num_procs(); // TBD adjust by possible threads used inside each solver. + m_num_threads = 2 * omp_get_num_procs(); // TBD adjust by possible threads used inside each solver. } unsigned get_max_conflicts() { @@ -175,16 +179,14 @@ private: } } - lbool simplify(solver& s) { - params_ref p; - p.copy(m_params); - p.set_uint("max_conflicts", 10); - p.set_bool("lookahead_simplify", true); - s.updt_params(p); - lbool is_sat = s.check_sat(0,0); - p.set_uint("max_conflicts", get_max_conflicts()); - p.set_bool("lookahead_simplify", false); - s.updt_params(p); + lbool simplify(solver_state& s) { + s.params().set_uint("max_conflicts", 10); + s.params().set_bool("lookahead_simplify", true); + s.get_solver().updt_params(s.params()); + lbool is_sat = s.get_solver().check_sat(0,0); + s.params().set_uint("max_conflicts", get_max_conflicts()); + s.params().set_bool("lookahead_simplify", false); + s.get_solver().updt_params(s.params()); return is_sat; } @@ -228,12 +230,10 @@ private: return l_undef; } - lbool solve(solver& s) { - params_ref p; - p.copy(m_params); - p.set_uint("max_conflicts", get_max_conflicts()); - s.updt_params(p); - return s.check_sat(0, 0); + lbool solve(solver_state& s) { + s.params().set_uint("max_conflicts", get_max_conflicts()); + s.get_solver().updt_params(s.params()); + return s.get_solver().check_sat(0, 0); } void remove_unsat(svector& unsat) { @@ -260,6 +260,25 @@ private: } lbool solve(model_ref& mdl) { + + { + solver_state& st = *m_solvers[0]; + st.params().set_uint("restart.max", 200); + st.get_solver().updt_params(st.params()); + lbool is_sat = st.get_solver().check_sat(0, 0); + st.params().set_uint("restart.max", UINT_MAX); + st.get_solver().updt_params(st.params()); + switch (is_sat) { + case l_true: + get_model(mdl, 0); + return l_true; + case l_false: + return l_false; + default: + break; + } + } + while (true) { int sz = pick_solvers(); @@ -276,7 +295,7 @@ private: #pragma omp parallel for for (int i = 0; i < sz; ++i) { - lbool is_sat = simplify(m_solvers[i]->get_solver()); + lbool is_sat = simplify(*m_solvers[i]); switch (is_sat) { case l_false: #pragma omp critical (parallel_tactic) @@ -305,7 +324,7 @@ private: #pragma omp parallel for for (int i = 0; i < sz; ++i) { - lbool is_sat = solve(m_solvers[i]->get_solver()); + lbool is_sat = solve(*m_solvers[i]); switch (is_sat) { case l_false: #pragma omp critical (parallel_tactic) @@ -328,6 +347,7 @@ private: remove_unsat(unsat); sz = std::min(max_num_splits(), sz); + sz = std::min(static_cast(m_num_threads/2), sz); if (sz == 0) continue; @@ -360,9 +380,9 @@ private: } std::ostream& display(std::ostream& out) { + out << "branches: " << m_solvers.size() << "\n"; for (solver_state* s : m_solvers) { - out << "solver units " << s->num_units() << "\n"; - out << "cube " << s->cube() << "\n"; + out << "cube " << s->cube_size() << " units " << s->num_units() << "\n"; } m_stats.display(out); return out;