mirror of
https://github.com/Z3Prover/z3
synced 2025-04-28 11:25:51 +00:00
fix local search initialization of units, encode offset in clauses
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
38888b5e5c
commit
2f025f52c0
6 changed files with 47 additions and 18 deletions
|
|
@ -95,7 +95,6 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
|
||||
|
||||
bool clause::satisfied_by(model const & m) const {
|
||||
for (literal l : *this) {
|
||||
if (l.sign()) {
|
||||
|
|
@ -110,6 +109,23 @@ namespace sat {
|
|||
return false;
|
||||
}
|
||||
|
||||
clause_offset clause::get_new_offset() const {
|
||||
unsigned o1 = m_lits[0].index();
|
||||
if (sizeof(clause_offset) == 8) {
|
||||
unsigned o2 = m_lits[1].index();
|
||||
return (clause_offset)o1 + (((clause_offset)o2) << 32);
|
||||
}
|
||||
return (clause_offset)o1;
|
||||
}
|
||||
|
||||
void clause::set_new_offset(clause_offset offset) {
|
||||
m_lits[0] = to_literal(static_cast<unsigned>(offset));
|
||||
if (sizeof(offset) == 8) {
|
||||
m_lits[1] = to_literal(static_cast<unsigned>(offset >> 32));
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
void tmp_clause::set(unsigned num_lits, literal const * lits, bool learned) {
|
||||
if (m_clause && m_clause->m_capacity < num_lits) {
|
||||
dealloc_svect(m_clause);
|
||||
|
|
|
|||
|
|
@ -98,6 +98,8 @@ namespace sat {
|
|||
unsigned glue() const { return m_glue; }
|
||||
void set_psm(unsigned psm) { m_psm = psm > 255 ? 255 : psm; }
|
||||
unsigned psm() const { return m_psm; }
|
||||
clause_offset get_new_offset() const;
|
||||
void set_new_offset(clause_offset off);
|
||||
|
||||
bool on_reinit_stack() const { return m_reinit_stack; }
|
||||
void set_reinit_stack(bool f) { m_reinit_stack = f; }
|
||||
|
|
|
|||
|
|
@ -79,11 +79,13 @@ namespace sat {
|
|||
void local_search::init_cur_solution() {
|
||||
for (var_info& vi : m_vars) {
|
||||
// use bias with a small probability
|
||||
if (m_rand() % 10 < 5 || m_config.phase_sticky()) {
|
||||
vi.m_value = ((unsigned)(m_rand() % 100) < vi.m_bias);
|
||||
}
|
||||
else {
|
||||
vi.m_value = (m_rand() % 2) == 0;
|
||||
if (!vi.m_unit) {
|
||||
if (m_rand() % 10 < 5 || m_config.phase_sticky()) {
|
||||
vi.m_value = ((unsigned)(m_rand() % 100) < vi.m_bias);
|
||||
}
|
||||
else {
|
||||
vi.m_value = (m_rand() % 2) == 0;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -149,7 +151,7 @@ namespace sat {
|
|||
|
||||
void local_search::reinit() {
|
||||
|
||||
IF_VERBOSE(0, verbose_stream() << "(sat-local-search reinit)\n";);
|
||||
IF_VERBOSE(1, verbose_stream() << "(sat-local-search reinit)\n";);
|
||||
if (true || !m_is_pb) {
|
||||
//
|
||||
// the following methods does NOT converge for pseudo-boolean
|
||||
|
|
@ -216,13 +218,15 @@ namespace sat {
|
|||
for (unsigned i = 0; i < m_prop_queue.size() && i < m_vars.size(); ++i) {
|
||||
literal lit2 = m_prop_queue[i];
|
||||
if (!is_true(lit2)) {
|
||||
if (is_unit(lit2)) return false;
|
||||
if (is_unit(lit2)) {
|
||||
return false;
|
||||
}
|
||||
flip_walksat(lit2.var());
|
||||
add_propagation(lit2);
|
||||
}
|
||||
}
|
||||
if (m_prop_queue.size() >= m_vars.size()) {
|
||||
IF_VERBOSE(0, verbose_stream() << "failed literal\n");
|
||||
IF_VERBOSE(0, verbose_stream() << "propagation loop\n");
|
||||
return false;
|
||||
}
|
||||
if (unit) {
|
||||
|
|
@ -328,6 +332,7 @@ namespace sat {
|
|||
return;
|
||||
}
|
||||
if (k == 1 && sz == 2) {
|
||||
// IF_VERBOSE(0, verbose_stream() << "bin: " << ~c[0] << " + " << ~c[1] << " <= 1\n");
|
||||
for (unsigned i = 0; i < 2; ++i) {
|
||||
literal t(c[i]), s(c[1-i]);
|
||||
m_vars.reserve(t.var() + 1);
|
||||
|
|
@ -750,11 +755,12 @@ namespace sat {
|
|||
IF_VERBOSE(1, verbose_stream() << "(sat.local_search :unsat)\n");
|
||||
return;
|
||||
}
|
||||
|
||||
if (is_unit(best_var)) {
|
||||
goto reflip;
|
||||
}
|
||||
flip_walksat(best_var);
|
||||
literal lit(best_var, !cur_solution(best_var));
|
||||
if (!propagate(lit)) {
|
||||
IF_VERBOSE(0, verbose_stream() << "failed literal " << lit << "\n");
|
||||
if (is_true(lit)) {
|
||||
flip_walksat(best_var);
|
||||
}
|
||||
|
|
@ -774,6 +780,7 @@ namespace sat {
|
|||
}
|
||||
|
||||
void local_search::flip_walksat(bool_var flipvar) {
|
||||
VERIFY(!is_unit(flipvar));
|
||||
m_vars[flipvar].m_value = !cur_solution(flipvar);
|
||||
|
||||
bool flip_is_true = cur_solution(flipvar);
|
||||
|
|
|
|||
|
|
@ -529,26 +529,26 @@ namespace sat {
|
|||
IF_VERBOSE(1, verbose_stream() << "(sat-defrag)\n");
|
||||
clause_allocator& alloc = m_cls_allocator[!m_cls_allocator_idx];
|
||||
ptr_vector<clause> new_clauses, new_learned;
|
||||
ptr_addr_map<clause, clause_offset> cls2offset;
|
||||
for (clause* c : m_clauses) c->unmark_used();
|
||||
for (clause* c : m_learned) c->unmark_used();
|
||||
|
||||
#if 0
|
||||
svector<bool_var> vars;
|
||||
for (unsigned i = 0; i < num_vars(); ++i) vars.push_back(i);
|
||||
std::stable_sort(vars.begin(), vars.end(), cmp_activity(*this));
|
||||
literal_vector lits;
|
||||
for (bool_var v : vars) lits.push_back(to_literal(v)), lits.push_back(~to_literal(v));
|
||||
|
||||
// walk clauses, reallocate them in an order that defragments memory and creates locality.
|
||||
//for (literal lit : lits) {
|
||||
//watch_list& wlist = m_watches[lit.index()];
|
||||
#endif
|
||||
for (watch_list& wlist : m_watches) {
|
||||
for (watched& w : wlist) {
|
||||
if (w.is_clause()) {
|
||||
clause& c1 = get_clause(w);
|
||||
clause_offset offset;
|
||||
if (c1.was_used()) {
|
||||
offset = cls2offset[&c1];
|
||||
offset = c1.get_new_offset();
|
||||
}
|
||||
else {
|
||||
clause* c2 = alloc.copy_clause(c1);
|
||||
|
|
@ -560,7 +560,7 @@ namespace sat {
|
|||
new_clauses.push_back(c2);
|
||||
}
|
||||
offset = get_offset(*c2);
|
||||
cls2offset.insert(&c1, offset);
|
||||
c1.set_new_offset(offset);
|
||||
}
|
||||
w = watched(w.get_blocked_literal(), offset);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -5,7 +5,7 @@ def_module_params('parallel',
|
|||
params=(
|
||||
('enable', BOOL, False, 'enable parallel solver by default on selected tactics (for QF_BV)'),
|
||||
('threads.max', UINT, 10000, 'caps maximal number of threads below the number of processors'),
|
||||
('conquer.batch_size', UINT, 1000, 'number of cubes to batch together for fast conquer'),
|
||||
('conquer.batch_size', UINT, 100, 'number of cubes to batch together for fast conquer'),
|
||||
('conquer.restart.max', UINT, 5, 'maximal number of restarts during conquer phase'),
|
||||
('conquer.delay', UINT, 10, 'delay of cubes until applying conquer'),
|
||||
('conquer.backtrack_frequency', UINT, 10, 'frequency to apply core minimization during conquer'),
|
||||
|
|
|
|||
|
|
@ -99,6 +99,8 @@ class parallel_tactic : public tactic {
|
|||
}
|
||||
}
|
||||
|
||||
bool in_shutdown() const { return m_shutdown; }
|
||||
|
||||
void add_task(solver_state* task) {
|
||||
std::lock_guard<std::mutex> lock(m_mutex);
|
||||
m_tasks.push_back(task);
|
||||
|
|
@ -285,6 +287,7 @@ class parallel_tactic : public tactic {
|
|||
p.set_uint("restart.max", pp.simplify_restart_max() * mult);
|
||||
p.set_bool("lookahead_simplify", true);
|
||||
p.set_bool("retain_blocked_clauses", retain_blocked);
|
||||
if (m_depth > 1) p.set_uint("bce_delay", 0);
|
||||
get_solver().updt_params(p);
|
||||
}
|
||||
|
||||
|
|
@ -479,8 +482,8 @@ private:
|
|||
break;
|
||||
|
||||
}
|
||||
if (cubes.size() >= conquer_batch_size() || (!cubes.empty() && m_queue.is_idle())) {
|
||||
spawn_cubes(s, std::max(2u, width), cubes);
|
||||
if (cubes.size() >= conquer_batch_size()) {
|
||||
spawn_cubes(s, 10*width, cubes);
|
||||
first = false;
|
||||
cubes.reset();
|
||||
}
|
||||
|
|
@ -575,6 +578,7 @@ private:
|
|||
}
|
||||
catch (z3_exception& ex) {
|
||||
IF_VERBOSE(1, verbose_stream() << ex.msg() << "\n";);
|
||||
if (m_queue.in_shutdown()) return;
|
||||
m_queue.shutdown();
|
||||
std::lock_guard<std::mutex> lock(m_mutex);
|
||||
if (ex.has_error_code()) {
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue