mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-26 07:43:41 +00:00
Code Activity

adding ability to ahve multiple local search threads

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-03-06 10:48:58 -08:00
parent fda5809c89
commit cd4a2701db
4 changed files with 29 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/sat_config.cpp
View file

@ -36,8 +36,7 @@ namespace sat {
m_glue_psm("glue_psm"), m_glue_psm("glue_psm"),
m_psm_glue("psm_glue") { m_psm_glue("psm_glue") {
m_num_threads = 1; m_num_threads = 1;
m_local_search = false; m_local_search = 0;
m_local_search_parameter1 = 0;
updt_params(p); updt_params(p);
} }
@ -82,7 +81,6 @@ namespace sat {
m_max_conflicts = p.max_conflicts(); m_max_conflicts = p.max_conflicts();
m_num_threads = p.threads(); m_num_threads = p.threads();
m_local_search = p.local_search(); m_local_search = p.local_search();
m_local_search_parameter1 = p.local_search_int();
// These parameters are not exposed // These parameters are not exposed
m_simplify_mult1 = _p.get_uint("simplify_mult1", 300); m_simplify_mult1 = _p.get_uint("simplify_mult1", 300);

3
src/sat/sat_config.h
View file

@ -58,8 +58,7 @@ namespace sat {
unsigned m_burst_search; unsigned m_burst_search;
unsigned m_max_conflicts; unsigned m_max_conflicts;
unsigned m_num_threads; unsigned m_num_threads;
bool m_local_search; unsigned m_local_search;
unsigned m_local_search_parameter1;
unsigned m_simplify_mult1; unsigned m_simplify_mult1;
double m_simplify_mult2; double m_simplify_mult2;

3
src/sat/sat_params.pyg
View file

@ -28,6 +28,5 @@ def_module_params('sat',
('drat.check', BOOL, False, 'build up internal proof and check'), ('drat.check', BOOL, False, 'build up internal proof and check'),
('cardinality.solver', BOOL, False, 'use cardinality solver'), ('cardinality.solver', BOOL, False, 'use cardinality solver'),
('xor.solver', BOOL, False, 'use xor solver'), ('xor.solver', BOOL, False, 'use xor solver'),
('local_search', BOOL, False, 'add local search co-processor to find satisfiable solution'), ('local_search', UINT, 0, 'number of local search threads to find satisfiable solution'),
('local_search.int', UINT, 0, 'arbitrary integer'),
)) ))

46
src/sat/sat_solver.cpp
View file

