From 82922d92f7527c5b4060fbedcc376865d473e6ac Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 24 Sep 2017 13:29:46 -0700 Subject: [PATCH] add cube functionality Signed-off-by: Nikolaj Bjorner --- src/sat/sat_lookahead.cpp | 124 ++++++++++++++++++++++---------------- src/sat/sat_lookahead.h | 6 +- src/sat/sat_solver.cpp | 9 +-- src/sat/sat_solver.h | 2 +- 4 files changed, 83 insertions(+), 58 deletions(-) diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 7205b9ac3..6b55802d0 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -820,6 +820,15 @@ namespace sat { } return out; } + + void lookahead::display_search_string() { + printf("\r"); + std::stringstream strm; + strm << pp_prefix(m_prefix, m_trail_lim.size()); + for (unsigned i = 0; i < 50; ++i) strm << " "; + printf(strm.str().c_str()); + fflush(stdout); + } void lookahead::construct_lookahead_table() { literal u = get_child(null_literal), v = null_literal; @@ -1710,47 +1719,6 @@ namespace sat { return true; } - void lookahead::cube() { - m_model.reset(); - scoped_level _sl(*this, c_fixed_truth); - literal_vector trail; - m_search_mode = lookahead_mode::searching; - double freevars_threshold = 0; - while (true) { - TRACE("sat", display(tout);); - inc_istamp(); - checkpoint(); - literal l = choose(); - if (inconsistent()) { - freevars_threshold = m_freevars.size(); - if (!backtrack(trail)) return; - continue; - } - unsigned depth = m_trail_lim.size(); - if (l == null_literal || - (m_config.m_cube_cutoff != 0 && depth == m_config.m_cube_cutoff) || - (m_config.m_cube_cutoff == 0 && m_freevars.size() < freevars_threshold)) { - display_cube(std::cout); - set_conflict(); - if (!backtrack(trail)) return; - freevars_threshold *= (1.0 - pow(m_config.m_cube_fraction, depth)); - continue; - } - TRACE("sat", tout << "choose: " << l << " " << trail << "\n";); - ++m_stats.m_decisions; - IF_VERBOSE(1, printf("\r"); - std::stringstream strm; - strm << pp_prefix(m_prefix, m_trail_lim.size()); - for (unsigned i = 0; i < 50; ++i) strm << " "; - printf(strm.str().c_str()); - fflush(stdout); - ); - push(l, c_fixed_truth); - trail.push_back(l); - SASSERT(inconsistent() || !is_unsat()); - } - } - lbool lookahead::search() { m_model.reset(); scoped_level _sl(*this, c_fixed_truth); @@ -1770,19 +1738,73 @@ namespace sat { } TRACE("sat", tout << "choose: " << l << " " << trail << "\n";); ++m_stats.m_decisions; - IF_VERBOSE(1, printf("\r"); - std::stringstream strm; - strm << pp_prefix(m_prefix, m_trail_lim.size()); - for (unsigned i = 0; i < 50; ++i) strm << " "; - printf(strm.str().c_str()); - fflush(stdout); - ); + IF_VERBOSE(1, display_search_string();); push(l, c_fixed_truth); trail.push_back(l); SASSERT(inconsistent() || !is_unsat()); } } + bool lookahead::backtrack(literal_vector& trail, svector & is_decision) { + while (inconsistent()) { + if (trail.empty()) return false; + if (is_decision.back()) { + pop(); + trail.back().neg(); + assign(trail.back()); + is_decision.back() = false; + propagate(); + } + else { + trail.pop_back(); + is_decision.pop_back(); + } + } + return true; + } + + lbool lookahead::cube() { + lbool result = l_false; + init_search(); + m_model.reset(); + scoped_level _sl(*this, c_fixed_truth); + literal_vector cube; + svector is_decision; + m_search_mode = lookahead_mode::searching; + double freevars_threshold = 0; + while (true) { + TRACE("sat", display(tout);); + inc_istamp(); + checkpoint(); + literal l = choose(); + if (inconsistent()) { + TRACE("sat", tout << "inconsistent: " << cube << "\n";); + freevars_threshold = m_freevars.size(); + if (!backtrack(cube, is_decision)) return result; + continue; + } + if (l == null_literal) { + return l_true; + } + unsigned depth = cube.size(); + if ((m_config.m_cube_cutoff != 0 && depth == m_config.m_cube_cutoff) || + (m_config.m_cube_cutoff == 0 && m_freevars.size() < freevars_threshold)) { + display_cube(std::cout, cube); + freevars_threshold *= (1.0 - pow(m_config.m_cube_fraction, depth)); + result = l_undef; + set_conflict(); + if (!backtrack(cube, is_decision)) return result; + continue; + } + TRACE("sat", tout << "choose: " << l << " cube: " << cube << "\n";); + ++m_stats.m_decisions; + push(l, c_fixed_truth); + cube.push_back(l); + is_decision.push_back(true); + SASSERT(inconsistent() || !is_unsat()); + } + } + void lookahead::init_model() { m_model.reset(); for (unsigned i = 0; i < m_num_vars; ++i) { @@ -1801,12 +1823,12 @@ namespace sat { } } - std::ostream& lookahead::display_cube(std::ostream& out) const { + std::ostream& lookahead::display_cube(std::ostream& out, literal_vector const& cube) const { out << "c"; - for (literal l : m_assumptions) { + for (literal l : cube) { out << " " << ~l; } - return out << "\n"; + return out << " 0\n"; } std::ostream& lookahead::display_binary(std::ostream& out) const { diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index 0bd6e39d4..609f72a51 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -444,13 +444,15 @@ namespace sat { void assign(literal l); void propagated(literal l); bool backtrack(literal_vector& trail); + bool backtrack(literal_vector& trail, svector & is_decision); lbool search(); void init_model(); std::ostream& display_binary(std::ostream& out) const; std::ostream& display_clauses(std::ostream& out) const; std::ostream& display_values(std::ostream& out) const; std::ostream& display_lookahead(std::ostream& out) const; - std::ostream& display_cube(std::ostream& out) const; + std::ostream& display_cube(std::ostream& out, literal_vector const& cube) const; + void display_search_string(); void init_search(); void checkpoint(); @@ -486,7 +488,7 @@ namespace sat { If cut-depth != 0, then it is used to control the depth of cuts. Otherwise, cut-fraction gives an adaptive threshold for creating cuts. */ - void cube(); + lbool cube(); literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars); /** diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 5e054bdaf..f0a423491 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -857,8 +857,7 @@ namespace sat { return lookahead_search(); } if (m_config.m_lookahead_cube && num_lits == 0) { - lookahead_cube(); - return l_undef; + return lookahead_cube(); } if (m_config.m_local_search) { return do_local_search(num_lits, lits); @@ -952,16 +951,18 @@ namespace sat { return r; } - void solver::lookahead_cube() { + lbool solver::lookahead_cube() { lookahead lh(*this); + lbool r = l_undef; try { - lh.cube(); + r = lh.cube(); } catch (z3_exception&) { lh.collect_statistics(m_aux_stats); throw; } lh.collect_statistics(m_aux_stats); + return r; } lbool solver::lookahead_search() { diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index ab2dd7a1f..581f557a7 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -403,7 +403,7 @@ namespace sat { void exchange_par(); lbool check_par(unsigned num_lits, literal const* lits); lbool lookahead_search(); - void lookahead_cube(); + lbool lookahead_cube(); lbool do_local_search(unsigned num_lits, literal const* lits); lbool do_ccc();