From 4b4e8cbc6ed7c77e2bb06778bf6cae3eb8a40811 Mon Sep 17 00:00:00 2001 From: ValentinPromies <44966217+ValentinPromies@users.noreply.github.com> Date: Wed, 20 Aug 2025 16:36:35 +0200 Subject: [PATCH] Nl2lin (#7795) * add linearized projection in nlsat * implement nlsat check for given assignment * add some comments --- src/nlsat/nlsat_explain.cpp | 212 +++++++++++++++++++++++++++++++++++- src/nlsat/nlsat_explain.h | 1 + src/nlsat/nlsat_solver.cpp | 61 ++++++++++- 3 files changed, 272 insertions(+), 2 deletions(-) diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 92a0428a2..19c6316d5 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -45,6 +45,7 @@ namespace nlsat { bool m_minimize_cores; bool m_factor; bool m_signed_project; + bool m_linear_project; bool m_cell_sample; @@ -155,6 +156,7 @@ namespace nlsat { m_full_dimensional = false; m_minimize_cores = false; m_signed_project = false; + m_linear_project = false; } std::ostream& display(std::ostream & out, polynomial_ref const & p) const { @@ -1262,8 +1264,212 @@ namespace nlsat { } } + + /** + * \brief add cell literals for the linearized projection and categorize the polynomials in ps + * - ps_below will contain all polynomials from ps which have a root below m_assignment w.r.t. x + * - ps_above will contain all polynomials from ps which have a root above m_assignment w.r.t. x + * - ps_equal will contain at least one polynomial from ps which have a root equal to m_assignment + * - In addition, they may contain additional linear polynomials added as cell boundaries + * - The back elements of ps_below, ps_above, ps_equal are the polynomials used for the cell literals + */ + void add_cell_lits_linear(polynomial_ref_vector const& ps, + var const x, + polynomial_ref_vector& ps_below, + polynomial_ref_vector& ps_above, + polynomial_ref_vector& ps_equal) { + ps_below.reset(); + ps_above.reset(); + ps_equal.reset(); + + SASSERT(m_assignment.is_assigned(x)); + anum const & x_val = m_assignment.value(x); + + bool lower_inf = true, upper_inf = true; + scoped_anum lower(m_am), upper(m_am); + polynomial_ref p_lower(m_pm), p_upper(m_pm); + unsigned i_lower = UINT_MAX, i_upper = UINT_MAX; + + scoped_anum_vector & roots = m_roots_tmp; + polynomial_ref p(m_pm); + + unsigned sz = ps.size(); + for (unsigned k = 0; k < sz; k++) { + p = ps.get(k); + if (max_var(p) != x) + continue; + roots.reset(); + + // Temporarily unassign x, s.t. isolate_roots does not assume p as constant. + m_am.isolate_roots(p, undef_var_assignment(m_assignment, x), roots); + unsigned num_roots = roots.size(); + if (num_roots == 0) continue; + + // find p's smallest root above the sample + unsigned i = 0; + int s = 1; + for (; i < num_roots; ++i) { + s = m_am.compare(x_val, roots[i]); + if (s <= 0) break; + } + + if (s == 0) { + // roots[i] == x_val + ps_equal.push_back(p); + p_lower = p; + i_lower = i+1; + break; // TODO: choose the best among multiple section polynomials? + } else if (s < 0) { + // x_val < roots[i] + ps_above.push_back(p); + if (upper_inf || m_am.lt(roots[i], upper)) { + upper_inf = false; + m_am.set(upper, roots[i]); + p_upper = p; + i_upper = i + 1; + } + } + // in any case, roots[i-1] might provide a lower bound if it exists + if (i > 0) { + // roots[i-1] < x_val + ps_below.push_back(p); + if (lower_inf || m_am.lt(lower, roots[i-1])) { + lower_inf = false; + m_am.set(lower, roots[i-1]); + p_lower = p; + i_lower = i; + } + } + } + + // add linear cell bounds + + if (!ps_equal.empty()) { + if (!m_am.is_rational(x_val)) { + // TODO: FAIL + NOT_IMPLEMENTED_YET(); + } else if (m_pm.total_degree(p_lower) > 1) { + rational bound; + m_am.to_rational(x_val, bound); + p_lower = m_pm.mk_polynomial(x); + p_lower = p_lower - bound; + } + add_root_literal(atom::ROOT_EQ, x, 1, p_lower); + // make sure bounding poly is at the back of the vector + ps_equal.push_back(p_lower); + return; + } + if (!lower_inf) { + bool approximate = (m_pm.total_degree(p_lower) > 1); + if (approximate) { + scoped_anum between(m_am); + m_am.select(lower, x_val, between); + rational new_bound; + m_am.to_rational(between, new_bound); + p_lower = m_pm.mk_polynomial(x); + p_lower = p_lower - new_bound; + } + add_root_literal((approximate || m_full_dimensional) ? atom::ROOT_GE : atom::ROOT_GT, x, 1, p_lower); + // make sure bounding poly is at the back of the vector + ps_below.push_back(p_lower); + } + if (!upper_inf) { + bool approximate = (m_pm.total_degree(p_upper) > 1); + if (approximate) { + scoped_anum between(m_am); + m_am.select(x_val, upper, between); + rational new_bound; + m_am.to_rational(between, new_bound); + p_upper = m_pm.mk_polynomial(x); + p_upper = p_upper - new_bound; + } + add_root_literal((approximate || m_full_dimensional) ? atom::ROOT_LE : atom::ROOT_LT, x, 1, p_upper); + // make sure bounding poly is at the back of the vector + ps_below.push_back(p_upper); + } + } + + + /** + * \brief compute the resultants of p with each polynomial in ps w.r.t. x + */ + void psc_resultants_with(polynomial_ref_vector const& ps, polynomial_ref p, var const x) { + polynomial_ref q(m_pm); + unsigned sz = ps.size(); + for (unsigned i = 0; i < sz; i++) { + q = ps.get(i); + if (q == p) continue; + psc(p, q, x); + } + } + + + /** + * Linearized projection based on: + * Valentin Promies, Jasper Nalbach, Erika Abraham and Paul Wagner + * "More is Less: Adding Polynomials for Faster Explanations in NLSAT" + * in CADE30, 2025 + */ + void project_linear(polynomial_ref_vector & ps, var max_x) { + if (ps.empty()) + return; + m_todo.reset(); + for (poly* p : ps) { + m_todo.insert(p); + } + + polynomial_ref_vector ps_below_sample(m_pm); + polynomial_ref_vector ps_above_sample(m_pm); + polynomial_ref_vector ps_equal_sample(m_pm); + var x = m_todo.extract_max_polys(ps); + if (x == max_x) { + // top level projection like original + // we could also do a covering-style projection, sparing some resultants + add_lcs(ps, x); + psc_discriminant(ps, x); + psc_resultant(ps, x); + x = m_todo.extract_max_polys(ps); + } + + while(!m_todo.empty()) { + add_cell_lits_linear(ps, x, ps_below_sample, ps_above_sample, ps_equal_sample); + if (all_univ(ps, x) && m_todo.empty()) { + m_todo.reset(); + break; + } + add_lcs(ps, x); + psc_discriminant(ps, x); + polynomial_ref lb(m_pm); + polynomial_ref ub(m_pm); + + if (!ps_equal_sample.empty()) { + // section + lb = ps_equal_sample.back(); + psc_resultants_with(ps, lb, x); + } else { + if (!ps_below_sample.empty()) { + lb = ps_below_sample.back(); + psc_resultants_with(ps_below_sample, lb, x); + } + if (!ps_above_sample.empty()) { + ub = ps_above_sample.back(); + psc_resultants_with(ps_above_sample, ub, x); + if (!ps_below_sample.empty()) { + // also need resultant between bounds + psc(lb, ub, x); + } + } + } + x = m_todo.extract_max_polys(ps); + } + } + + void project(polynomial_ref_vector & ps, var max_x) { - if (m_cell_sample) { + if (m_linear_project) { + project_linear(ps, max_x); + } + else if (m_cell_sample) { project_cdcac(ps, max_x); } else { @@ -2126,6 +2332,10 @@ namespace nlsat { m_imp->m_signed_project = f; } + void explain::set_linear_project(bool f) { + m_imp->m_linear_project = f; + } + void explain::main_operator(unsigned n, literal const * ls, scoped_literal_vector & result) { (*m_imp)(n, ls, result); } diff --git a/src/nlsat/nlsat_explain.h b/src/nlsat/nlsat_explain.h index 6e1cf091b..316a1367e 100644 --- a/src/nlsat/nlsat_explain.h +++ b/src/nlsat/nlsat_explain.h @@ -45,6 +45,7 @@ namespace nlsat { void set_minimize_cores(bool f); void set_factor(bool f); void set_signed_project(bool f); + void set_linear_project(bool f); /** \brief Given a set of literals ls[0], ... ls[n-1] s.t. diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index ed4e50c38..34109578c 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -2035,7 +2035,66 @@ namespace nlsat { } lbool check(assignment const& rvalues, atom_vector& core) { - return l_undef; + // temporarily set m_assignment to the given one + assignment tmp = m_assignment; + m_assignment.reset(); + m_assignment.copy(rvalues); + + // check whether the asserted atoms are satisfied by rvalues + literal best_literal = null_literal; + unsigned sz = m_clauses.size(); + lbool satisfied = l_true; + for (unsigned i = 0; i < sz; i++) { + bool c_satisfied = false; + clause const & c = *(m_clauses[i]); + for (literal l : c) { + if (const_cast(this)->value(l) != l_false) { + c_satisfied = true; + break; + } + } + if (c_satisfied) continue; + + // take best literal from c + for (literal l : c) { + if (best_literal == null_literal) { + best_literal = l; + } else { + bool_var b_best = best_literal.var(); + bool_var b_l = l.var(); + if (degree(m_atoms[b_l]) < degree(m_atoms[b_best])) { + best_literal = l; + } + // TODO: there might be better criteria than just the degree in the main variable. + } + } + } + + if (satisfied == l_true) { + // nothing to do + return l_true; + } + if (satisfied == l_undef) { + // nothing to do? + return l_undef; + } + + // assignment does not satisfy the constraints -> create lemma + SASSERT(best_literal != null_literal); + m_lazy_clause.reset(); + m_explain.set_linear_project(true); + m_explain.main_operator(1, &best_literal, m_lazy_clause); + m_explain.set_linear_project(false); // TODO: there should be a better way to control this. + m_lazy_clause.push_back(~best_literal); + + core.clear(); + for (literal l : m_lazy_clause) { + core.push_back(m_atoms[l.var()]); + } + + m_assignment.reset(); + m_assignment.copy(tmp); + return l_false; } lbool check(literal_vector& assumptions) {