mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-15 06:01:27 +00:00
Code Activity

fix some bugs and the PQ approach is working for now. the depth sets approach is actually unsound, but I am going to focus on the PQ approach for now since it has more potential for SAT problems with the right hardness metric

Browse source
This commit is contained in:
Ilana Shapiro 2025-08-31 18:49:14 -07:00
parent c2c0194f3f
commit 7af7ba6495
2 changed files with 17 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

40
src/smt/smt_parallel.cpp
View file

@ -57,16 +57,17 @@ namespace smt {
b.set_exception("context cancelled");
return;
}
LOG_WORKER(1, " checking cube: " << mk_bounded_pp(mk_and(cube), m, 3) << " max-conflicts " << m_config.m_threads_max_conflicts << "\n");
unsigned conflicts_before = ctx->m_stats.m_num_conflicts;
unsigned propagations_before = ctx->m_stats.m_num_propagations + ctx->m_stats.m_num_bin_propagations;
unsigned decisions_before = ctx->m_stats.m_num_decisions;
unsigned restarts_before = ctx->m_stats.m_num_restarts;
LOG_WORKER(1, " checking cube\n");
lbool r = check_cube(cube);
if (m.limit().is_canceled()) {
LOG_WORKER(1, " context cancelled\n");
return;
}
switch (r) {
case l_undef: {
if (m.limit().is_canceled())
break;
LOG_WORKER(1, " found undef cube\n");
// return unprocessed cubes to the batch manager
// add a split literal to the batch manager.
@ -76,24 +77,14 @@ namespace smt {
returned_cubes.push_back(cube);
auto split_atoms = get_split_atoms();
if (m_config.m_iterative_deepening) {
unsigned conflicts_before = ctx->m_stats.m_num_conflicts;
unsigned propagations_before = ctx->m_stats.m_num_propagations + ctx->m_stats.m_num_bin_propagations;
unsigned decisions_before = ctx->m_stats.m_num_decisions;
unsigned restarts_before = ctx->m_stats.m_num_restarts;
lbool r = check_cube(cube);
unsigned conflicts_after = ctx->m_stats.m_num_conflicts;
unsigned propagations_after = ctx->m_stats.m_num_propagations + ctx->m_stats.m_num_bin_propagations;
unsigned decisions_after = ctx->m_stats.m_num_decisions;
unsigned restarts_after = ctx->m_stats.m_num_restarts;
LOG_WORKER(1, " CUBING\n");
if (m_config.m_iterative_deepening || m_config.m_beam_search) { // let's automatically do iterative deepening for beam search
LOG_WORKER(1, " applying iterative deepening\n");
// per-cube deltas
unsigned conflicts_delta = conflicts_after - conflicts_before;
unsigned propagations_delta = propagations_after - propagations_before;
unsigned decisions_delta = decisions_after - decisions_before;
unsigned restarts_delta = restarts_after - restarts_before;
unsigned conflicts_delta = ctx->m_stats.m_num_conflicts - conflicts_before;
unsigned propagations_delta = (ctx->m_stats.m_num_propagations + ctx->m_stats.m_num_bin_propagations) - propagations_before;
unsigned decisions_delta = ctx->m_stats.m_num_decisions - decisions_before;
unsigned restarts_delta = ctx->m_stats.m_num_restarts - restarts_before;
LOG_WORKER(1, " cube deltas: conflicts: " << conflicts_delta << " propagations: " << propagations_delta << " decisions: " << decisions_delta << " restarts: " << restarts_delta << "\n");
// tuned experimentally
@ -194,6 +185,7 @@ namespace smt {
m_config.m_num_split_lits = pp.num_split_lits();
m_config.m_backbone_detection = pp.backbone_detection();
m_config.m_iterative_deepening = pp.iterative_deepening();
m_config.m_beam_search = pp.beam_search();
// don't share initial units
ctx->pop_to_base_lvl();

1
src/smt/smt_parallel.h
View file

@ -164,6 +164,7 @@ namespace smt {
unsigned m_num_split_lits = 2;
bool m_backbone_detection = false;
bool m_iterative_deepening = false;
bool m_beam_search = false;
};
unsigned id; // unique identifier for the worker