From a216bee64779f8a7100b8a890f73178490544c03 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 29 Sep 2020 03:29:33 -0700 Subject: [PATCH] updated notes, fixes to dual solver --- src/ast/euf/euf_egraph.cpp | 78 +++++++++++++++++++++------------ src/math/lp/int_gcd_test.cpp | 38 ++++++++++++---- src/sat/smt/sat_dual_solver.cpp | 29 ++++++------ src/sat/smt/sat_dual_solver.h | 9 ++-- src/util/lim_vector.h | 42 ++++++++++++++++++ 5 files changed, 142 insertions(+), 54 deletions(-) create mode 100644 src/util/lim_vector.h diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index 6963079f5..f99ba6486 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -19,36 +19,63 @@ Each node has a congruence closure root, cg. cg is set to the representative in the cc table (first insertion of congruent node). Each node n has a set of parents, denoted n.P. +The table maintains the invariant + - p.cg = find(p) -set r2 to the root of r1: +Merge sets r2 to the root of r1 +(r2 and r1 are both considered roots before the merge). +The operation Unmerge reverses the effect of Merge. -Merge: Erase: - for each p r1.P such that p.cg == p: - erase from table - Update root: - r1.root := r2 - Insert: - for each p in r1.P: + +Merge(r1, r2) +------------- + +Erase: for each p in r1.P such that p.cg == p: + erase from table +Update root: r1.root := r2 +Insert: for each p in r1.P: p.cg = insert p in table if p.cg == p: append p to r2.P else - add p.cg, p to worklist + add (p.cg == p) to 'to_merge' -Unmerge: Erase: - for each p in added nodes: - erase p from table - Revert root: - r1.root := r1 - Insert: - for each p in r1.P: - insert p if n was cc root before merge +Unmerge(r1, r2) +--------------- + +Erase: for each p in r2.P added from r1.P: + erase p from table +Revert root: r1.root := r1 +Insert: for each p in r1.P: + insert p if n was cc root before merge condition for being cc root before merge: - p->cg == p - congruent(p, p->cg) + p.cg == p or !congruent(p, p.cg) -congruent(p,q) := roots of p.children = roots of q.children +congruent(p,q) := roots of p.args = roots of q.args + +The algorithm orients r1, r2 such that class_size(r1) <= class_size(r2). +With N nodes, there can be at most N calls to Merge. +Each of the calls traverse r1.P from the smaller class size. +Label a merge tree with nodes from the larger class size. +In other words, if Merge(r2,r1); Merge(r3,r1) is a sequence +of calls where r1 is selected root, then the merge tree is + + r1 + / \ + r1 r3 + \ + r2 + +Note that parent lists are re-examined only for nodes that join +from right subtrees (with lesser class sizes). +Claim: a node participates in a path along right adjoining sub-trees at most O(log(N)) times. +Justification (very roughly): the size of a right adjoining subtree can at most +be equal to the left adjoining sub-tree. This entails a logarithmic number of +re-examinations from the right adjoining tree. +(TBD check how Hopcroft's main argument is phrased) + +The parent lists are bounded by the maximal arity of functions. Example: @@ -491,14 +518,9 @@ namespace euf { bool egraph::propagate() { SASSERT(m_new_lits_qhead <= m_new_lits.size()); SASSERT(m_num_scopes == 0 || m_to_merge.empty()); - unsigned head = 0, tail = m_to_merge.size(); - while (head < tail && m.limit().inc() && !inconsistent()) { - for (unsigned i = head; i < tail && !inconsistent(); ++i) { - auto const& w = m_to_merge[i]; - merge(w.a, w.b, justification::congruence(w.commutativity)); - } - head = tail; - tail = m_to_merge.size(); + for (unsigned i = 0; i < m_to_merge.size() && m_limit().inc() && !inconsistent(); ++i) { + auto const& w = m_to_merge[i]; + merge(w.a, w.b, justification::congruence(w.commutativity)); } m_to_merge.reset(); force_push(); diff --git a/src/math/lp/int_gcd_test.cpp b/src/math/lp/int_gcd_test.cpp index 049acc7c0..a590f712c 100644 --- a/src/math/lp/int_gcd_test.cpp +++ b/src/math/lp/int_gcd_test.cpp @@ -13,7 +13,35 @@ Author: Nikolaj Bjorner (nbjorner) Lev Nachmanson (levnach) -Revision History: +Notes: + +Basic: + For each row a*x + b = 0, where fixed variables are replaced by b, + check if gcd(a) divides b + +Extended: + For each row a*x + b*y + c = 0, where + - the coefficients in a are all the same and smaller than the coefficients in b + - the variables x are bounded + Let l := a*lb(x), u := a*ub(x) + - that is the lower and upper bounds for a*x based on the bounds for x. + let ll := ceil (l / gcd(b,c)) + uu := floor (u / gcd(b,c)) + If uu > ll, there is no space to find solutions for x within the bounds + +Accumulative: + For each row a*x + b*y - c = 0, where |a| = 1 < |b|, and x is a single variable, + (it could also be a group of variables) accumulate constraint x = c mod b + + If there are row gcd constraints, such that + - x = c1 mod b1, from rows R1 + - x = c2 mod b2, from rows R2 + + - If c1 mod gcd(b1,b2) != c2 mod gcd(b1,b2) report conflict for the rows involved. + + - Otherwise accumulate x = (c1 * lcm(b1,b2) / b2) + (c2 * lcm(b1,b2) / b1) mod lcm(b,b2) + and accumulate the rows from R1, R2 + --*/ #include "math/lp/int_solver.h" @@ -28,15 +56,7 @@ namespace lp { if (!lia.settings().int_run_gcd_test()) return false; -#if 1 return true; -#else - if (m_delay == 0) { - return true; - } - --m_delay; - return false; -#endif } lia_move int_gcd_test::operator()() { diff --git a/src/sat/smt/sat_dual_solver.cpp b/src/sat/smt/sat_dual_solver.cpp index e80bb0301..e473a4a00 100644 --- a/src/sat/smt/sat_dual_solver.cpp +++ b/src/sat/smt/sat_dual_solver.cpp @@ -24,22 +24,19 @@ namespace sat { void dual_solver::push() { m_solver.user_push(); - m_roots_lim.push_back(m_roots.size()); - m_tracked_lim.push_back(m_tracked_stack.size()); - m_units_lim.push_back(m_units.size()); + m_roots.push_scope(); + m_tracked_vars.push_scope(); + m_units.push_scope(); } void dual_solver::pop(unsigned num_scopes) { m_solver.user_pop(num_scopes); - unsigned old_sz = m_roots_lim.size() - num_scopes; - for (unsigned v = m_tracked_stack.size(); v-- > m_tracked_lim[old_sz]; ) - m_is_tracked[v] = false; - m_roots.shrink(m_roots_lim[old_sz]); - m_tracked_stack.shrink(m_tracked_lim[old_sz]); - m_units.shrink(m_units_lim[old_sz]); - m_roots_lim.shrink(old_sz); - m_tracked_lim.shrink(old_sz); - m_units_lim.shrink(old_sz); + unsigned old_sz = m_tracked_vars.old_size(num_scopes); + for (unsigned i = m_tracked_vars.size(); i-- > old_sz; ) + m_is_tracked[m_tracked_vars[i]] = false; + m_units.pop_scope(num_scopes); + m_roots.pop_scope(num_scopes); + m_tracked_vars.pop_scope(num_scopes); } bool_var dual_solver::ext2var(bool_var v) { @@ -56,7 +53,7 @@ namespace sat { v = ext2var(v); if (!m_is_tracked.get(v, false)) { m_is_tracked.setx(v, true, false); - m_tracked_stack.push_back(v); + m_tracked_vars.push_back(v); } } @@ -69,6 +66,10 @@ namespace sat { } void dual_solver::add_root(unsigned sz, literal const* clause) { + if (sz == 1) { + m_units.push_back(clause[0]); + return; + } literal root(m_solver.mk_var(), false); for (unsigned i = 0; i < sz; ++i) m_solver.mk_clause(root, ~ext2lit(clause[i]), status::input()); @@ -86,7 +87,7 @@ namespace sat { m_solver.user_push(); m_solver.add_clause(m_roots.size(), m_roots.c_ptr(), status::input()); m_lits.reset(); - for (bool_var v : m_tracked_stack) + for (bool_var v : m_tracked_vars) m_lits.push_back(literal(v, l_false == s.value(m_var2ext[v]))); lbool is_sat = m_solver.check(m_lits.size(), m_lits.c_ptr()); m_core.reset(); diff --git a/src/sat/smt/sat_dual_solver.h b/src/sat/smt/sat_dual_solver.h index 4133dfeb3..8dc9e0826 100644 --- a/src/sat/smt/sat_dual_solver.h +++ b/src/sat/smt/sat_dual_solver.h @@ -8,6 +8,8 @@ Module Name: Abstract: Solver for obtaining implicant. + Based on an idea by Armin Biere to use dual propagation + for representation of negated goal. Author: @@ -15,18 +17,19 @@ Author: --*/ #pragma once +#include "util/lim_vector.h" #include "sat/sat_solver.h" namespace sat { class dual_solver { solver m_solver; - literal_vector m_roots, m_lits, m_core, m_units; + lim_svector m_units, m_roots; + lim_svector m_tracked_vars; + literal_vector m_lits, m_core; bool_var_vector m_is_tracked; - unsigned_vector m_tracked_stack; unsigned_vector m_ext2var; unsigned_vector m_var2ext; - unsigned_vector m_roots_lim, m_tracked_lim, m_units_lim; void add_literal(literal lit); bool_var ext2var(bool_var v); diff --git a/src/util/lim_vector.h b/src/util/lim_vector.h new file mode 100644 index 000000000..24a4a3f0b --- /dev/null +++ b/src/util/lim_vector.h @@ -0,0 +1,42 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + lim_vector.h + +Abstract: + + Vector that restores during backtracking. + +Author: + + Nikolaj Bjorner (nbjorner) 2020-29-09 + +--*/ +#pragma once + +#include "util/vector.h" + +template +class lim_svector : public svector { + unsigned_vector m_lim; +public: + lim_svector() {} + + void push_scope() { + m_lim.push_back(size()); + } + + void pop_scope(unsigned num_scopes) { + SASSERT(num_scopes > 0); + unsigned old_sz = m_lim.size() - num_scopes; + shrink(m_lim[old_sz]); + m_lim.shrink(old_sz); + } + + unsigned num_scopes() const { return m_lim.size(); } + + unsigned old_size(unsigned n) const { return m_lim[m_lim.size() - n]; } +}; +