Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

port sample cell projection #7333

Merged
merged 12 commits into from
Aug 11, 2024
Merged

port sample cell projection #7333

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
bb842d3
port sample cell projection
levnach Aug 2, 2024
3dfcfae
cleaning up
levnach Aug 6, 2024
43a6b4b
port look for 0 witness
levnach Aug 7, 2024
14ff13f
remove option look_for_0_witness
levnach Aug 7, 2024
a599f55
cleanup porting comments
levnach Aug 7, 2024
4336764
port more from hybridSMT
levnach Aug 8, 2024
460c346
port hybridSMT
levnach Aug 8, 2024
b5f74b1
fix the build
levnach Aug 8, 2024
f0f2ceb
remove printouts
levnach Aug 9, 2024
8ba2667
delete unused nlsat_symmetry_checker
levnach Aug 9, 2024
9a33630
cleanup
levnach Aug 9, 2024
9dc9de1
cleanup
levnach Aug 11, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion src/nlsat/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,9 @@ z3_add_component(nlsat
nlsat_simplify.cpp
nlsat_solver.cpp
nlsat_types.cpp
COMPONENT_DEPENDENCIES
nlsat_simple_checker.cpp
nlsat_variable_ordering_strategy.cpp
COMPONENT_DEPENDENCIES
polynomial
sat
PYG_FILES
Expand Down
244 changes: 223 additions & 21 deletions src/nlsat/nlsat_explain.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,8 @@ namespace nlsat {
bool m_minimize_cores;
bool m_factor;
bool m_signed_project;
bool m_cell_sample;


struct todo_set {
polynomial::cache & m_cache;
Expand Down Expand Up @@ -130,7 +132,7 @@ namespace nlsat {
evaluator & m_evaluator;

imp(solver & s, assignment const & x2v, polynomial::cache & u, atom_vector const & atoms, atom_vector const & x2eq,
evaluator & ev):
evaluator & ev, bool is_sample):
m_solver(s),
m_assignment(x2v),
m_atoms(atoms),
Expand All @@ -148,6 +150,9 @@ namespace nlsat {
m_core1(s),
m_core2(s),
m_result(nullptr),

m_cell_sample(is_sample),

m_evaluator(ev) {
m_simplify_cores = false;
m_full_dimensional = false;
Expand Down Expand Up @@ -646,6 +651,45 @@ namespace nlsat {
m_todo.insert(p);
}
}

void add_sample_coeff(polynomial_ref_vector &ps, var x){
polynomial_ref p(m_pm);
polynomial_ref lc(m_pm);
unsigned sz = ps.size();
for (unsigned i = 0; i < sz; i++){
p = ps.get(i);
unsigned k = degree(p, x);
SASSERT(k > 0);
TRACE("nlsat_explain", tout << "add_lc, x: "; display_var(tout, x); tout << "\nk: " << k << "\n"; display(tout, p); tout << "\n";);
for(; k > 0; k--){
lc = m_pm.coeff(p, x, k);
add_factors(lc);
if (m_pm.nonzero_const_coeff(p, x, k)){
TRACE("nlsat_explain", tout << "constant coefficient, skipping...\n";);
break;
}
}
SASSERT(sign(lc) != 0);
SASSERT(!is_const(lc));
}
}

void psc_resultant_sample(polynomial_ref_vector &ps, var x, polynomial_ref_vector & samples){
polynomial_ref p(m_pm);
polynomial_ref q(m_pm);
SASSERT(samples.size() <= 2);

for (unsigned i = 0; i < ps.size(); i++){
p = ps.get(i);
for (unsigned j = 0; j < samples.size(); j++){
q = samples.get(j);
if (!m_pm.eq(p, q)) {
psc(p, q, x);
}
}
}
}


/**
\brief Add leading coefficients of the polynomials in ps.
Expand Down Expand Up @@ -689,7 +733,6 @@ namespace nlsat {
bool have_zero = false;
for (unsigned i = 0; i < num_factors; i++) {
f = m_factors.get(i);
// std::cout << "f=";display(std::cout, f) << "\n";
if (coeffs_are_zeroes_in_factor(f)) {
have_zero = true;
break;
Expand Down Expand Up @@ -973,6 +1016,92 @@ namespace nlsat {
add_simple_assumption(k, p, lsign);
}

void cac_add_cell_lits(polynomial_ref_vector & ps, var y, polynomial_ref_vector & res) {
res.reset();
SASSERT(m_assignment.is_assigned(y));
bool lower_inf = true;
bool upper_inf = true;
scoped_anum_vector & roots = m_roots_tmp;
scoped_anum lower(m_am);
scoped_anum upper(m_am);
anum const & y_val = m_assignment.value(y);
TRACE("nlsat_explain", tout << "adding literals for "; display_var(tout, y); tout << " -> ";
m_am.display_decimal(tout, y_val); tout << "\n";);
polynomial_ref p_lower(m_pm);
unsigned i_lower = UINT_MAX;
polynomial_ref p_upper(m_pm);
unsigned i_upper = UINT_MAX;
polynomial_ref p(m_pm);
unsigned sz = ps.size();
for (unsigned k = 0; k < sz; k++) {
p = ps.get(k);
if (max_var(p) != y)
continue;
roots.reset();
// Variable y is assigned in m_assignment. We must temporarily unassign it.
// Otherwise, the isolate_roots procedure will assume p is a constant polynomial.
m_am.isolate_roots(p, undef_var_assignment(m_assignment, y), roots);
unsigned num_roots = roots.size();
bool all_lt = true;
for (unsigned i = 0; i < num_roots; i++) {
int s = m_am.compare(y_val, roots[i]);
TRACE("nlsat_explain",
m_am.display_decimal(tout << "comparing root: ", roots[i]); tout << "\n";
m_am.display_decimal(tout << "with y_val:", y_val);
tout << "\nsign " << s << "\n";
tout << "poly: " << p << "\n";
);
if (s == 0) {
// y_val == roots[i]
// add literal
// ! (y = root_i(p))
add_root_literal(atom::ROOT_EQ, y, i+1, p);
res.push_back(p);
return;
}
else if (s < 0) {
// y_val < roots[i]
if (i > 0) {
// y_val > roots[j]
int j = i - 1;
if (lower_inf || m_am.lt(lower, roots[j])) {
lower_inf = false;
m_am.set(lower, roots[j]);
p_lower = p;
i_lower = j + 1;
}
}
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;
}
all_lt = false;
break;
}
}
if (all_lt && num_roots > 0) {
int j = num_roots - 1;
if (lower_inf || m_am.lt(lower, roots[j])) {
lower_inf = false;
m_am.set(lower, roots[j]);
p_lower = p;
i_lower = j + 1;
}
}
}

if (!lower_inf) {
res.push_back(p_lower);
add_root_literal(m_full_dimensional ? atom::ROOT_GE : atom::ROOT_GT, y, i_lower, p_lower);
}
if (!upper_inf) {
res.push_back(p_upper);
add_root_literal(m_full_dimensional ? atom::ROOT_LE : atom::ROOT_LT, y, i_upper, p_upper);
}
}

/**
Add one or two literals that specify in which cell of variable y the current interpretation is.
One literal is added for the cases:
Expand Down Expand Up @@ -1016,6 +1145,7 @@ namespace nlsat {
// Otherwise, the isolate_roots procedure will assume p is a constant polynomial.
m_am.isolate_roots(p, undef_var_assignment(m_assignment, y), roots);
unsigned num_roots = roots.size();
bool all_lt = true;
for (unsigned i = 0; i < num_roots; i++) {
int s = m_am.compare(y_val, roots[i]);
TRACE("nlsat_explain",
Expand All @@ -1033,25 +1163,33 @@ namespace nlsat {
}
else if (s < 0) {
// y_val < roots[i]

// check if roots[i] is a better upper bound
if (i > 0) {
// y_val > roots[j]
int j = i - 1;
if (lower_inf || m_am.lt(lower, roots[j])) {
lower_inf = false;
m_am.set(lower, roots[j]);
p_lower = p;
i_lower = j + 1;
}
}
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;
i_upper = i + 1;
}
all_lt = false;
break;
}
else if (s > 0) {
// roots[i] < y_val

// check if roots[i] is a better lower bound
if (lower_inf || m_am.lt(lower, roots[i])) {
lower_inf = false;
m_am.set(lower, roots[i]);
p_lower = p;
i_lower = i+1;
}
}
if (all_lt && num_roots > 0) {
int j = num_roots - 1;
if (lower_inf || m_am.lt(lower, roots[j])) {
lower_inf = false;
m_am.set(lower, roots[j]);
p_lower = p;
i_lower = j + 1;
}
}
}
Expand All @@ -1064,6 +1202,7 @@ namespace nlsat {
}
}


/**
\brief Return true if all polynomials in ps are univariate in x.
*/
Expand All @@ -1082,7 +1221,8 @@ namespace nlsat {
/**
\brief Apply model-based projection operation defined in our paper.
*/
void project(polynomial_ref_vector & ps, var max_x) {

void project_original(polynomial_ref_vector & ps, var max_x) {
if (ps.empty())
return;
m_todo.reset();
Expand All @@ -1094,12 +1234,12 @@ namespace nlsat {
if (x < max_x)
add_cell_lits(ps, x);
while (true) {
TRACE("nlsat_explain", tout << "project loop, processing var "; display_var(tout, x); tout << "\npolynomials\n";
display(tout, ps); tout << "\n";);
if (all_univ(ps, x) && m_todo.empty()) {
m_todo.reset();
break;
}
TRACE("nlsat_explain", tout << "project loop, processing var "; display_var(tout, x); tout << "\npolynomials\n";
display(tout, ps); tout << "\n";);
add_lc(ps, x);
psc_discriminant(ps, x);
psc_resultant(ps, x);
Expand All @@ -1110,6 +1250,68 @@ namespace nlsat {
}
}

/**
* Sample Projection
* Reference:
* Haokun Li and Bican Xia.
* "Solving Satisfiability of Polynomial Formulas By Sample - Cell Projection"
* https://arxiv.org/abs/2003.00409
*/
void project_cdcac(polynomial_ref_vector & ps, var max_x) {
if (ps.empty())
return;
bool first = true;
m_todo.reset();
for (poly* p : ps) {
m_todo.insert(p);
}
var x = m_todo.remove_max_polys(ps);
// Remark: after vanishing coefficients are eliminated, ps may not contain max_x anymore

polynomial_ref_vector samples(m_pm);


if (x < max_x){
cac_add_cell_lits(ps, x, samples);
}

while (true) {
if (all_univ(ps, x) && m_todo.empty()) {
m_todo.reset();
break;
}
TRACE("nlsat_explain", tout << "project loop, processing var "; display_var(tout, x); tout << "\npolynomials\n";
display(tout, ps); tout << "\n";);

if (first) {
add_lc(ps, x);
psc_discriminant(ps, x);
psc_resultant(ps, x);
first = false;
}
else {
add_lc(ps, x);
// add_sample_coeff(ps, x);
psc_discriminant(ps, x);
psc_resultant_sample(ps, x, samples);
}

if (m_todo.empty())
break;
x = m_todo.remove_max_polys(ps);
cac_add_cell_lits(ps, x, samples);
}
}

void project(polynomial_ref_vector & ps, var max_x) {
if (m_cell_sample) {
project_cdcac(ps, max_x);
}
else {
project_original(ps, max_x);
}
}

bool check_already_added() const {
for (bool b : m_already_added_literal) {
(void)b;
Expand Down Expand Up @@ -1474,7 +1676,7 @@ namespace nlsat {
var max_x = max_var(m_ps);
TRACE("nlsat_explain", tout << "polynomials in the conflict:\n"; display(tout, m_ps); tout << "\n";);
elim_vanishing(m_ps);
TRACE("nlsat_explain", tout << "elim vanishing x" << max_x << "\n"; display(tout, m_ps); tout << "\n";);
TRACE("nlsat_explain", tout << "elim vanishing\n"; display(tout, m_ps); tout << "\n";);
project(m_ps, max_x);
TRACE("nlsat_explain", tout << "after projection\n"; display(tout, m_ps); tout << "\n";);
}
Expand Down Expand Up @@ -1936,8 +2138,8 @@ namespace nlsat {
};

explain::explain(solver & s, assignment const & x2v, polynomial::cache & u,
atom_vector const& atoms, atom_vector const& x2eq, evaluator & ev) {
m_imp = alloc(imp, s, x2v, u, atoms, x2eq, ev);
atom_vector const& atoms, atom_vector const& x2eq, evaluator & ev, bool use_cell_sample) {
m_imp = alloc(imp, s, x2v, u, atoms, x2eq, ev, use_cell_sample);
}

explain::~explain() {
Expand Down
3 changes: 2 additions & 1 deletion src/nlsat/nlsat_explain.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,8 @@ namespace nlsat {
imp * m_imp;
public:
explain(solver & s, assignment const & x2v, polynomial::cache & u,
atom_vector const& atoms, atom_vector const& x2eq, evaluator & ev);
atom_vector const& atoms, atom_vector const& x2eq, evaluator & ev, bool use_cell_sample_proj);

~explain();

void reset();
Expand Down
Loading
Loading