Nl2lin (#7795)

* add linearized projection in nlsat

* implement nlsat check for given assignment

* add some comments

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);
     }

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.

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<imp*>(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) {