@ -21,6 +21,7 @@ Revision History:
#include"luby.h" #include"luby.h"
#include"trace.h" #include"trace.h"
#include"max_cliques.h" #include"max_cliques.h"
#include"scoped_ptr_vector.h"
// define to update glue during propagation // define to update glue during propagation
#define UPDATE_GLUE #define UPDATE_GLUE
@ -782,7 +783,7 @@ namespace sat {
pop_to_base_level(); pop_to_base_level();
IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver)\n";); IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver)\n";);
SASSERT(at_base_lvl()); SASSERT(at_base_lvl());
if ((m_config.m_num_threads > 1 || m_config.m_local_search) && !m_par) { if ((m_config.m_num_threads > 1 || m_config.m_local_search > 0) && !m_par) {
return check_par(num_lits, lits); return check_par(num_lits, lits);
} }
flet<bool> _searching(m_searching, true); flet<bool> _searching(m_searching, true);
@ -856,17 +857,20 @@ namespace sat {
lbool solver::check_par(unsigned num_lits, literal const* lits) { lbool solver::check_par(unsigned num_lits, literal const* lits) {
bool use_local_search = m_config.m_local_search; scoped_ptr_vector<local_search> ls;
scoped_ptr<local_search> ls; int num_threads = static_cast<int>(m_config.m_num_threads + m_config.m_local_search);
if (use_local_search) { int num_extra_solvers = m_config.m_num_threads - 1;
ls = alloc(local_search); int num_local_search = static_cast<int>(m_config.m_local_search);
ls->config().set_seed(m_config.m_random_seed); for (int i = 0; i < num_local_search; ++i) {
ls->import(*this, false); local_search* l = alloc(local_search);
l->config().set_seed(m_config.m_random_seed);
l->import(*this, false);
ls.push_back(l);
} }
int num_threads = static_cast<int>(m_config.m_num_threads) + (use_local_search ? 1 : 0);
int num_extra_solvers = num_threads - 1 - (use_local_search ? 1 : 0);
#define IS_LOCAL_SEARCH(i) i == num_extra_solvers && use_local_search #define IS_AUX_SOLVER(i) (0 <= i && i < num_extra_solvers)
#define IS_LOCAL_SEARCH(i) (num_extra_solvers <= i && i + 1 < num_threads)
#define IS_MAIN_SOLVER(i) (i + 1 == num_threads)
sat::parallel par(*this); sat::parallel par(*this);
par.reserve(num_threads, 1 << 12); par.reserve(num_threads, 1 << 12);
@ -881,11 +885,11 @@ namespace sat {
for (int i = 0; i < num_threads; ++i) { for (int i = 0; i < num_threads; ++i) {
try { try {
lbool r = l_undef; lbool r = l_undef;
if (i < num_extra_solvers) { if (IS_AUX_SOLVER(i)) {
r = par.get_solver(i).check(num_lits, lits); r = par.get_solver(i).check(num_lits, lits);
} }
else if (IS_LOCAL_SEARCH(i)) { else if (IS_LOCAL_SEARCH(i)) {
r = ls->check(num_lits, lits, &par); r = ls[i-num_extra_solvers]->check(num_lits, lits, &par);
} }
else { else {
r = check(num_lits, lits); r = check(num_lits, lits);
@ -900,15 +904,15 @@ namespace sat {
} }
} }
if (first) { if (first) {
if (ls) { for (unsigned j = 0; j < ls.size(); ++j) {
ls->rlimit().cancel(); ls[j]->rlimit().cancel();
} }
for (int j = 0; j < num_extra_solvers; ++j) { for (int j = 0; j < num_extra_solvers; ++j) {
if (i != j) { if (i != j) {
par.cancel_solver(j); par.cancel_solver(j);
} }
} }
if ((0 <= i && i < num_extra_solvers) || IS_LOCAL_SEARCH(i)) { if (!IS_MAIN_SOLVER(i)) {
canceled = !rlimit().inc(); canceled = !rlimit().inc();
if (!canceled) { if (!canceled) {
rlimit().cancel(); rlimit().cancel();
@ -926,24 +930,24 @@ namespace sat {
} }
} }
if (finished_id != -1 && finished_id < num_extra_solvers) { if (IS_AUX_SOLVER(finished_id)) {
m_stats = par.get_solver(finished_id).m_stats; m_stats = par.get_solver(finished_id).m_stats;
} }
if (result == l_true && finished_id != -1 && finished_id < num_extra_solvers) { if (result == l_true && IS_AUX_SOLVER(finished_id)) {
set_model(par.get_solver(finished_id).get_model()); set_model(par.get_solver(finished_id).get_model());
} }
else if (result == l_false && finished_id != -1 && finished_id < num_extra_solvers) { else if (result == l_false && IS_AUX_SOLVER(finished_id)) {
m_core.reset(); m_core.reset();
m_core.append(par.get_solver(finished_id).get_core()); m_core.append(par.get_solver(finished_id).get_core());
} }
if (result == l_true && finished_id != -1 && IS_LOCAL_SEARCH(finished_id)) { if (result == l_true && IS_LOCAL_SEARCH(finished_id)) {
set_model(ls->get_model()); set_model(ls[finished_id - num_extra_solvers]->get_model());
} }
if (!canceled) { if (!canceled) {
rlimit().reset_cancel(); rlimit().reset_cancel();
} }
set_par(0, 0); set_par(0, 0);
ls = 0; ls.reset();
if (finished_id == -1) { if (finished_id == -1) {
switch (ex_kind) { switch (ex_kind) {
case ERROR_EX: throw z3_error(error_code); case ERROR_EX: throw z3_error(error_code);