mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-20 17:14:43 +00:00
Code Activity

Add dynamic heuristic selection for levelwise projection

Browse source 
Implement weight-based dynamic selection of projection heuristics in
levelwise CAD. The weight function w(p, level) = deg(p, level) estimates
projection complexity, with w(res(a,b)) ≈ w(a) + w(b).

At each level, all three heuristics (biggest_cell, chain, lowest_degree)
are evaluated and the one with minimum estimated resultant weight is
selected. When fewer than 2 root functions exist, the default heuristic
is used since all produce equivalent results.

Add parameter nlsat.lws_dynamic_heuristic (default: true) to enable or
disable dynamic selection. When disabled, the static heuristic from
lws_sector_rel_mode/lws_section_rel_mode is used.

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
This commit is contained in:
Lev Nachmanson 2026-01-17 19:20:19 -10:00
parent 18553c8288
commit 5727e1d040
4 changed files with 251 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/nlsat/nlsat_solver.cpp
View file

@ -252,6 +252,7 @@ namespace nlsat {
unsigned m_lws_relation_mode = 1;
unsigned m_lws_sector_relation_mode = 1;
unsigned m_lws_section_relation_mode = 1;
bool m_lws_dynamic_heuristic = true;
imp(solver& s, ctx& c):
m_ctx(c),
m_solver(s),
@ -317,6 +318,7 @@ namespace nlsat {
unsigned lws_section_rel_mode = p.lws_section_rel_mode();
m_lws_sector_relation_mode = (lws_sector_rel_mode == UINT_MAX) ? m_lws_relation_mode : lws_sector_rel_mode;
m_lws_section_relation_mode = (lws_section_rel_mode == UINT_MAX) ? m_lws_relation_mode : lws_section_rel_mode;
m_lws_dynamic_heuristic = p.lws_dynamic_heuristic();
m_check_lemmas |= !(m_debug_known_solution_file_name.empty());
m_cell_sample = p.cell_sample();
@ -4653,5 +4655,6 @@ namespace nlsat {
unsigned solver::lws_section_relation_mode() const { return m_imp->m_lws_section_relation_mode; }
bool solver::lws_dynamic_heuristic() const { return m_imp->m_lws_dynamic_heuristic; }
};