From eca250933df23dbc170c49df91c813c8327c8a6d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 1 Feb 2018 19:56:01 -0800 Subject: [PATCH] disable uhle from lookahead solver Signed-off-by: Nikolaj Bjorner --- src/opt/opt_parse.cpp | 229 ++++++++++++++++++++++++++++++----- src/sat/sat_asymm_branch.cpp | 34 +----- src/sat/sat_asymm_branch.h | 2 - src/sat/sat_big.cpp | 4 +- src/sat/sat_big.h | 2 +- src/sat/sat_config.cpp | 1 - src/sat/sat_config.h | 1 - src/sat/sat_lookahead.cpp | 29 +---- src/sat/sat_lookahead.h | 2 - src/sat/sat_params.pyg | 1 - src/sat/sat_scc.cpp | 2 +- src/sat/sat_simplifier.cpp | 2 +- 12 files changed, 213 insertions(+), 96 deletions(-) diff --git a/src/opt/opt_parse.cpp b/src/opt/opt_parse.cpp index 2cba7561f..6a7ea3614 100644 --- a/src/opt/opt_parse.cpp +++ b/src/opt/opt_parse.cpp @@ -36,40 +36,36 @@ public: void next() { m_val = m_stream.get(); } bool eof() const { return ch() == EOF; } unsigned line() const { return m_line; } - void skip_whitespace(); - void skip_space(); - void skip_line(); + void skip_whitespace() { + while ((ch() >= 9 && ch() <= 13) || ch() == 32) { + if (ch() == 10) ++m_line; + next(); + } + } + void skip_space() { + while (ch() != 10 && ((ch() >= 9 && ch() <= 13) || ch() == 32)) + next(); + } + void skip_line() { + while(true) { + if (eof()) { + return; + } + if (ch() == '\n') { + ++m_line; + next(); + return; + } + next(); + } + } bool parse_token(char const* token); int parse_int(); unsigned parse_unsigned(); }; -void opt_stream_buffer::skip_whitespace() { - while ((ch() >= 9 && ch() <= 13) || ch() == 32) { - if (ch() == 10) ++m_line; - next(); - } -} -void opt_stream_buffer::skip_space() { - while (ch() != 10 && ((ch() >= 9 && ch() <= 13) || ch() == 32)) { - next(); - } -} -void opt_stream_buffer::skip_line() { - while(true) { - if (eof()) { - return; - } - if (ch() == '\n') { - ++m_line; - next(); - return; - } - next(); - } -} bool opt_stream_buffer::parse_token(char const* token) { skip_whitespace(); @@ -314,4 +310,183 @@ void parse_opb(opt::context& opt, std::istream& is, unsigned_vector& h) { opb.parse(); } +#if 0 +class lp_stream_buffer : opt_stream_buffer { +public: + lp_stream_buffer(std::istream & s): + opt_stream_buffer(s) + {} + + char lower(char c) { + return ('A' <= c && c <= 'Z') ? c - 'A' + 'a' : c; + } + + bool parse_token_nocase(char const* token) { + skip_whitespace(); + char const* t = token; + while (lower(ch()) == *t) { + next(); + ++t; + } + return 0 == *t; + } +}; + + +class lp_tokenizer { + opt_stream_buffer& in; +public: + lp_tokenizer(opt_stream_buffer& in): + in(in) + {} + +}; + +class lp_parse { + opt::context& opt; + lp_tokenizer& tok; +public: + lp_parse(opt::context& opt, lp_stream_buffer& in): opt(opt), tok(is) {} + + void parse() { + objective(); + subject_to(); + bounds(); + general(); + binary(); + } + + void objective() { + m_objective.m_is_max = minmax(); + m_objective.m_name = try_name(); + m_objective.m_expr = expr(); + } + + bool minmax() { + if (try_accept("minimize")) + return false; + if (try_accept("min")) + return false; + if (try_accept("maximize")) + return true; + if (try_accept("max")) + return true; + error("expected min or max objective"); + return false; + } + + bool try_accept(char const* token) { + return false; + } + + bool indicator(symbol& var, bool& val) { + if (!try_variable(var)) return false; + check(in.parse_token("=")); + + } + + + def indicator(self): + v = self.variable() + self.accept("=") + val = self.try_accept("1") + if val is None: + val = self.accept("0") + self.accept("->") + return (var, val) + + def try_indicator(self): + try: + return self.indicator() + with: + return None + + def constraints(self): + return [c for c in self._constraints()] + + def _constraints(self): + while True: + c = self.try_constraint() + if c in None: + return + yield c + + def try_constraint(self): + try: + return self.constraint() + except: + return None + + def constraint(self): + name = self.try_label() + guard = self.try_guard() + e = self.expr() + op = self.relation() + rhs = self.numeral() + return (name, guard, e, ops, rhs) + + def expr(self): + return [t for t in self.terms()] + + def terms(self): + while True: + t = self.term() + if t is None: + return None + yield t + + def term(self): + sign = self.sign() + coeff = self.coeff() + v = self.variable() + return (sign*coeff, v) + + def sign(self): + if self.try_accept("-"): + return -1 + return 1 + + def coeff(self): + tok = self.peek() + if tok is int: + self.next() + return (int) tok + return 1 + + def relation(self): + if self.try_accept("<="): + return "<=" + if self.try_accept(">="): + return ">=" + if self.try_accept("=<"): + return "<=" + if self.try_accept("=>"): + return ">=" + if self.try_accept("="): + return "=" + return None + + def subject_to(self): + if self.accept("subject") and self.accept("to"): + return + if self.accept("such") and self.accept("that"): + return + if self.accept("st"): + return + if self.accept("s"): + self.try_accept(".") + self.accept("t") + self.accept(".") + return + + +}; + +void parse_lp(opt::context& opt, std::istream& is) { + lp_stream_buffer _is(is); + lp_parse lp(opt, _is); + lp.parse(); +} + +#endif diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index b05de55e6..a94ea461a 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -150,27 +150,6 @@ namespace sat { } } - void asymm_branch::operator()(big& big) { - s.propagate(false); - if (s.m_inconsistent) - return; - report rpt(*this); - - for (unsigned i = 0; i < m_asymm_branch_rounds; ++i) { - unsigned elim = m_elim_literals; - big.reinit(); - process(&big, s.m_clauses); - process(&big, s.m_learned); - process_bin(big); - unsigned num_elim = m_elim_literals - elim; - IF_VERBOSE(1, verbose_stream() << "(sat-asymm-branch-step :elim " << num_elim << ")\n";); - if (num_elim == 0) - break; - if (num_elim > 1000) - i = 0; - } - s.propagate(false); - } void asymm_branch::operator()(bool force) { ++m_calls; @@ -196,11 +175,11 @@ namespace sat { ++counter; change = false; if (m_asymm_branch_sampled) { - big big(s.m_rand, true); + big big(s.m_rand); if (process(big, true)) change = true; } if (m_asymm_branch_sampled) { - big big(s.m_rand, false); + big big(s.m_rand); if (process(big, false)) change = true; } if (m_asymm_branch) { @@ -431,11 +410,10 @@ namespace sat { bool asymm_branch::process_sampled(big& big, clause & c) { scoped_detach scoped_d(s, c); sort(big, c); - if (!big.learned() && !c.is_learned() && uhte(big, c)) { - // TBD: mark clause as learned. - ++m_hidden_tautologies; - scoped_d.del_clause(); - return false; + if (uhte(big, c)) { + // don't touch hidden tautologies. + // ATE takes care of them. + return true; } return uhle(scoped_d, big, c); } diff --git a/src/sat/sat_asymm_branch.h b/src/sat/sat_asymm_branch.h index fb8048c37..1a57f8800 100644 --- a/src/sat/sat_asymm_branch.h +++ b/src/sat/sat_asymm_branch.h @@ -91,8 +91,6 @@ namespace sat { void operator()(bool force); - void operator()(big& big); - void updt_params(params_ref const & p); static void collect_param_descrs(param_descrs & d); diff --git a/src/sat/sat_big.cpp b/src/sat/sat_big.cpp index b35930e96..9c2bef50e 100644 --- a/src/sat/sat_big.cpp +++ b/src/sat/sat_big.cpp @@ -21,9 +21,8 @@ Revision History: namespace sat { - big::big(random_gen& rand, bool binary): + big::big(random_gen& rand): m_rand(rand) { - m_binary = binary; } void big::init(solver& s, bool learned) { @@ -141,7 +140,6 @@ namespace sat { } unsigned big::reduce_tr(solver& s) { - if (!m_binary && learned()) return 0; unsigned num_lits = s.num_vars() * 2; unsigned idx = 0; unsigned elim = 0; diff --git a/src/sat/sat_big.h b/src/sat/sat_big.h index 8477ad186..cb3466d26 100644 --- a/src/sat/sat_big.h +++ b/src/sat/sat_big.h @@ -41,7 +41,7 @@ namespace sat { public: - big(random_gen& rand, bool binary); + big(random_gen& rand); /** \brief initialize a BIG from a solver. */ diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index c3352797e..e2cbf0e3c 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -76,7 +76,6 @@ namespace sat { m_unit_walk_threads = p.unit_walk_threads(); m_lookahead_simplify = p.lookahead_simplify(); m_lookahead_simplify_bca = p.lookahead_simplify_bca(); - m_lookahead_simplify_asymm_branch = p.lookahead_simplify_asymm_branch(); if (p.lookahead_reward() == symbol("heule_schur")) m_lookahead_reward = heule_schur_reward; else if (p.lookahead_reward() == symbol("heuleu")) diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index e64c0c544..d70ae0cb7 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -94,7 +94,6 @@ namespace sat { bool m_unit_walk; bool m_lookahead_simplify; bool m_lookahead_simplify_bca; - bool m_lookahead_simplify_asymm_branch; cutoff_t m_lookahead_cube_cutoff; double m_lookahead_cube_fraction; unsigned m_lookahead_cube_depth; diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 5bf3a194d..804f06341 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -2306,16 +2306,12 @@ namespace sat { roots[v] = p; VERIFY(get_parent(p) == p); VERIFY(get_parent(~p) == ~p); - IF_VERBOSE(0, verbose_stream() << p << " " << q << "\n";); } } IF_VERBOSE(1, verbose_stream() << "(sat-lookahead :equivalences " << to_elim.size() << ")\n";); elim_eqs elim(m_s); elim(roots, to_elim); - if (get_config().m_lookahead_simplify_asymm_branch) { - big_asymm_branch(learned); - } if (learned && get_config().m_lookahead_simplify_bca) { add_hyper_binary(); } @@ -2324,29 +2320,6 @@ namespace sat { m_lookahead.reset(); } - /** - \brief extract binary implication graph from learned binary clauses and use it - for strengthening clauses. - */ - - void lookahead::big_asymm_branch(bool learned) { - unsigned num_lits = m_s.num_vars() * 2; - unsigned idx = 0; - big big(m_s.m_rand, false); - big.init_adding_edges(m_s.num_vars(), learned); - for (auto const& lits : m_binary) { - literal u = get_parent(to_literal(idx++)); - if (u == null_literal) continue; - for (literal v : lits) { - v = get_parent(v); - if (v != null_literal) - big.add_edge(u, v); - } - } - big.done_adding_edges(); - asymm_branch ab(m_s, m_s.m_params); - ab(big); - } /** \brief reduction based on binary implication graph @@ -2372,7 +2345,7 @@ namespace sat { } } - big big(m_s.m_rand, false); + big big(m_s.m_rand); big.init(m_s, true); svector> candidates; diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index 794d868f1..a37f32a1b 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -555,8 +555,6 @@ namespace sat { void add_hyper_binary(); - void big_asymm_branch(bool learned); - double psat_heur(); public: diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 3630365d6..c702941f6 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -51,7 +51,6 @@ def_module_params('sat', ('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'), ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'), ('lookahead_simplify.bca', BOOL, True, 'add learned binary clauses as part of lookahead simplification'), - ('lookahead_simplify.asymm_branch', BOOL, True, 'apply asymmetric branch simplification with lookahead simplifier'), ('lookahead.global_autarky', BOOL, False, 'prefer to branch on variables that occur in clauses that are reduced'), ('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu'))) diff --git a/src/sat/sat_scc.cpp b/src/sat/sat_scc.cpp index 484cb93ff..3010c92f2 100644 --- a/src/sat/sat_scc.cpp +++ b/src/sat/sat_scc.cpp @@ -27,7 +27,7 @@ namespace sat { scc::scc(solver & s, params_ref const & p): m_solver(s), - m_big(s.m_rand, true) { + m_big(s.m_rand) { reset_statistics(); updt_params(p); } diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 831539351..f439036b2 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -214,7 +214,7 @@ namespace sat { } register_clauses(s.m_clauses); - if (bce_enabled() || bca_enabled() || ate_enabled()) { + if (!learned && (bce_enabled() || bca_enabled() || ate_enabled())) { elim_blocked_clauses(); }