Unit propagation on monomials #6905
Conversation
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
src/math/lp/lp_bound_propagator.h
Outdated
|
|
||
| T& m_imp; | ||
| vector<implied_bound> m_ibounds; | ||
| std::vector<implied_bound, my_allocator<implied_bound>> m_ibounds; |
There was a problem hiding this comment.
I will be moving this as a general definition to util/vector in a separate pull request.
src/math/lp/lp_bound_propagator.h
Outdated
| @@ -86,76 +122,248 @@ class lp_bound_propagator { | |||
| public: | |||
| lp_bound_propagator(T& imp) : m_imp(imp) {} | |||
|
|
|||
| const vector<implied_bound>& ibounds() const { return m_ibounds; } | |||
| const std::vector<implied_bound, my_allocator<implied_bound>>& ibounds() const { return m_ibounds; } | |||
There was a problem hiding this comment.
this is why it deserves a stand-alone typedef or sub-class.
src/smt/theory_lra.cpp
Outdated
| return; | ||
|
|
||
| m_bp.init(); | ||
| propagate_bounds_for_touched_monomials(); |
There was a problem hiding this comment.
I don't see where the bounds found by nlp monomials are propagated to LP. The bounds are "just" imposed on existing literals. We didn't have a way to propagate the resulting bounds on to the LP tableau. The problem, of course, is that this kind of bounds propagation is fragile with respect to convergence. So it has to be throttled or has to use detection of propagation loops. Dealing with this properly requires more than a simple code change.
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
src/smt/theory_arith_nl.h
Outdated
| @@ -511,6 +511,7 @@ bool theory_arith<Ext>::propagate_nl_downward(expr * n, var_power_pair const& p) | |||
| */ | |||
| template<typename Ext> | |||
| bool theory_arith<Ext>::propagate_nl_bounds(expr * m) { | |||
| return false; | |||
There was a problem hiding this comment.
this should not be part of pull request
src/math/lp/nla_core.cpp
Outdated
| const auto& vars = m_emons[monic_var].vars(); | ||
| if (!is_linear(vars, zero_var, non_fixed)) | ||
| return; | ||
| if (throttle) |
There was a problem hiding this comment.
this looks really strange to me: what is the case where you don't want to throttle?
Once a monomial is linear it is either fixed or has a single non-fixed variable. The single non-fixed variable times the values of the fixed variables is equal to the variable of the monomial.
The monomial is no longer representing a non-linear sub-term. Strengthening bounds doesn't make it more linear. Whatever information comes from stronger bounds at this point should be captured by what got propagated.
src/math/lp/nla_core.cpp
Outdated
| for (auto v : vars) | ||
| if (v != non_fixed) { | ||
| k *= val(v); | ||
| if (k.is_big()) return; |
There was a problem hiding this comment.
why do you throttle on is_big()?
There is no such throttling for arith.solver=2
src/math/lp/nla_core.cpp
Outdated
| bool is_strict; | ||
| auto& lps = lra; | ||
|
|
||
| if (lower_bound_is_available(non_fixed)) { |
There was a problem hiding this comment.
why is this so involved and yet not adding equalities to the tableau?
The equality should be that monic_var = k*non_fixed explained by dependencies for the fixed variables in vars.
src/math/lp/nla_core.cpp
Outdated
| } | ||
| } | ||
|
|
||
| bool core::lower_bound_is_available(unsigned j) const { |
There was a problem hiding this comment.
this one now has two implementations.
Neither appear to be the right place, which would be lar_solver since bounds are maintained there. This is not specific to non-linear
There was a problem hiding this comment.
how are these functions related to column_has_upper/lower_bound in lp_core_solver_base.h, and re-exposed from lar_solver?
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
No description provided.