diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 80e6f403f..de1759486 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -7,7 +7,7 @@ def_module_params('sat', ('phase.caching.off', UINT, 100, 'phase caching off period (in number of conflicts)'), ('restart', SYMBOL, 'luby', 'restart strategy: luby or geometric'), ('restart.initial', UINT, 100, 'initial restart (number of conflicts)'), - ('restart.max', UINT, 0, 'maximal number of restarts. Ignored if set to 0'), + ('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'), ('restart.factor', DOUBLE, 1.5, 'restart increment factor for geometric strategy'), ('random_freq', DOUBLE, 0.01, 'frequency of random case splits'), ('random_seed', UINT, 0, 'random seed'), diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 8a75e8dfc..5c004b1a2 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -768,7 +768,7 @@ namespace sat { if (check_inconsistent()) return l_false; gc(); - if (m_config.m_restart_max != 0 && m_config.m_restart_max <= m_restarts) { + if (m_config.m_restart_max <= m_restarts) { IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-restarts\")\n";); return l_undef; } @@ -3122,6 +3122,9 @@ namespace sat { literal_vector lits; lbool is_sat = l_true; + if (m_config.m_restart_max != UINT_MAX && !m_model_is_current) { + return get_bounded_consequences(asms, vars, conseq); + } if (!m_model_is_current) { is_sat = check(asms.size(), asms.c_ptr()); } @@ -3142,9 +3145,89 @@ namespace sat { return is_sat; } + void solver::fixup_consequence_core() { + index_set s; + for (unsigned i = 0; i < m_core.size(); ++i) { + s |= m_antecedents.find(m_core[i].var()); + } + m_core.reset(); + index_set::iterator it = s.begin(), end = s.end(); + for (; it != end; ++it) { + m_core.push_back(to_literal(*it)); + } + } + + + lbool solver::get_bounded_consequences(literal_vector const& asms, bool_var_vector const& vars, vector& conseq) { + bool_var_set unfixed_vars; + unsigned num_units = 0, num_iterations = 0; + for (unsigned i = 0; i < vars.size(); ++i) { + unfixed_vars.insert(vars[i]); + } + m_antecedents.reset(); + pop_to_base_level(); + if (inconsistent()) return l_false; + init_search(); + propagate(false); + if (inconsistent()) return l_false; + if (asms.empty()) { + bool_var v = mk_var(true, false); + literal lit(v, false); + init_assumptions(1, &lit, 0, 0); + } + else { + init_assumptions(asms.size(), asms.c_ptr(), 0, 0); + } + propagate(false); + if (check_inconsistent()) return l_false; + + extract_fixed_consequences(num_units, asms, unfixed_vars, conseq); + + simplify_problem(); + if (check_inconsistent()) { + fixup_consequence_core(); + return l_false; + } + + while (true) { + ++num_iterations; + SASSERT(!inconsistent()); + + lbool r = bounded_search(); + if (r != l_undef) { + fixup_consequence_core(); + return r; + } + + extract_fixed_consequences(num_units, asms, unfixed_vars, conseq); + + if (m_conflicts > m_config.m_max_conflicts) { + IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = " << m_conflicts << "\")\n";); + return l_undef; + } + + restart(); + simplify_problem(); + if (check_inconsistent()) { + fixup_consequence_core(); + return l_false; + } + gc(); + + if (m_config.m_restart_max <= num_iterations) { + IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-restarts\")\n";); + return l_undef; + } + } + } + lbool solver::get_consequences(literal_vector const& asms, literal_vector const& lits, vector& conseq) { m_antecedents.reset(); - literal_set vars(lits), assumptions(asms); + literal_set unfixed_lits(lits), assumptions(asms); + bool_var_set unfixed_vars; + for (unsigned i = 0; i < lits.size(); ++i) { + unfixed_vars.insert(lits[i].var()); + } pop_to_base_level(); if (inconsistent()) return l_false; @@ -3163,11 +3246,15 @@ namespace sat { if (check_inconsistent()) return l_false; unsigned num_units = 0, num_iterations = 0; - extract_fixed_consequences(num_units, assumptions, vars, conseq); - while (!vars.empty()) { + extract_fixed_consequences(num_units, assumptions, unfixed_vars, conseq); + update_unfixed_literals(unfixed_lits, unfixed_vars); + while (!unfixed_lits.empty()) { + if (scope_lvl() > 1) { + pop(scope_lvl() - 1); + } ++num_iterations; checkpoint(); - literal_set::iterator it = vars.begin(), end = vars.end(); + literal_set::iterator it = unfixed_lits.begin(), end = unfixed_lits.end(); unsigned num_resolves = 0; lbool is_sat = l_true; for (; it != end; ++it) { @@ -3208,45 +3295,58 @@ namespace sat { m_inconsistent = false; } if (is_sat == l_true) { - delete_unfixed(vars); + delete_unfixed(unfixed_lits, unfixed_vars); } - extract_fixed_consequences(num_units, assumptions, vars, conseq); + extract_fixed_consequences(num_units, assumptions, unfixed_vars, conseq); + update_unfixed_literals(unfixed_lits, unfixed_vars); IF_VERBOSE(1, verbose_stream() << "(sat.get-consequences" << " iterations: " << num_iterations - << " variables: " << vars.size() + << " variables: " << unfixed_lits.size() << " fixed: " << conseq.size() - << " unfixed: " << lits.size() - conseq.size() - vars.size() + << " unfixed: " << lits.size() - conseq.size() - unfixed_lits.size() << ")\n";); - if (!vars.empty() && - m_config.m_restart_max != 0 && - m_config.m_restart_max <= num_iterations) { + if (!unfixed_lits.empty() && m_config.m_restart_max <= num_iterations) { return l_undef; } - } return l_true; } - void solver::delete_unfixed(literal_set& unfixed) { + void solver::delete_unfixed(literal_set& unfixed_lits, bool_var_set& unfixed_vars) { literal_set to_keep; - literal_set::iterator it = unfixed.begin(), end = unfixed.end(); + literal_set::iterator it = unfixed_lits.begin(), end = unfixed_lits.end(); for (; it != end; ++it) { literal lit = *it; if (value(lit) == l_true) { to_keep.insert(lit); } + else { + unfixed_vars.remove(lit.var()); + } } - unfixed = to_keep; + unfixed_lits = to_keep; } - void solver::extract_fixed_consequences(unsigned& start, literal_set const& assumptions, literal_set& unfixed, vector& conseq) { - if (scope_lvl() > 1) { - pop(scope_lvl() - 1); + void solver::update_unfixed_literals(literal_set& unfixed_lits, bool_var_set& unfixed_vars) { + literal_vector to_delete; + literal_set::iterator it = unfixed_lits.begin(), end = unfixed_lits.end(); + for (; it != end; ++it) { + literal lit = *it; + if (!unfixed_vars.contains(lit.var())) { + to_delete.push_back(lit); + } } + for (unsigned i = 0; i < to_delete.size(); ++i) { + unfixed_lits.remove(to_delete[i]); + } + } + + + void solver::extract_fixed_consequences(unsigned& start, literal_set const& assumptions, bool_var_set& unfixed, vector& conseq) { SASSERT(!inconsistent()); unsigned sz = m_trail.size(); - for (unsigned i = start; i < sz; ++i) { + for (unsigned i = start; i < sz && lvl(m_trail[i]) <= 1; ++i) { extract_fixed_consequences(m_trail[i], assumptions, unfixed, conseq); } start = sz; @@ -3288,7 +3388,7 @@ namespace sat { } } - void solver::extract_fixed_consequences(literal lit, literal_set const& assumptions, literal_set& unfixed, vector& conseq) { + void solver::extract_fixed_consequences(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector& conseq) { index_set s; if (assumptions.contains(lit)) { s.insert(lit.index()); @@ -3298,14 +3398,14 @@ namespace sat { extract_assumptions(lit, s); } m_antecedents.insert(lit.var(), s); - if (unfixed.contains(lit)) { + if (unfixed.contains(lit.var())) { literal_vector cons; cons.push_back(lit); index_set::iterator it = s.begin(), end = s.end(); for (; it != end; ++it) { cons.push_back(to_literal(*it)); } - unfixed.remove(lit); + unfixed.remove(lit.var()); conseq.push_back(cons); } } diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index aa45a1043..a9037c65a 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -457,11 +457,17 @@ namespace sat { lbool get_consequences(literal_vector const& assms, literal_vector const& lits, vector& conseq); - void delete_unfixed(literal_set& unfixed); + lbool get_bounded_consequences(literal_vector const& assms, bool_var_vector const& vars, vector& conseq); - void extract_fixed_consequences(unsigned& start, literal_set const& assumptions, literal_set& unfixed, vector& conseq); + void delete_unfixed(literal_set& unfixed_lits, bool_var_set& unfixed_vars); - void extract_fixed_consequences(literal lit, literal_set const& assumptions, literal_set& unfixed, vector& conseq); + void extract_fixed_consequences(unsigned& start, literal_set const& assumptions, bool_var_set& unfixed, vector& conseq); + + void extract_fixed_consequences(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector& conseq); + + void update_unfixed_literals(literal_set& unfixed_lits, bool_var_set& unfixed_vars); + + void fixup_consequence_core(); // ----------------------- // diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 6d3a5b552..b7ce92108 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -252,12 +252,17 @@ public: m_solver.pop_to_base_level(); lbool r = internalize_formulas(); if (r != l_true) return r; + r = internalize_vars(vars, bvars); + if (r != l_true) return r; r = internalize_assumptions(assumptions.size(), assumptions.c_ptr(), dep2asm); if (r != l_true) return r; - r = internalize_vars(vars, bvars); - r = m_solver.get_consequences(m_asms, bvars, lconseq); - if (r == l_false) return r; + if (r == l_false) { + if (!m_asms.empty()) { + extract_core(dep2asm); + } + return r; + } // build map from bound variables to // the consequences that cover them.