From 9314ad3808b488a9a9ec051f6b2373ccb82ed2ac Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 1 Feb 2023 10:36:49 +0100 Subject: [PATCH 1/6] minor changes to bounds propagation --- src/math/polysat/saturation.cpp | 23 ++++++++++++++++------- 1 file changed, 16 insertions(+), 7 deletions(-) diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp index b842ce7a8..b0138bd01 100644 --- a/src/math/polysat/saturation.cpp +++ b/src/math/polysat/saturation.cpp @@ -1596,8 +1596,7 @@ namespace polysat { } /** - * if !x_split: update d such that 0 <= a*x*y0 + b*x + c*y0 + d < M for every value x_min <= x <= x_max - * if x_split: update d such that -M < a*x*y0 + b*x + c*y0 + d < M for every value x_min <= x <= x_max, return x_split such that [x_min,x_split[ and [x_split,x_max] can fit into [0,M[ + * Update d such that -M < a*x*y0 + b*x + c*y0 + d < M for every value x_min <= x <= x_max, return x_split such that [x_min,x_split[ and [x_split,x_max] can fit into [0,M[ * return false if there is no such d. */ bool saturation::adjust_bound(rational const& x_min, rational const& x_max, rational const& y0, rational const& M, rational const& a, rational const& b, rational const& c, rational& d, rational* x_split) { @@ -1610,14 +1609,22 @@ namespace polysat { if (max - min >= M) return false; + // k0 = min k. val + kM >= 0 + // = min k. k >= -val/M + // = ceil(-val/M) = -floor(val/M) rational offset = rational::zero(); +#if 0 if (max >= M) offset = -M * floor(max / M); else if (max < 0) offset = M * floor((-max + M - 1) / M); +#else + if (max < 0 || max >= M) + offset = -M * floor(max / M); +#endif d += offset; - // If min + offset < 0, then [min,max] contained a multiple of M. + // If min + offset < 0, then [min,max] contains a multiple of M. if (min + offset < 0) { if (!x_split) return false; @@ -1731,11 +1738,12 @@ namespace polysat { VERIFY(x_min <= x_max); - // TODO: d +/- M would suffice here rational d1 = dd1; + if (a1*x_min*y0 + b1*x_min + c1*y0 + d1 < 0) + d1 += M; rational d2 = dd2; - VERIFY(adjust_bound(x_min, x_max, y0, M, a1, b1, c1, d1, nullptr)); - VERIFY(adjust_bound(x_min, x_max, y0, M, a2, b2, c2, d2, nullptr)); + if (a2*x_min*y0 + b2*x_min + c2*y0 + d2 < 0) + d2 += M; IF_VERBOSE(2, verbose_stream() << "Adjusted for x in [" << x_min << "; " << x_max << "]\n"; @@ -1833,8 +1841,8 @@ namespace polysat { verbose_stream() << "\n---\n\n"; verbose_stream() << "constraint " << lit_pp(s, a_l_b) << "\n"; verbose_stream() << "x = v" << x << "\n"; - s.m_viable.display(verbose_stream(), x) << "\n"; verbose_stream() << "y = v" << y << "\n"; + s.m_viable.display(verbose_stream() << "\nx-intervals:\n", x, "\n") << "\n"; verbose_stream() << "\n"; verbose_stream() << "x_min " << x_min << " x_max " << x_max << "\n"; verbose_stream() << "v" << y << " " << y0 << "\n"; @@ -1851,6 +1859,7 @@ namespace polysat { if (x_sp1 > x_sp2) std::swap(x_sp1, x_sp2); + SASSERT(x_min <= x_sp1 && x_sp1 <= x_sp2 && x_sp2 <= x_max); IF_VERBOSE(2, verbose_stream() << "Adjusted\n"; From 3c822117d16399fcd2364e6cd2a1e131dc170d29 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 1 Feb 2023 10:41:02 +0100 Subject: [PATCH 2/6] assert before deref --- src/math/polysat/conflict.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index 85084acf8..1c0b7ed45 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -303,15 +303,15 @@ namespace polysat { } void conflict::add_lemma(char const* name, clause_ref lemma) { + if (!name) + name = ""; + LOG_H3("Lemma " << name << ": " << show_deref(lemma)); + VERIFY(lemma); for (auto lit : *lemma) if (s.m_bvars.is_true(lit)) verbose_stream() << "REDUNDANT lemma " << lit << " : " << show_deref(lemma) << "\n"; - if (!name) - name = ""; - LOG_H3("Lemma " << name << ": " << show_deref(lemma)); - SASSERT(lemma); s.m_simplify_clause.apply(*lemma); lemma->set_redundant(true); lemma->set_name(name); From 1bb68a4fc126528017c8e296292e834d59087455 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 1 Feb 2023 10:47:26 +0100 Subject: [PATCH 3/6] track dependency of base-level conflict --- src/math/polysat/conflict.cpp | 7 +++++-- src/math/polysat/conflict.h | 3 ++- src/math/polysat/solver.cpp | 6 ++---- src/math/polysat/solver.h | 2 +- 4 files changed, 10 insertions(+), 8 deletions(-) diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index 1c0b7ed45..d9ebe3ebf 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -158,6 +158,7 @@ namespace polysat { SASSERT(m_vars_occurring.empty()); SASSERT(m_lemmas.empty()); SASSERT(m_narrow_queue.empty()); + SASSERT(m_dep.is_null()); } return is_empty; } @@ -170,6 +171,7 @@ namespace polysat { m_lemmas.reset(); m_narrow_queue.reset(); m_level = UINT_MAX; + m_dep = null_dependency; SASSERT(empty()); } @@ -181,10 +183,11 @@ namespace polysat { return contains(lit) || contains(~lit); } - void conflict::init_at_base_level() { + void conflict::init_at_base_level(dependency dep) { SASSERT(empty()); SASSERT(s.at_base_level()); m_level = s.m_level; + m_dep = dep; SASSERT(!empty()); // TODO: logger().begin_conflict??? // TODO: check uses of logger().begin_conflict(). sometimes we call it before adding constraints, sometimes after... @@ -434,7 +437,7 @@ namespace polysat { clause_builder lemma(s); - for (auto c : *this) + for (signed_constraint c : *this) lemma.insert(~c); for (unsigned v : m_vars) { diff --git a/src/math/polysat/conflict.h b/src/math/polysat/conflict.h index affdb4ba7..ccb1ee448 100644 --- a/src/math/polysat/conflict.h +++ b/src/math/polysat/conflict.h @@ -101,6 +101,7 @@ namespace polysat { // Level at which the conflict was discovered unsigned m_level = UINT_MAX; + dependency m_dep = null_dependency; public: conflict(solver& s); @@ -126,7 +127,7 @@ namespace polysat { bool is_relevant(sat::literal lit) const; /** conflict due to obvious input inconsistency */ - void init_at_base_level(); + void init_at_base_level(dependency dep); /** conflict because the constraint c is false under current variable assignment */ void init(signed_constraint c); /** boolean conflict with the given clause */ diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 43707e395..042cb390e 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -158,8 +158,7 @@ namespace polysat { case l_false: // Input literal contradicts current boolean state (e.g., opposite literals in the input) // => conflict only flags the inconsistency - set_conflict_at_base_level(); - SASSERT(dep == null_dependency && "track dependencies is TODO"); + set_conflict_at_base_level(dep); return; case l_true: // constraint c is already asserted => ignore @@ -174,8 +173,7 @@ namespace polysat { case l_false: // asserted an always-false constraint => conflict at base level LOG("Always false: " << c); - set_conflict_at_base_level(); - SASSERT(dep == null_dependency && "track dependencies is TODO"); + set_conflict_at_base_level(dep); return; case l_true: // asserted an always-true constraint => ignore diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index cf31c2c6e..d6931e665 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -253,7 +253,7 @@ namespace polysat { void erase_pwatch(pvar v, constraint* c); void erase_pwatch(constraint* c); - void set_conflict_at_base_level() { m_conflict.init_at_base_level(); } + void set_conflict_at_base_level(dependency dep) { m_conflict.init_at_base_level(dep); } void set_conflict(signed_constraint c) { m_conflict.init(c); } void set_conflict(clause& cl) { m_conflict.init(cl); } void set_conflict_by_viable_interval(pvar v) { m_conflict.init_by_viable_interval(v); } From 576e0b70b266fe8e21fd64d9104f6f5f20a194f0 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 1 Feb 2023 10:53:49 +0100 Subject: [PATCH 4/6] stub for conflict::find_deps --- src/math/polysat/conflict.cpp | 21 +++++++++++++++++++++ src/math/polysat/conflict.h | 2 ++ src/math/polysat/solver.cpp | 9 ++------- 3 files changed, 25 insertions(+), 7 deletions(-) diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index d9ebe3ebf..4ccab9f07 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -504,6 +504,27 @@ namespace polysat { } #endif + void conflict::find_deps(dependency_vector& out_deps) const { + sat::literal_vector todo; + sat::literal_set done; + indexed_uint_set deps; + + LOG("conflict: " << *this); + + // TODO: starting at literals/variables in the conflict, chase propagations backwards and accumulate dependencies. + verbose_stream() << "WARNING: unsat_core requested but dependency tracking in polysat is TODO\n"; + for (signed_constraint c : *this) { + dependency d = s.m_bvars.dep(c.blit()); + if (!d.is_null()) + deps.insert(d.val()); + } + + for (unsigned d : deps) + out_deps.push_back(dependency(d)); + if (!m_dep.is_null()) + out_deps.push_back(m_dep); + } + std::ostream& conflict::display(std::ostream& out) const { char const* sep = ""; for (auto c : *this) diff --git a/src/math/polysat/conflict.h b/src/math/polysat/conflict.h index ccb1ee448..958b7993b 100644 --- a/src/math/polysat/conflict.h +++ b/src/math/polysat/conflict.h @@ -195,6 +195,8 @@ namespace polysat { /** Move the literals to be narrowed out of the conflict */ sat::literal_vector take_narrow_queue(); + void find_deps(dependency_vector& out_deps) const; + std::ostream& display(std::ostream& out) const; }; diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 042cb390e..774f15793 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -1318,14 +1318,9 @@ namespace polysat { } void solver::unsat_core(dependency_vector& deps) { - verbose_stream() << "WARNING: unsat_core requested but dependency tracking in polysat is TODO\n"; + VERIFY(is_conflict()); deps.reset(); - LOG("conflict" << m_conflict); - for (auto c : m_conflict) { - auto d = m_bvars.dep(c.blit()); - if (d != null_dependency) - deps.push_back(d); - } + m_conflict.find_deps(deps); } std::ostream& solver::display(std::ostream& out) const { From f0625b604acadab9d94e264a5013dc14ecb396f3 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 1 Feb 2023 11:12:13 +0100 Subject: [PATCH 5/6] Promote assertions to release mode --- src/math/polysat/solver.cpp | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 774f15793..91e7d7edb 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -723,9 +723,7 @@ namespace polysat { /// Verify the value we're trying to assign against the univariate solver void solver::assign_verify(pvar v, rational val, justification j) { SASSERT(j.is_decision() || j.is_propagation()); -#ifndef NDEBUG unsigned const old_size = m_search.size(); -#endif signed_constraint c; clause_ref lemma; { @@ -746,8 +744,8 @@ namespace polysat { LOG("Produced lemma: " << show_deref(lemma)); } } - SASSERT(m_search.size() == old_size); - SASSERT(!m_search.get_assignment().contains(v)); + VERIFY_EQ(m_search.size(), old_size); + VERIFY(!m_search.get_assignment().contains(v)); if (lemma) { add_clause(*lemma); if (is_conflict()) { From 975fb252219890cd159f53e0c243cfc721608617 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 1 Feb 2023 11:17:29 +0100 Subject: [PATCH 6/6] Fix to bench15 bug was unsound --- src/math/polysat/solver.cpp | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 91e7d7edb..c581d3e1f 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -1174,7 +1174,18 @@ namespace polysat { LOG((clause.is_redundant() ? "Lemma: ": "Aux: ") << clause); for (sat::literal lit : clause) { LOG(" " << lit_pp(*this, lit)); - // SASSERT(m_bvars.value(lit) != l_true); + if (!m_bvars.is_assigned(lit)) { + switch (lit2cnstr(lit).eval(*this)) { + case l_true: + assign_eval(lit); + break; + case l_false: + assign_eval(~lit); + break; + default: + break; + } + } // it could be that such a literal has been created previously but we don't detect it when e.g. narrowing a mul_ovfl_constraint if (m_bvars.value(lit) == l_true) { // in this case the clause is useless @@ -1225,7 +1236,7 @@ namespace polysat { clause_ref solver::mk_clause(unsigned n, signed_constraint const* cs, bool is_redundant) { clause_builder cb(*this); for (unsigned i = 0; i < n; ++i) - cb.insert_try_eval(cs[i]); + cb.insert(cs[i]); cb.set_redundant(is_redundant); return cb.build(); }