mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
include chronological backtracking, two-phase sat, xor inprocessing, probsat, ddfw
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
46d23ea8d7
commit
d17248821a
|
@ -10,6 +10,7 @@ z3_add_component(sat
|
|||
sat_clause_use_list.cpp
|
||||
sat_cleaner.cpp
|
||||
sat_config.cpp
|
||||
sat_ddfw.cpp
|
||||
sat_drat.cpp
|
||||
sat_elim_eqs.cpp
|
||||
sat_elim_vars.cpp
|
||||
|
@ -20,6 +21,7 @@ z3_add_component(sat
|
|||
sat_model_converter.cpp
|
||||
sat_mus.cpp
|
||||
sat_parallel.cpp
|
||||
sat_prob.cpp
|
||||
sat_probing.cpp
|
||||
sat_scc.cpp
|
||||
sat_simplifier.cpp
|
||||
|
|
File diff suppressed because it is too large
Load diff
|
@ -26,6 +26,7 @@ Revision History:
|
|||
#include "sat/sat_lookahead.h"
|
||||
#include "sat/sat_unit_walk.h"
|
||||
#include "sat/sat_big.h"
|
||||
#include "util/small_object_allocator.h"
|
||||
#include "util/scoped_ptr_vector.h"
|
||||
#include "util/sorting_network.h"
|
||||
|
||||
|
@ -331,6 +332,7 @@ namespace sat {
|
|||
unsigned use_count(literal lit) const { return m_cnstr_use_list[lit.index()].size() + m_clause_use_list.get(lit).size(); }
|
||||
|
||||
void cleanup_clauses();
|
||||
void cleanup_clauses(clause_vector& clauses);
|
||||
void cleanup_constraints();
|
||||
void cleanup_constraints(ptr_vector<constraint>& cs, bool learned);
|
||||
void remove_constraint(constraint& c, char const* reason);
|
||||
|
@ -347,7 +349,9 @@ namespace sat {
|
|||
void init_watch(bool_var v);
|
||||
void clear_watch(constraint& c);
|
||||
lbool add_assign(constraint& c, literal l);
|
||||
bool incremental_mode() const;
|
||||
void simplify(constraint& c);
|
||||
void pre_simplify(constraint& c);
|
||||
void nullify_tracking_literal(constraint& c);
|
||||
void set_conflict(constraint& c, literal lit);
|
||||
void assign(constraint& c, literal lit);
|
||||
|
@ -355,6 +359,8 @@ namespace sat {
|
|||
void get_antecedents(literal l, constraint const& c, literal_vector & r);
|
||||
bool validate_conflict(constraint const& c) const;
|
||||
bool validate_unit_propagation(constraint const& c, literal alit) const;
|
||||
void validate_eliminated();
|
||||
void validate_eliminated(ptr_vector<constraint> const& cs);
|
||||
void attach_constraint(constraint const& c);
|
||||
void detach_constraint(constraint const& c);
|
||||
lbool eval(constraint const& c) const;
|
||||
|
@ -365,6 +371,7 @@ namespace sat {
|
|||
void recompile(constraint& c);
|
||||
void split_root(constraint& c);
|
||||
unsigned next_id() { return m_constraint_id++; }
|
||||
void set_non_learned(constraint& c);
|
||||
|
||||
|
||||
// cardinality
|
||||
|
@ -391,6 +398,40 @@ namespace sat {
|
|||
void get_xr_antecedents(literal l, unsigned index, justification js, literal_vector& r);
|
||||
void get_antecedents(literal l, xr const& x, literal_vector & r);
|
||||
void simplify(xr& x);
|
||||
void extract_xor();
|
||||
void merge_xor();
|
||||
struct clause_filter {
|
||||
unsigned m_filter;
|
||||
clause* m_clause;
|
||||
clause_filter(unsigned f, clause* cp):
|
||||
m_filter(f), m_clause(cp) {}
|
||||
};
|
||||
typedef svector<bool> bool_vector;
|
||||
unsigned m_max_xor_size;
|
||||
vector<svector<clause_filter>> m_clause_filters; // index of clauses.
|
||||
unsigned m_barbet_combination; // bit-mask of parities that have been found
|
||||
vector<bool_vector> m_barbet_parity; // lookup parity for clauses
|
||||
clause_vector m_barbet_clauses_to_remove; // remove clauses that become xors
|
||||
unsigned_vector m_barbet_var_position; // position of var in main clause
|
||||
literal_vector m_barbet_clause; // reference clause with literals sorted according to main clause
|
||||
unsigned_vector m_barbet_missing; // set of indices not occurring in clause.
|
||||
void init_clause_filter();
|
||||
void init_clause_filter(clause_vector& clauses);
|
||||
inline void barbet_set_combination(unsigned mask) { m_barbet_combination |= (1 << mask); }
|
||||
inline bool barbet_get_combination(unsigned mask) const { return (m_barbet_combination & (1 << mask)) != 0; }
|
||||
void barbet_extract_xor();
|
||||
void barbet_init_parity();
|
||||
void barbet_extract_xor(clause& c);
|
||||
bool barbet_extract_xor(bool parity, clause& c, clause& c2);
|
||||
bool barbet_extract_xor(bool parity, clause& c, literal l1, literal l2);
|
||||
bool barbet_update_combinations(clause& c, bool parity, unsigned mask);
|
||||
void barbet_add_xor(bool parity, clause& c);
|
||||
unsigned get_clause_filter(clause& c);
|
||||
|
||||
vector<ptr_vector<clause>> m_ternary;
|
||||
void extract_ternary(clause_vector const& clauses);
|
||||
bool extract_xor(clause& c, literal l);
|
||||
bool extract_xor(clause& c1, clause& c2);
|
||||
bool clausify(xr& x);
|
||||
void flush_roots(xr& x);
|
||||
lbool eval(xr const& x) const;
|
||||
|
@ -445,7 +486,7 @@ namespace sat {
|
|||
inline void assign(literal l, justification j) {
|
||||
if (m_lookahead) m_lookahead->assign(l);
|
||||
else if (m_unit_walk) m_unit_walk->assign(l);
|
||||
else m_solver->assign(l, j);
|
||||
else m_solver->assign(l, j);
|
||||
}
|
||||
inline void set_conflict(justification j, literal l) {
|
||||
if (m_lookahead) m_lookahead->set_conflict();
|
||||
|
@ -519,6 +560,10 @@ namespace sat {
|
|||
constraint* add_at_least(literal l, literal_vector const& lits, unsigned k, bool learned);
|
||||
constraint* add_pb_ge(literal l, svector<wliteral> const& wlits, unsigned k, bool learned);
|
||||
constraint* add_xr(literal_vector const& lits, bool learned);
|
||||
literal add_xor_def(literal_vector& lits, bool learned = false);
|
||||
bool all_distinct(literal_vector const& lits);
|
||||
bool all_distinct(xr const& x);
|
||||
bool all_distinct(clause const& cl);
|
||||
|
||||
void copy_core(ba_solver* result, bool learned);
|
||||
void copy_constraints(ba_solver* result, ptr_vector<constraint> const& constraints);
|
||||
|
@ -540,6 +585,7 @@ namespace sat {
|
|||
check_result check() override;
|
||||
void push() override;
|
||||
void pop(unsigned n) override;
|
||||
void pre_simplify() override;
|
||||
void simplify() override;
|
||||
void clauses_modifed() override;
|
||||
lbool get_phase(bool_var v) override;
|
||||
|
|
|
@ -32,6 +32,7 @@ namespace sat {
|
|||
updt_params(p);
|
||||
reset_statistics();
|
||||
m_calls = 0;
|
||||
m_touch_index = 0;
|
||||
}
|
||||
|
||||
struct clause_size_lt {
|
||||
|
@ -103,6 +104,7 @@ namespace sat {
|
|||
unsigned eliml0 = m_elim_learned_literals;
|
||||
unsigned elim = m_elim_literals;
|
||||
process(nullptr, s.m_clauses);
|
||||
if (learned) process(nullptr, s.m_learned);
|
||||
s.propagate(false);
|
||||
IF_VERBOSE(4, if (m_elim_learned_literals > eliml0)
|
||||
verbose_stream() << "(sat-asymm-branch :elim " << m_elim_learned_literals - eliml0 << ")\n";);
|
||||
|
@ -168,13 +170,14 @@ namespace sat {
|
|||
CASSERT("asymm_branch", s.check_invariant());
|
||||
TRACE("asymm_branch_detail", s.display(tout););
|
||||
report rpt(*this);
|
||||
svector<char> saved_phase(s.m_phase);
|
||||
svector<bool> saved_phase(s.m_phase);
|
||||
|
||||
bool change = true;
|
||||
unsigned counter = 0;
|
||||
while (change && counter < 2) {
|
||||
++counter;
|
||||
change = false;
|
||||
s.m_touch_index++;
|
||||
if (m_asymm_branch_sampled) {
|
||||
big big(s.m_rand);
|
||||
if (process(big, true)) change = true;
|
||||
|
@ -185,9 +188,10 @@ namespace sat {
|
|||
}
|
||||
if (m_asymm_branch) {
|
||||
m_counter = 0;
|
||||
if (process(true)) change = true;
|
||||
if (process(false)) change = true;
|
||||
m_counter = -m_counter;
|
||||
}
|
||||
m_touch_index = s.m_touch_index;
|
||||
}
|
||||
|
||||
s.m_phase = saved_phase;
|
||||
|
@ -196,6 +200,7 @@ namespace sat {
|
|||
m_asymm_branch_limit = UINT_MAX;
|
||||
|
||||
CASSERT("asymm_branch", s.check_invariant());
|
||||
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -222,24 +227,12 @@ namespace sat {
|
|||
}
|
||||
};
|
||||
|
||||
void asymm_branch::sort(big& big, clause const& c) {
|
||||
sort(big, c.begin(), c.end());
|
||||
bool asymm_branch::is_touched(bool_var v) const {
|
||||
return s.m_touched[v] >= m_touch_index;
|
||||
}
|
||||
|
||||
void asymm_branch::radix_sort(big& big, literal_vector& lits) {
|
||||
const unsigned d = 4;
|
||||
const unsigned w = 20; // 1M variable cap
|
||||
unsigned sz = lits.size();
|
||||
m_tmp.reserve(sz);
|
||||
for (unsigned p = 0; p < w/d; ++p) {
|
||||
unsigned on[16];
|
||||
memset(on, 0, 16*sizeof(unsigned));
|
||||
for (literal l : lits) on[(big.get_left(l) >> 4*p) & 15]++;
|
||||
for (unsigned i = 1; i < 16; ++i) on[i] += on[i-1];
|
||||
for (unsigned i = sz; i-- > 0; )
|
||||
m_tmp[--on[(big.get_left(lits[i]) >> 4*p) & 15]] = lits[i];
|
||||
for (unsigned i = sz; i-- > 0; ) lits[i] = m_tmp[i];
|
||||
}
|
||||
void asymm_branch::sort(big& big, clause const& c) {
|
||||
sort(big, c.begin(), c.end());
|
||||
}
|
||||
|
||||
void asymm_branch::sort(big& big, literal const* begin, literal const* end) {
|
||||
|
@ -253,10 +246,6 @@ namespace sat {
|
|||
std::sort(m_pos.begin(), m_pos.end(), cmp);
|
||||
std::sort(m_neg.begin(), m_neg.end(), cmp);
|
||||
|
||||
// alternative: worse
|
||||
// radix_sort(big, m_pos);
|
||||
// radix_sort(big, m_neg);
|
||||
|
||||
IF_VERBOSE(100,
|
||||
for (literal l : m_pos) verbose_stream() << big.get_left(l) << " ";
|
||||
verbose_stream() << "\n";
|
||||
|
@ -286,22 +275,6 @@ namespace sat {
|
|||
return false;
|
||||
}
|
||||
|
||||
void asymm_branch::minimize(big& big, literal_vector& lemma) {
|
||||
big.ensure_big(s, true);
|
||||
sort(big, lemma.begin(), lemma.end());
|
||||
uhle(big);
|
||||
if (!m_to_delete.empty()) {
|
||||
unsigned j = 0;
|
||||
for (unsigned i = 0; i < lemma.size(); ++i) {
|
||||
literal l = lemma[i];
|
||||
if (!m_to_delete.contains(l)) {
|
||||
lemma[j++] = l;
|
||||
}
|
||||
}
|
||||
lemma.shrink(j);
|
||||
}
|
||||
}
|
||||
|
||||
void asymm_branch::uhle(big& big) {
|
||||
m_to_delete.reset();
|
||||
if (m_to_delete.empty()) {
|
||||
|
@ -365,6 +338,9 @@ namespace sat {
|
|||
|
||||
|
||||
bool asymm_branch::propagate_literal(clause const& c, literal l) {
|
||||
if (!is_touched(l.var())) {
|
||||
return false;
|
||||
}
|
||||
SASSERT(!s.inconsistent());
|
||||
TRACE("asymm_branch_detail", tout << "assigning: " << l << "\n";);
|
||||
s.assign_scoped(l);
|
||||
|
@ -439,13 +415,7 @@ namespace sat {
|
|||
scoped_d.del_clause();
|
||||
return false;
|
||||
default:
|
||||
c.shrink(new_sz);
|
||||
if (s.m_config.m_drat && new_sz < old_sz) {
|
||||
s.m_drat.add(c, true);
|
||||
c.restore(old_sz);
|
||||
s.m_drat.del(c);
|
||||
c.shrink(new_sz);
|
||||
}
|
||||
s.shrink(c, old_sz, new_sz);
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
|
|
@ -36,6 +36,7 @@ namespace sat {
|
|||
int64_t m_counter;
|
||||
random_gen m_rand;
|
||||
unsigned m_calls;
|
||||
unsigned m_touch_index;
|
||||
|
||||
// config
|
||||
bool m_asymm_branch;
|
||||
|
@ -57,9 +58,10 @@ namespace sat {
|
|||
|
||||
struct compare_left;
|
||||
|
||||
bool is_touched(bool_var v) const;
|
||||
|
||||
void sort(big& big, literal const* begin, literal const* end);
|
||||
void sort(big & big, clause const& c);
|
||||
void radix_sort(big & big, literal_vector& lits);
|
||||
|
||||
bool uhle(scoped_detach& scoped_d, big & big, clause & c);
|
||||
|
||||
|
@ -100,8 +102,6 @@ namespace sat {
|
|||
void collect_statistics(statistics & st) const;
|
||||
void reset_statistics();
|
||||
|
||||
void minimize(big& big, literal_vector& lemma);
|
||||
|
||||
void init_search() { m_calls = 0; }
|
||||
|
||||
inline void dec(unsigned c) { m_counter -= c; }
|
||||
|
|
|
@ -82,6 +82,7 @@ namespace sat {
|
|||
int get_right(literal l) const { return m_right[l.index()]; }
|
||||
literal get_parent(literal l) const { return m_parent[l.index()]; }
|
||||
literal get_root(literal l);
|
||||
bool is_root(literal l) { return get_root(l) == l; }
|
||||
bool reaches(literal u, literal v) const { return m_left[u.index()] < m_left[v.index()] && m_right[v.index()] < m_right[u.index()]; }
|
||||
bool connected(literal u, literal v) const { return reaches(u, v) || reaches(~v, ~u); }
|
||||
void display(std::ostream& out) const;
|
||||
|
|
|
@ -133,18 +133,12 @@ namespace sat {
|
|||
s.del_clause(c);
|
||||
break;
|
||||
default:
|
||||
c.shrink(new_sz);
|
||||
s.shrink(c, sz, new_sz);
|
||||
*it2 = *it;
|
||||
it2++;
|
||||
if (!c.frozen()) {
|
||||
s.attach_clause(c);
|
||||
}
|
||||
if (s.m_config.m_drat && new_sz < sz) {
|
||||
s.m_drat.add(c, true);
|
||||
c.restore(sz);
|
||||
s.m_drat.del(c);
|
||||
c.shrink(new_sz);
|
||||
}
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
@ -173,12 +167,33 @@ namespace sat {
|
|||
}
|
||||
};
|
||||
|
||||
bool cleaner::is_clean() const {
|
||||
for (clause* cp : s.m_clauses) {
|
||||
for (literal lit : *cp) {
|
||||
if (s.value(lit) != l_undef && s.lvl(lit) == 0) return false;
|
||||
}
|
||||
}
|
||||
for (clause* cp : s.m_learned) {
|
||||
for (literal lit : *cp) {
|
||||
if (s.value(lit) != l_undef && s.lvl(lit) == 0) return false;
|
||||
}
|
||||
}
|
||||
unsigned idx = 0;
|
||||
for (auto& wlist : s.m_watches) {
|
||||
literal lit = to_literal(idx);
|
||||
if (s.value(lit) != l_undef && s.lvl(lit) == 0 && !wlist.empty()) return false;
|
||||
++idx;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Return true if cleaner executed.
|
||||
*/
|
||||
bool cleaner::operator()(bool force) {
|
||||
CASSERT("cleaner_bug", s.check_invariant());
|
||||
unsigned trail_sz = s.m_trail.size();
|
||||
|
||||
s.propagate(false); // make sure that everything was propagated.
|
||||
TRACE("sat_cleaner_bug", s.display(tout); s.display_watches(tout););
|
||||
if (s.m_inconsistent)
|
||||
|
|
|
@ -40,6 +40,7 @@ namespace sat {
|
|||
public:
|
||||
cleaner(solver & s);
|
||||
|
||||
bool is_clean() const;
|
||||
bool operator()(bool force = false);
|
||||
|
||||
void collect_statistics(statistics & st) const;
|
||||
|
|
|
@ -54,32 +54,40 @@ namespace sat {
|
|||
m_phase = PS_ALWAYS_FALSE;
|
||||
else if (s == symbol("always_true"))
|
||||
m_phase = PS_ALWAYS_TRUE;
|
||||
else if (s == symbol("basic_caching"))
|
||||
m_phase = PS_BASIC_CACHING;
|
||||
else if (s == symbol("caching"))
|
||||
m_phase = PS_CACHING;
|
||||
m_phase = PS_SAT_CACHING;
|
||||
else if (s == symbol("random"))
|
||||
m_phase = PS_RANDOM;
|
||||
else
|
||||
throw sat_param_exception("invalid phase selection strategy");
|
||||
|
||||
m_phase_caching_on = p.phase_caching_on();
|
||||
m_phase_caching_off = p.phase_caching_off();
|
||||
m_rephase_base = p.rephase_base();
|
||||
m_search_sat_conflicts = p.search_sat_conflicts();
|
||||
m_search_unsat_conflicts = p.search_unsat_conflicts();
|
||||
m_phase_sticky = p.phase_sticky();
|
||||
|
||||
m_restart_initial = p.restart_initial();
|
||||
m_restart_factor = p.restart_factor();
|
||||
m_restart_max = p.restart_max();
|
||||
m_activity_scale = 100;
|
||||
m_propagate_prefetch = p.propagate_prefetch();
|
||||
m_inprocess_max = p.inprocess_max();
|
||||
|
||||
m_random_freq = p.random_freq();
|
||||
m_random_seed = p.random_seed();
|
||||
if (m_random_seed == 0)
|
||||
if (m_random_seed == 0) {
|
||||
m_random_seed = _p.get_uint("random_seed", 0);
|
||||
}
|
||||
|
||||
m_burst_search = p.burst_search();
|
||||
|
||||
m_max_conflicts = p.max_conflicts();
|
||||
m_num_threads = p.threads();
|
||||
m_ddfw_search = p.ddfw_search();
|
||||
m_ddfw_threads = p.ddfw_threads();
|
||||
m_prob_search = p.prob_search();
|
||||
m_local_search = p.local_search();
|
||||
m_local_search_threads = p.local_search_threads();
|
||||
if (p.local_search_mode() == symbol("gsat"))
|
||||
|
@ -89,6 +97,7 @@ namespace sat {
|
|||
m_local_search_dbg_flips = p.local_search_dbg_flips();
|
||||
m_unit_walk = p.unit_walk();
|
||||
m_unit_walk_threads = p.unit_walk_threads();
|
||||
m_binspr = false; // unsound :-( p.binspr();
|
||||
m_lookahead_simplify = p.lookahead_simplify();
|
||||
m_lookahead_double = p.lookahead_double();
|
||||
m_lookahead_simplify_bca = p.lookahead_simplify_bca();
|
||||
|
@ -159,6 +168,9 @@ namespace sat {
|
|||
|
||||
m_force_cleanup = p.force_cleanup();
|
||||
|
||||
m_backtrack_scopes = p.backtrack_scopes();
|
||||
m_backtrack_init_conflicts = p.backtrack_conflicts();
|
||||
|
||||
m_minimize_lemmas = p.minimize_lemmas();
|
||||
m_core_minimize = p.core_minimize();
|
||||
m_core_minimize_partial = p.core_minimize_partial();
|
||||
|
@ -217,6 +229,7 @@ namespace sat {
|
|||
throw sat_param_exception("invalid PB lemma format: 'cardinality' or 'pb' expected");
|
||||
|
||||
m_card_solver = p.cardinality_solver();
|
||||
m_xor_solver = p.xor_solver();
|
||||
|
||||
sat_simplifier_params sp(_p);
|
||||
m_elim_vars = sp.elim_vars();
|
||||
|
|
|
@ -27,7 +27,8 @@ namespace sat {
|
|||
enum phase_selection {
|
||||
PS_ALWAYS_TRUE,
|
||||
PS_ALWAYS_FALSE,
|
||||
PS_CACHING,
|
||||
PS_BASIC_CACHING,
|
||||
PS_SAT_CACHING,
|
||||
PS_RANDOM
|
||||
};
|
||||
|
||||
|
@ -86,9 +87,10 @@ namespace sat {
|
|||
struct config {
|
||||
unsigned long long m_max_memory;
|
||||
phase_selection m_phase;
|
||||
unsigned m_phase_caching_on;
|
||||
unsigned m_phase_caching_off;
|
||||
unsigned m_search_sat_conflicts;
|
||||
unsigned m_search_unsat_conflicts;
|
||||
bool m_phase_sticky;
|
||||
unsigned m_rephase_base;
|
||||
bool m_propagate_prefetch;
|
||||
restart_strategy m_restart;
|
||||
bool m_restart_fast;
|
||||
|
@ -96,6 +98,7 @@ namespace sat {
|
|||
double m_restart_factor; // for geometric case
|
||||
double m_restart_margin; // for ema
|
||||
unsigned m_restart_max;
|
||||
unsigned m_activity_scale;
|
||||
double m_fast_glue_avg;
|
||||
double m_slow_glue_avg;
|
||||
unsigned m_inprocess_max;
|
||||
|
@ -104,12 +107,16 @@ namespace sat {
|
|||
unsigned m_burst_search;
|
||||
unsigned m_max_conflicts;
|
||||
unsigned m_num_threads;
|
||||
bool m_ddfw_search;
|
||||
unsigned m_ddfw_threads;
|
||||
bool m_prob_search;
|
||||
unsigned m_local_search_threads;
|
||||
bool m_local_search;
|
||||
local_search_mode m_local_search_mode;
|
||||
bool m_local_search_dbg_flips;
|
||||
unsigned m_unit_walk_threads;
|
||||
bool m_unit_walk;
|
||||
bool m_binspr;
|
||||
bool m_lookahead_simplify;
|
||||
bool m_lookahead_simplify_bca;
|
||||
cutoff_t m_lookahead_cube_cutoff;
|
||||
|
@ -143,11 +150,16 @@ namespace sat {
|
|||
|
||||
bool m_force_cleanup;
|
||||
|
||||
// backtracking
|
||||
unsigned m_backtrack_scopes;
|
||||
unsigned m_backtrack_init_conflicts;
|
||||
|
||||
bool m_minimize_lemmas;
|
||||
bool m_dyn_sub_res;
|
||||
bool m_core_minimize;
|
||||
bool m_core_minimize_partial;
|
||||
|
||||
// drat proofs
|
||||
bool m_drat;
|
||||
bool m_drat_binary;
|
||||
symbol m_drat_file;
|
||||
|
@ -155,6 +167,7 @@ namespace sat {
|
|||
bool m_drat_check_sat;
|
||||
|
||||
bool m_card_solver;
|
||||
bool m_xor_solver;
|
||||
pb_resolve m_pb_resolve;
|
||||
pb_lemma_format m_pb_lemma_format;
|
||||
|
||||
|
|
594
src/sat/sat_ddfw.cpp
Normal file
594
src/sat/sat_ddfw.cpp
Normal file
|
@ -0,0 +1,594 @@
|
|||
/*++
|
||||
Copyright (c) 2019 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
sat_ddfw.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
DDFW Local search module for clauses
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner, Marijn Heule 2019-4-23
|
||||
|
||||
|
||||
Notes:
|
||||
|
||||
http://www.ict.griffith.edu.au/~johnt/publications/CP2006raouf.pdf
|
||||
|
||||
|
||||
Todo:
|
||||
- rephase strategy
|
||||
- experiment with backoff schemes for restarts
|
||||
- parallel sync
|
||||
--*/
|
||||
|
||||
#include "util/luby.h"
|
||||
#include "sat/sat_ddfw.h"
|
||||
#include "sat/sat_solver.h"
|
||||
#include "sat/sat_params.hpp"
|
||||
|
||||
namespace sat {
|
||||
|
||||
ddfw::~ddfw() {
|
||||
for (auto& ci : m_clauses) {
|
||||
m_alloc.del_clause(ci.m_clause);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
lbool ddfw::check(unsigned sz, literal const* assumptions, parallel* p) {
|
||||
init(sz, assumptions);
|
||||
flet<parallel*> _p(m_par, p);
|
||||
while (m_limit.inc() && m_min_sz > 0) {
|
||||
if (should_reinit_weights()) do_reinit_weights();
|
||||
else if (do_flip()) ;
|
||||
else if (should_restart()) do_restart();
|
||||
else if (should_parallel_sync()) do_parallel_sync();
|
||||
else shift_weights();
|
||||
}
|
||||
return m_min_sz == 0 ? l_true : l_undef;
|
||||
}
|
||||
|
||||
void ddfw::log() {
|
||||
double sec = m_stopwatch.get_current_seconds();
|
||||
double kflips_per_sec = (m_flips - m_last_flips) / (1000.0 * sec);
|
||||
if (m_last_flips == 0) {
|
||||
IF_VERBOSE(0, verbose_stream() << "(sat.ddfw :unsat :models :kflips/sec :flips :restarts :reinits :unsat_vars :shifts";
|
||||
if (m_par) verbose_stream() << " :par";
|
||||
verbose_stream() << ")\n");
|
||||
}
|
||||
IF_VERBOSE(0, verbose_stream() << "(sat.ddfw "
|
||||
<< std::setw(07) << m_min_sz
|
||||
<< std::setw(07) << m_models.size()
|
||||
<< std::setw(10) << kflips_per_sec
|
||||
<< std::setw(10) << m_flips
|
||||
<< std::setw(10) << m_restart_count
|
||||
<< std::setw(10) << m_reinit_count
|
||||
<< std::setw(10) << m_unsat_vars.size()
|
||||
<< std::setw(10) << m_shifts;
|
||||
if (m_par) verbose_stream() << std::setw(10) << m_parsync_count;
|
||||
verbose_stream() << ")\n");
|
||||
m_stopwatch.start();
|
||||
m_last_flips = m_flips;
|
||||
}
|
||||
|
||||
bool ddfw::do_flip() {
|
||||
bool_var v = pick_var();
|
||||
if (reward(v) > 0 || (reward(v) == 0 && m_rand(100) <= m_config.m_use_reward_zero_pct)) {
|
||||
flip(v);
|
||||
if (m_unsat.size() <= m_min_sz) save_best_values();
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
bool_var ddfw::pick_var() {
|
||||
double sum_pos = 0;
|
||||
unsigned n = 1;
|
||||
bool_var v0 = null_bool_var;
|
||||
for (bool_var v : m_unsat_vars) {
|
||||
int r = reward(v);
|
||||
if (r > 0) {
|
||||
sum_pos += score(r);
|
||||
}
|
||||
else if (r == 0 && sum_pos == 0 && (m_rand() % (n++)) == 0) {
|
||||
v0 = v;
|
||||
}
|
||||
}
|
||||
if (sum_pos > 0) {
|
||||
double lim_pos = ((double) m_rand() / (1.0 + m_rand.max_value())) * sum_pos;
|
||||
for (bool_var v : m_unsat_vars) {
|
||||
int r = reward(v);
|
||||
if (r > 0) {
|
||||
lim_pos -= score(r);
|
||||
if (lim_pos <= 0) {
|
||||
if (m_par) update_reward_avg(v);
|
||||
return v;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
if (v0 != null_bool_var) {
|
||||
return v0;
|
||||
}
|
||||
return m_unsat_vars.elem_at(m_rand(m_unsat_vars.size()));
|
||||
}
|
||||
|
||||
/**
|
||||
* TBD: map reward value to a score, possibly through an exponential function, such as
|
||||
* exp(-tau/r), where tau > 0
|
||||
*/
|
||||
double ddfw::mk_score(unsigned r) {
|
||||
return r;
|
||||
}
|
||||
|
||||
|
||||
void ddfw::add(unsigned n, literal const* c) {
|
||||
clause* cls = m_alloc.mk_clause(n, c, false);
|
||||
unsigned idx = m_clauses.size();
|
||||
m_clauses.push_back(clause_info(cls, m_config.m_init_clause_weight));
|
||||
for (literal lit : *cls) {
|
||||
m_use_list.reserve(lit.index()+1);
|
||||
m_vars.reserve(lit.var()+1);
|
||||
m_use_list[lit.index()].push_back(idx);
|
||||
}
|
||||
}
|
||||
|
||||
void ddfw::add(solver const& s) {
|
||||
for (auto& ci : m_clauses) {
|
||||
m_alloc.del_clause(ci.m_clause);
|
||||
}
|
||||
m_clauses.reset();
|
||||
m_use_list.reset();
|
||||
m_num_non_binary_clauses = 0;
|
||||
|
||||
unsigned trail_sz = s.init_trail_size();
|
||||
for (unsigned i = 0; i < trail_sz; ++i) {
|
||||
add(1, s.m_trail.c_ptr() + i);
|
||||
}
|
||||
unsigned sz = s.m_watches.size();
|
||||
for (unsigned l_idx = 0; l_idx < sz; ++l_idx) {
|
||||
literal l1 = ~to_literal(l_idx);
|
||||
watch_list const & wlist = s.m_watches[l_idx];
|
||||
for (watched const& w : wlist) {
|
||||
if (!w.is_binary_non_learned_clause())
|
||||
continue;
|
||||
literal l2 = w.get_literal();
|
||||
if (l1.index() > l2.index())
|
||||
continue;
|
||||
literal ls[2] = { l1, l2 };
|
||||
add(2, ls);
|
||||
}
|
||||
}
|
||||
for (clause* c : s.m_clauses) {
|
||||
add(c->size(), c->begin());
|
||||
}
|
||||
m_num_non_binary_clauses = s.m_clauses.size();
|
||||
}
|
||||
|
||||
void ddfw::add_assumptions() {
|
||||
for (unsigned i = 0; i < m_assumptions.size(); ++i) {
|
||||
add(1, m_assumptions.c_ptr() + i);
|
||||
}
|
||||
}
|
||||
|
||||
void ddfw::init(unsigned sz, literal const* assumptions) {
|
||||
m_assumptions.reset();
|
||||
m_assumptions.append(sz, assumptions);
|
||||
add_assumptions();
|
||||
for (unsigned v = 0; v < num_vars(); ++v) {
|
||||
literal lit(v, false), nlit(v, true);
|
||||
value(v) = (m_rand() % 2) == 0; // m_use_list[lit.index()].size() >= m_use_list[nlit.index()].size();
|
||||
}
|
||||
init_clause_data();
|
||||
flatten_use_list();
|
||||
|
||||
m_reinit_count = 0;
|
||||
m_reinit_next = m_config.m_reinit_base;
|
||||
|
||||
m_restart_count = 0;
|
||||
m_restart_next = m_config.m_restart_base*2;
|
||||
|
||||
m_parsync_count = 0;
|
||||
m_parsync_next = m_config.m_parsync_base;
|
||||
|
||||
m_min_sz = m_unsat.size();
|
||||
m_flips = 0;
|
||||
m_last_flips = 0;
|
||||
m_shifts = 0;
|
||||
m_stopwatch.start();
|
||||
}
|
||||
|
||||
void ddfw::reinit(solver& s) {
|
||||
add(s);
|
||||
add_assumptions();
|
||||
if (s.m_best_phase_size > 0) {
|
||||
for (unsigned v = 0; v < num_vars(); ++v) {
|
||||
value(v) = s.m_best_phase[v];
|
||||
reward(v) = 0;
|
||||
make_count(v) = 0;
|
||||
}
|
||||
}
|
||||
init_clause_data();
|
||||
flatten_use_list();
|
||||
}
|
||||
|
||||
void ddfw::flatten_use_list() {
|
||||
m_use_list_index.reset();
|
||||
m_flat_use_list.reset();
|
||||
for (auto const& ul : m_use_list) {
|
||||
m_use_list_index.push_back(m_flat_use_list.size());
|
||||
m_flat_use_list.append(ul);
|
||||
}
|
||||
m_use_list_index.push_back(m_flat_use_list.size());
|
||||
}
|
||||
|
||||
|
||||
void ddfw::flip(bool_var v) {
|
||||
++m_flips;
|
||||
literal lit = literal(v, !value(v));
|
||||
literal nlit = ~lit;
|
||||
SASSERT(is_true(lit));
|
||||
for (unsigned cls_idx : use_list(*this, lit)) {
|
||||
clause_info& ci = m_clauses[cls_idx];
|
||||
ci.del(lit);
|
||||
unsigned w = ci.m_weight;
|
||||
// cls becomes false: flip any variable in clause to receive reward w
|
||||
switch (ci.m_num_trues) {
|
||||
case 0: {
|
||||
m_unsat.insert(cls_idx);
|
||||
clause const& c = get_clause(cls_idx);
|
||||
for (literal l : c) {
|
||||
inc_reward(l, w);
|
||||
inc_make(l);
|
||||
}
|
||||
inc_reward(lit, w);
|
||||
break;
|
||||
}
|
||||
case 1:
|
||||
dec_reward(to_literal(ci.m_trues), w);
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
}
|
||||
for (unsigned cls_idx : use_list(*this, nlit)) {
|
||||
clause_info& ci = m_clauses[cls_idx];
|
||||
unsigned w = ci.m_weight;
|
||||
// the clause used to have a single true (pivot) literal, now it has two.
|
||||
// Then the previous pivot is no longer penalized for flipping.
|
||||
switch (ci.m_num_trues) {
|
||||
case 0: {
|
||||
m_unsat.remove(cls_idx);
|
||||
clause const& c = get_clause(cls_idx);
|
||||
for (literal l : c) {
|
||||
dec_reward(l, w);
|
||||
dec_make(l);
|
||||
}
|
||||
dec_reward(nlit, w);
|
||||
break;
|
||||
}
|
||||
case 1:
|
||||
inc_reward(to_literal(ci.m_trues), w);
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
ci.add(nlit);
|
||||
}
|
||||
value(v) = !value(v);
|
||||
}
|
||||
|
||||
bool ddfw::should_reinit_weights() {
|
||||
return m_flips >= m_reinit_next;
|
||||
}
|
||||
|
||||
void ddfw::do_reinit_weights() {
|
||||
log();
|
||||
|
||||
if (m_reinit_count % 2 == 0) {
|
||||
for (auto& ci : m_clauses) {
|
||||
ci.m_weight += 1;
|
||||
}
|
||||
}
|
||||
else {
|
||||
for (auto& ci : m_clauses) {
|
||||
if (ci.is_true()) {
|
||||
ci.m_weight = m_config.m_init_clause_weight;
|
||||
}
|
||||
else {
|
||||
ci.m_weight = m_config.m_init_clause_weight + 1;
|
||||
}
|
||||
}
|
||||
}
|
||||
init_clause_data();
|
||||
++m_reinit_count;
|
||||
m_reinit_next += m_reinit_count * m_config.m_reinit_base;
|
||||
}
|
||||
|
||||
void ddfw::init_clause_data() {
|
||||
for (unsigned v = 0; v < num_vars(); ++v) {
|
||||
make_count(v) = 0;
|
||||
reward(v) = 0;
|
||||
}
|
||||
m_unsat_vars.reset();
|
||||
m_unsat.reset();
|
||||
unsigned sz = m_clauses.size();
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
auto& ci = m_clauses[i];
|
||||
clause const& c = get_clause(i);
|
||||
ci.m_trues = 0;
|
||||
ci.m_num_trues = 0;
|
||||
for (literal lit : c) {
|
||||
if (is_true(lit)) {
|
||||
ci.add(lit);
|
||||
}
|
||||
}
|
||||
switch (ci.m_num_trues) {
|
||||
case 0:
|
||||
for (literal lit : c) {
|
||||
inc_reward(lit, ci.m_weight);
|
||||
inc_make(lit);
|
||||
}
|
||||
m_unsat.insert(i);
|
||||
break;
|
||||
case 1:
|
||||
dec_reward(to_literal(ci.m_trues), ci.m_weight);
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
bool ddfw::should_restart() {
|
||||
return m_flips >= m_restart_next;
|
||||
}
|
||||
|
||||
void ddfw::do_restart() {
|
||||
reinit_values();
|
||||
init_clause_data();
|
||||
m_restart_next += m_config.m_restart_base*get_luby(++m_restart_count);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief the higher the bias, the lower the probability to deviate from the value of the bias
|
||||
during a restart.
|
||||
bias = 0 -> flip truth value with 50%
|
||||
|bias| = 1 -> toss coin with 25% probability
|
||||
|bias| = 2 -> toss coin with 12.5% probability
|
||||
etc
|
||||
*/
|
||||
void ddfw::reinit_values() {
|
||||
for (unsigned i = 0; i < num_vars(); ++i) {
|
||||
int b = bias(i);
|
||||
if (0 == (m_rand() % (1 + abs(b)))) {
|
||||
value(i) = (m_rand() % 2) == 0;
|
||||
}
|
||||
else {
|
||||
value(i) = bias(i) > 0;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
bool ddfw::should_parallel_sync() {
|
||||
return m_par != nullptr && m_flips >= m_parsync_next;
|
||||
}
|
||||
|
||||
void ddfw::do_parallel_sync() {
|
||||
if (m_par->from_solver(*this)) {
|
||||
// Sum exp(xi) / exp(a) = Sum exp(xi - a)
|
||||
double max_avg = 0;
|
||||
for (unsigned v = 0; v < num_vars(); ++v) {
|
||||
max_avg = std::max(max_avg, (double)m_vars[v].m_reward_avg);
|
||||
}
|
||||
double sum = 0;
|
||||
for (unsigned v = 0; v < num_vars(); ++v) {
|
||||
sum += exp(m_config.m_itau * (m_vars[v].m_reward_avg - max_avg));
|
||||
}
|
||||
if (sum == 0) {
|
||||
sum = 0.01;
|
||||
}
|
||||
m_probs.reset();
|
||||
for (unsigned v = 0; v < num_vars(); ++v) {
|
||||
m_probs.push_back(exp(m_config.m_itau * (m_vars[v].m_reward_avg - max_avg)) / sum);
|
||||
}
|
||||
m_par->to_solver(*this);
|
||||
}
|
||||
++m_parsync_count;
|
||||
m_parsync_next *= 3;
|
||||
m_parsync_next /= 2;
|
||||
}
|
||||
|
||||
void ddfw::save_best_values() {
|
||||
if (m_unsat.empty()) {
|
||||
m_model.reserve(num_vars());
|
||||
for (unsigned i = 0; i < num_vars(); ++i) {
|
||||
m_model[i] = to_lbool(value(i));
|
||||
}
|
||||
}
|
||||
if (m_unsat.size() < m_min_sz) {
|
||||
m_models.reset();
|
||||
// skip saving the first model.
|
||||
for (unsigned v = 0; v < num_vars(); ++v) {
|
||||
int& b = bias(v);
|
||||
if (abs(b) > 3) {
|
||||
b = b > 0 ? 3 : -3;
|
||||
}
|
||||
}
|
||||
}
|
||||
unsigned h = value_hash();
|
||||
if (!m_models.contains(h)) {
|
||||
for (unsigned v = 0; v < num_vars(); ++v) {
|
||||
bias(v) += value(v) ? 1 : -1;
|
||||
}
|
||||
m_models.insert(h);
|
||||
if (m_models.size() > m_config.m_max_num_models) {
|
||||
m_models.erase(*m_models.begin());
|
||||
}
|
||||
}
|
||||
m_min_sz = m_unsat.size();
|
||||
}
|
||||
|
||||
unsigned ddfw::value_hash() const {
|
||||
unsigned s0 = 0, s1 = 0;
|
||||
for (auto const& vi : m_vars) {
|
||||
s0 += vi.m_value;
|
||||
s1 += s0;
|
||||
}
|
||||
return s1;
|
||||
}
|
||||
|
||||
|
||||
/**
|
||||
\brief Filter on whether to select a satisfied clause
|
||||
1. with some probability prefer higher weight to lesser weight.
|
||||
2. take into account number of trues ?
|
||||
3. select multiple clauses instead of just one per clause in unsat.
|
||||
*/
|
||||
|
||||
bool ddfw::select_clause(unsigned max_weight, unsigned max_trues, clause_info const& cn, unsigned& n) {
|
||||
if (cn.m_num_trues == 0 || cn.m_weight < max_weight) {
|
||||
return false;
|
||||
}
|
||||
if (cn.m_weight > max_weight) {
|
||||
n = 2;
|
||||
return true;
|
||||
}
|
||||
return (m_rand() % (n++)) == 0;
|
||||
}
|
||||
|
||||
unsigned ddfw::select_max_same_sign(unsigned cf_idx) {
|
||||
clause const& c = get_clause(cf_idx);
|
||||
unsigned sz = c.size();
|
||||
unsigned max_weight = 2;
|
||||
unsigned max_trues = 0;
|
||||
unsigned cl = UINT_MAX; // clause pointer to same sign, max weight satisfied clause.
|
||||
unsigned n = 1;
|
||||
for (literal lit : c) {
|
||||
for (unsigned cn_idx : use_list(*this, lit)) {
|
||||
auto& cn = m_clauses[cn_idx];
|
||||
if (select_clause(max_weight, max_trues, cn, n)) {
|
||||
cl = cn_idx;
|
||||
max_weight = cn.m_weight;
|
||||
max_trues = cn.m_num_trues;
|
||||
}
|
||||
}
|
||||
}
|
||||
return cl;
|
||||
}
|
||||
|
||||
void ddfw::shift_weights() {
|
||||
++m_shifts;
|
||||
for (unsigned cf_idx : m_unsat) {
|
||||
auto& cf = m_clauses[cf_idx];
|
||||
SASSERT(!cf.is_true());
|
||||
unsigned cn_idx = select_max_same_sign(cf_idx);
|
||||
while (cn_idx == UINT_MAX) {
|
||||
unsigned idx = (m_rand() * m_rand()) % m_clauses.size();
|
||||
auto & cn = m_clauses[idx];
|
||||
if (cn.is_true() && cn.m_weight >= 2) {
|
||||
cn_idx = idx;
|
||||
}
|
||||
}
|
||||
auto & cn = m_clauses[cn_idx];
|
||||
SASSERT(cn.is_true());
|
||||
unsigned wn = cn.m_weight;
|
||||
SASSERT(wn >= 2);
|
||||
unsigned inc = (wn > 2) ? 2 : 1;
|
||||
SASSERT(wn - inc >= 1);
|
||||
cf.m_weight += inc;
|
||||
cn.m_weight -= inc;
|
||||
for (literal lit : get_clause(cf_idx)) {
|
||||
inc_reward(lit, inc);
|
||||
}
|
||||
if (cn.m_num_trues == 1) {
|
||||
inc_reward(to_literal(cn.m_trues), inc);
|
||||
}
|
||||
}
|
||||
// DEBUG_CODE(invariant(););
|
||||
}
|
||||
|
||||
std::ostream& ddfw::display(std::ostream& out) const {
|
||||
unsigned num_cls = m_clauses.size();
|
||||
for (unsigned i = 0; i < num_cls; ++i) {
|
||||
out << get_clause(i) << " ";
|
||||
auto const& ci = m_clauses[i];
|
||||
out << ci.m_num_trues << " " << ci.m_weight << "\n";
|
||||
}
|
||||
for (unsigned v = 0; v < num_vars(); ++v) {
|
||||
out << v << ": " << reward(v) << "\n";
|
||||
}
|
||||
out << "unsat vars: ";
|
||||
for (bool_var v : m_unsat_vars) {
|
||||
out << v << " ";
|
||||
}
|
||||
out << "\n";
|
||||
return out;
|
||||
}
|
||||
|
||||
void ddfw::invariant() {
|
||||
// every variable in unsat vars is in a false clause.
|
||||
for (bool_var v : m_unsat_vars) {
|
||||
bool found = false;
|
||||
for (unsigned cl : m_unsat) {
|
||||
for (literal lit : get_clause(cl)) {
|
||||
if (lit.var() == v) { found = true; break; }
|
||||
}
|
||||
if (found) break;
|
||||
}
|
||||
if (!found) IF_VERBOSE(0, verbose_stream() << "unsat var not found: " << v << "\n"; );
|
||||
VERIFY(found);
|
||||
}
|
||||
for (unsigned v = 0; v < num_vars(); ++v) {
|
||||
int v_reward = 0;
|
||||
literal lit(v, !value(v));
|
||||
for (unsigned j : m_use_list[lit.index()]) {
|
||||
clause_info const& ci = m_clauses[j];
|
||||
if (ci.m_num_trues == 1) {
|
||||
SASSERT(lit == to_literal(ci.m_trues));
|
||||
v_reward -= ci.m_weight;
|
||||
}
|
||||
}
|
||||
for (unsigned j : m_use_list[(~lit).index()]) {
|
||||
clause_info const& ci = m_clauses[j];
|
||||
if (ci.m_num_trues == 0) {
|
||||
v_reward += ci.m_weight;
|
||||
}
|
||||
}
|
||||
IF_VERBOSE(0, if (v_reward != reward(v)) verbose_stream() << v << " " << v_reward << " " << reward(v) << "\n");
|
||||
SASSERT(reward(v) == v_reward);
|
||||
}
|
||||
for (auto const& ci : m_clauses) {
|
||||
SASSERT(ci.m_weight > 0);
|
||||
}
|
||||
for (unsigned i = 0; i < m_clauses.size(); ++i) {
|
||||
clause_info const& ci = m_clauses[i];
|
||||
bool found = false;
|
||||
for (literal lit : get_clause(i)) {
|
||||
if (is_true(lit)) found = true;
|
||||
}
|
||||
SASSERT(ci.is_true() == found);
|
||||
SASSERT(found == !m_unsat.contains(i));
|
||||
}
|
||||
// every variable in a false clause is in unsat vars
|
||||
for (unsigned cl : m_unsat) {
|
||||
for (literal lit : get_clause(cl)) {
|
||||
SASSERT(m_unsat_vars.contains(lit.var()));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void ddfw::updt_params(params_ref const& _p) {
|
||||
sat_params p(_p);
|
||||
m_config.m_init_clause_weight = p.ddfw_init_clause_weight();
|
||||
m_config.m_use_reward_zero_pct = p.ddfw_use_reward_pct();
|
||||
m_config.m_reinit_base = p.ddfw_reinit_base();
|
||||
m_config.m_restart_base = p.ddfw_restart_base();
|
||||
}
|
||||
|
||||
}
|
||||
|
227
src/sat/sat_ddfw.h
Normal file
227
src/sat/sat_ddfw.h
Normal file
|
@ -0,0 +1,227 @@
|
|||
/*++
|
||||
Copyright (c) 2019 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
sat_ddfw.h
|
||||
|
||||
Abstract:
|
||||
|
||||
DDFW Local search module for clauses
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner, Marijn Heule 2019-4-23
|
||||
|
||||
Notes:
|
||||
|
||||
http://www.ict.griffith.edu.au/~johnt/publications/CP2006raouf.pdf
|
||||
|
||||
--*/
|
||||
#ifndef _SAT_DDFW_
|
||||
#define _SAT_DDFW_
|
||||
|
||||
#include "util/uint_set.h"
|
||||
#include "util/rlimit.h"
|
||||
#include "util/params.h"
|
||||
#include "util/ema.h"
|
||||
#include "sat/sat_clause.h"
|
||||
#include "sat/sat_types.h"
|
||||
|
||||
namespace sat {
|
||||
class solver;
|
||||
class parallel;
|
||||
|
||||
class ddfw : public i_local_search {
|
||||
|
||||
struct clause_info {
|
||||
clause_info(clause* cl, unsigned init_weight): m_weight(init_weight), m_trues(0), m_num_trues(0), m_clause(cl) {}
|
||||
unsigned m_weight; // weight of clause
|
||||
unsigned m_trues; // set of literals that are true
|
||||
unsigned m_num_trues; // size of true set
|
||||
clause* m_clause;
|
||||
bool is_true() const { return m_num_trues > 0; }
|
||||
void add(literal lit) { ++m_num_trues; m_trues += lit.index(); }
|
||||
void del(literal lit) { SASSERT(m_num_trues > 0); --m_num_trues; m_trues -= lit.index(); }
|
||||
};
|
||||
|
||||
struct config {
|
||||
config() { reset(); }
|
||||
unsigned m_use_reward_zero_pct;
|
||||
unsigned m_init_clause_weight;
|
||||
unsigned m_max_num_models;
|
||||
unsigned m_restart_base;
|
||||
unsigned m_reinit_base;
|
||||
unsigned m_parsync_base;
|
||||
double m_itau;
|
||||
void reset() {
|
||||
m_init_clause_weight = 8;
|
||||
m_use_reward_zero_pct = 15;
|
||||
m_max_num_models = (1 << 10);
|
||||
m_restart_base = 100333;
|
||||
m_reinit_base = 10000;
|
||||
m_parsync_base = 333333;
|
||||
m_itau = 0.5;
|
||||
}
|
||||
};
|
||||
|
||||
struct var_info {
|
||||
var_info(): m_value(false), m_reward(0), m_make_count(0), m_bias(0), m_reward_avg(1e-5) {}
|
||||
bool m_value;
|
||||
int m_reward;
|
||||
unsigned m_make_count;
|
||||
int m_bias;
|
||||
ema m_reward_avg;
|
||||
};
|
||||
|
||||
config m_config;
|
||||
reslimit m_limit;
|
||||
clause_allocator m_alloc;
|
||||
svector<clause_info> m_clauses;
|
||||
literal_vector m_assumptions;
|
||||
svector<var_info> m_vars; // var -> info
|
||||
svector<double> m_probs; // var -> probability of flipping
|
||||
svector<double> m_scores; // reward -> score
|
||||
model m_model; // var -> best assignment
|
||||
|
||||
vector<unsigned_vector> m_use_list;
|
||||
unsigned_vector m_flat_use_list;
|
||||
unsigned_vector m_use_list_index;
|
||||
|
||||
indexed_uint_set m_unsat;
|
||||
indexed_uint_set m_unsat_vars; // set of variables that are in unsat clauses
|
||||
random_gen m_rand;
|
||||
unsigned m_num_non_binary_clauses;
|
||||
unsigned m_restart_count, m_reinit_count, m_parsync_count;
|
||||
uint64_t m_restart_next, m_reinit_next, m_parsync_next;
|
||||
uint64_t m_flips, m_last_flips, m_shifts;
|
||||
unsigned m_min_sz;
|
||||
hashtable<unsigned, unsigned_hash, default_eq<unsigned>> m_models;
|
||||
stopwatch m_stopwatch;
|
||||
|
||||
parallel* m_par;
|
||||
|
||||
class use_list {
|
||||
ddfw& p;
|
||||
unsigned i;
|
||||
public:
|
||||
use_list(ddfw& p, literal lit):
|
||||
p(p), i(lit.index()) {}
|
||||
unsigned const* begin() { return p.m_flat_use_list.c_ptr() + p.m_use_list_index[i]; }
|
||||
unsigned const* end() { return p.m_flat_use_list.c_ptr() + p.m_use_list_index[i+1]; }
|
||||
};
|
||||
|
||||
void flatten_use_list();
|
||||
|
||||
double mk_score(unsigned r);
|
||||
|
||||
inline double score(unsigned r) { return r; } // TBD: { for (unsigned sz = m_scores.size(); sz <= r; ++sz) m_scores.push_back(mk_score(sz)); return m_scores[r]; }
|
||||
|
||||
inline unsigned num_vars() const { return m_vars.size(); }
|
||||
|
||||
inline unsigned& make_count(bool_var v) { return m_vars[v].m_make_count; }
|
||||
|
||||
inline bool& value(bool_var v) { return m_vars[v].m_value; }
|
||||
|
||||
inline bool value(bool_var v) const { return m_vars[v].m_value; }
|
||||
|
||||
inline int& reward(bool_var v) { return m_vars[v].m_reward; }
|
||||
|
||||
inline int reward(bool_var v) const { return m_vars[v].m_reward; }
|
||||
|
||||
inline int& bias(bool_var v) { return m_vars[v].m_bias; }
|
||||
|
||||
unsigned value_hash() const;
|
||||
|
||||
inline bool is_true(literal lit) const { return value(lit.var()) != lit.sign(); }
|
||||
|
||||
inline clause const& get_clause(unsigned idx) const { return *m_clauses[idx].m_clause; }
|
||||
|
||||
inline unsigned get_weight(unsigned idx) const { return m_clauses[idx].m_weight; }
|
||||
|
||||
inline bool is_true(unsigned idx) const { return m_clauses[idx].is_true(); }
|
||||
|
||||
void update_reward_avg(bool_var v) { m_vars[v].m_reward_avg.update(reward(v)); }
|
||||
|
||||
unsigned select_max_same_sign(unsigned cf_idx);
|
||||
|
||||
inline void inc_make(literal lit) {
|
||||
bool_var v = lit.var();
|
||||
if (make_count(v)++ == 0) m_unsat_vars.insert(v);
|
||||
}
|
||||
|
||||
inline void dec_make(literal lit) {
|
||||
bool_var v = lit.var();
|
||||
if (--make_count(v) == 0) m_unsat_vars.remove(v);
|
||||
}
|
||||
|
||||
inline void inc_reward(literal lit, int inc) { reward(lit.var()) += inc; }
|
||||
|
||||
inline void dec_reward(literal lit, int inc) { reward(lit.var()) -= inc; }
|
||||
|
||||
// flip activity
|
||||
bool do_flip();
|
||||
bool_var pick_var();
|
||||
void flip(bool_var v);
|
||||
void save_best_values();
|
||||
|
||||
// shift activity
|
||||
void shift_weights();
|
||||
|
||||
// reinitialize weights activity
|
||||
bool should_reinit_weights();
|
||||
void do_reinit_weights();
|
||||
inline bool select_clause(unsigned max_weight, unsigned max_trues, clause_info const& cn, unsigned& n);
|
||||
|
||||
// restart activity
|
||||
bool should_restart();
|
||||
void do_restart();
|
||||
void reinit_values();
|
||||
|
||||
// parallel integration
|
||||
bool should_parallel_sync();
|
||||
void do_parallel_sync();
|
||||
|
||||
void log();
|
||||
|
||||
void init(unsigned sz, literal const* assumptions);
|
||||
|
||||
void init_clause_data();
|
||||
|
||||
void invariant();
|
||||
|
||||
void add(unsigned sz, literal const* c);
|
||||
|
||||
void add_assumptions();
|
||||
|
||||
public:
|
||||
|
||||
ddfw(): m_par(nullptr) {}
|
||||
|
||||
~ddfw() override;
|
||||
|
||||
lbool check(unsigned sz, literal const* assumptions, parallel* p) override;
|
||||
|
||||
void updt_params(params_ref const& p) override;
|
||||
|
||||
model const& get_model() const override { return m_model; }
|
||||
|
||||
reslimit& rlimit() override { return m_limit; }
|
||||
|
||||
void set_seed(unsigned n) override { m_rand.set_seed(n); }
|
||||
|
||||
void add(solver const& s) override;
|
||||
|
||||
std::ostream& display(std::ostream& out) const;
|
||||
|
||||
// for parallel integration
|
||||
unsigned num_non_binary_clauses() const override { return m_num_non_binary_clauses; }
|
||||
void reinit(solver& s) override;
|
||||
|
||||
void collect_statistics(statistics& st) const override {}
|
||||
|
||||
double get_priority(bool_var v) const override { return m_probs[v]; }
|
||||
};
|
||||
}
|
||||
|
||||
#endif
|
|
@ -62,6 +62,7 @@ namespace sat {
|
|||
virtual lbool resolve_conflict() { return l_undef; } // stores result in sat::solver::m_lemma
|
||||
virtual void push() = 0;
|
||||
virtual void pop(unsigned n) = 0;
|
||||
virtual void pre_simplify() = 0;
|
||||
virtual void simplify() = 0;
|
||||
// have a way to replace l by r in all constraints
|
||||
virtual bool set_root(literal l, literal r) { return false; }
|
||||
|
|
|
@ -135,7 +135,6 @@ namespace sat {
|
|||
VERIFY(s.m_decision.size() == s.num_vars());
|
||||
VERIFY(s.m_eliminated.size() == s.num_vars());
|
||||
VERIFY(s.m_external.size() == s.num_vars());
|
||||
VERIFY(s.m_level.size() == s.num_vars());
|
||||
VERIFY(s.m_mark.size() == s.num_vars());
|
||||
VERIFY(s.m_activity.size() == s.num_vars());
|
||||
VERIFY(s.m_phase.size() == s.num_vars());
|
||||
|
|
|
@ -25,17 +25,20 @@ namespace sat {
|
|||
public:
|
||||
enum kind { NONE, BINARY, TERNARY, CLAUSE, EXT_JUSTIFICATION };
|
||||
private:
|
||||
unsigned m_level;
|
||||
size_t m_val1;
|
||||
unsigned m_val2;
|
||||
justification(ext_justification_idx idx, kind k):m_val1(idx), m_val2(k) {}
|
||||
justification(unsigned lvl, ext_justification_idx idx, kind k):m_level(lvl), m_val1(idx), m_val2(k) {}
|
||||
unsigned val1() const { return static_cast<unsigned>(m_val1); }
|
||||
public:
|
||||
justification():m_val1(0), m_val2(NONE) {}
|
||||
explicit justification(literal l):m_val1(l.to_uint()), m_val2(BINARY) {}
|
||||
justification(literal l1, literal l2):m_val1(l1.to_uint()), m_val2(TERNARY + (l2.to_uint() << 3)) {}
|
||||
explicit justification(clause_offset cls_off):m_val1(cls_off), m_val2(CLAUSE) {}
|
||||
static justification mk_ext_justification(ext_justification_idx idx) { return justification(idx, EXT_JUSTIFICATION); }
|
||||
justification(unsigned lvl):m_level(lvl), m_val1(0), m_val2(NONE) {}
|
||||
explicit justification(unsigned lvl, literal l):m_level(lvl), m_val1(l.to_uint()), m_val2(BINARY) {}
|
||||
justification(unsigned lvl, literal l1, literal l2):m_level(lvl), m_val1(l1.to_uint()), m_val2(TERNARY + (l2.to_uint() << 3)) {}
|
||||
explicit justification(unsigned lvl, clause_offset cls_off):m_level(lvl), m_val1(cls_off), m_val2(CLAUSE) {}
|
||||
static justification mk_ext_justification(unsigned lvl, ext_justification_idx idx) { return justification(lvl, idx, EXT_JUSTIFICATION); }
|
||||
|
||||
unsigned level() const { return m_level; }
|
||||
|
||||
kind get_kind() const { return static_cast<kind>(m_val2 & 7); }
|
||||
|
||||
bool is_none() const { return m_val2 == NONE; }
|
||||
|
@ -72,6 +75,7 @@ namespace sat {
|
|||
out << "external";
|
||||
break;
|
||||
}
|
||||
out << " @" << j.level();
|
||||
return out;
|
||||
}
|
||||
};
|
||||
|
|
|
@ -216,10 +216,10 @@ namespace sat {
|
|||
|
||||
void local_search::set_best_unsat() {
|
||||
m_best_unsat = m_unsat_stack.size();
|
||||
if (m_best_unsat == 1) {
|
||||
constraint const& c = m_constraints[m_unsat_stack[0]];
|
||||
IF_VERBOSE(2, display(verbose_stream() << "single unsat:", c));
|
||||
}
|
||||
m_best_phase.reserve(m_vars.size());
|
||||
for (unsigned i = m_vars.size(); i-- > 0; ) {
|
||||
m_best_phase[i] = m_vars[i].m_value;
|
||||
}
|
||||
}
|
||||
|
||||
void local_search::verify_solution() const {
|
||||
|
@ -351,7 +351,16 @@ namespace sat {
|
|||
m_par(nullptr) {
|
||||
}
|
||||
|
||||
void local_search::import(solver& s, bool _init) {
|
||||
void local_search::reinit(solver& s) {
|
||||
import(s, true);
|
||||
if (s.m_best_phase_size > 0) {
|
||||
for (unsigned i = num_vars(); i-- > 0; ) {
|
||||
set_phase(i, s.m_best_phase[i]);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void local_search::import(solver const& s, bool _init) {
|
||||
flet<bool> linit(m_initializing, true);
|
||||
m_is_pb = false;
|
||||
m_vars.reset();
|
||||
|
@ -364,7 +373,7 @@ namespace sat {
|
|||
if (m_config.phase_sticky()) {
|
||||
unsigned v = 0;
|
||||
for (var_info& vi : m_vars) {
|
||||
vi.m_bias = s.m_phase[v++] == POS_PHASE ? 98 : 2;
|
||||
vi.m_bias = s.m_phase[v++] ? 98 : 2;
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -495,7 +504,7 @@ namespace sat {
|
|||
|
||||
|
||||
lbool local_search::check() {
|
||||
return check(0, nullptr);
|
||||
return check(0, nullptr, nullptr);
|
||||
}
|
||||
|
||||
#define PROGRESS(tries, flips) \
|
||||
|
@ -530,7 +539,25 @@ namespace sat {
|
|||
}
|
||||
total_flips += step;
|
||||
PROGRESS(tries, total_flips);
|
||||
if (m_par && m_par->get_phase(*this)) {
|
||||
if (m_par) {
|
||||
double max_avg = 0;
|
||||
for (unsigned v = 0; v < num_vars(); ++v) {
|
||||
max_avg = std::max(max_avg, (double)m_vars[v].m_slow_break);
|
||||
}
|
||||
double sum = 0;
|
||||
for (unsigned v = 0; v < num_vars(); ++v) {
|
||||
sum += exp(m_config.itau() * (m_vars[v].m_slow_break - max_avg));
|
||||
}
|
||||
if (sum == 0) {
|
||||
sum = 0.01;
|
||||
}
|
||||
for (unsigned v = 0; v < num_vars(); ++v) {
|
||||
m_vars[v].m_break_prob = exp(m_config.itau() * (m_vars[v].m_slow_break - max_avg)) / sum;
|
||||
}
|
||||
|
||||
m_par->to_solver(*this);
|
||||
}
|
||||
if (m_par && m_par->from_solver(*this)) {
|
||||
reinit();
|
||||
}
|
||||
if (tries % 10 == 0 && !m_unsat_stack.empty()) {
|
||||
|
@ -834,11 +861,10 @@ namespace sat {
|
|||
}
|
||||
|
||||
|
||||
void local_search::set_phase(bool_var v, lbool f) {
|
||||
void local_search::set_phase(bool_var v, bool f) {
|
||||
unsigned& bias = m_vars[v].m_bias;
|
||||
if (f == l_true && bias < 100) bias++;
|
||||
if (f == l_false && bias > 0) bias--;
|
||||
// f == l_undef ?
|
||||
if (f && bias < 100) bias++;
|
||||
if (!f && bias > 0) bias--;
|
||||
}
|
||||
|
||||
void local_search::set_bias(bool_var v, lbool f) {
|
||||
|
|
|
@ -36,6 +36,7 @@ namespace sat {
|
|||
local_search_mode m_mode;
|
||||
bool m_phase_sticky;
|
||||
bool m_dbg_flips;
|
||||
double m_itau;
|
||||
|
||||
friend class local_search;
|
||||
|
||||
|
@ -53,6 +54,7 @@ namespace sat {
|
|||
m_mode = local_search_mode::wsat;
|
||||
m_phase_sticky = false;
|
||||
m_dbg_flips = false;
|
||||
m_itau = 0.5;
|
||||
}
|
||||
|
||||
unsigned random_seed() const { return m_random_seed; }
|
||||
|
@ -60,6 +62,7 @@ namespace sat {
|
|||
local_search_mode mode() const { return m_mode; }
|
||||
bool phase_sticky() const { return m_phase_sticky; }
|
||||
bool dbg_flips() const { return m_dbg_flips; }
|
||||
double itau() const { return m_itau; }
|
||||
|
||||
void set_random_seed(unsigned s) { m_random_seed = s; }
|
||||
void set_best_known_value(unsigned v) { m_best_known_value = v; }
|
||||
|
@ -67,7 +70,7 @@ namespace sat {
|
|||
};
|
||||
|
||||
|
||||
class local_search {
|
||||
class local_search : public i_local_search {
|
||||
|
||||
struct pbcoeff {
|
||||
unsigned m_constraint_id;
|
||||
|
@ -102,6 +105,7 @@ namespace sat {
|
|||
literal_vector m_bin[2];
|
||||
unsigned m_flips;
|
||||
ema m_slow_break;
|
||||
double m_break_prob;
|
||||
var_info():
|
||||
m_value(true),
|
||||
m_bias(50),
|
||||
|
@ -111,7 +115,8 @@ namespace sat {
|
|||
m_score(0),
|
||||
m_slack_score(0),
|
||||
m_flips(0),
|
||||
m_slow_break(1e-5)
|
||||
m_slow_break(1e-5),
|
||||
m_break_prob(0)
|
||||
{}
|
||||
};
|
||||
|
||||
|
@ -134,6 +139,7 @@ namespace sat {
|
|||
local_search_config m_config;
|
||||
|
||||
vector<var_info> m_vars; // variables
|
||||
svector<bool> m_best_phase; // best value in round
|
||||
svector<bool_var> m_units; // unit clauses
|
||||
vector<constraint> m_constraints; // all constraints
|
||||
literal_vector m_assumptions; // temporary assumptions
|
||||
|
@ -167,7 +173,6 @@ namespace sat {
|
|||
parallel* m_par;
|
||||
model m_model;
|
||||
|
||||
|
||||
inline int score(bool_var v) const { return m_vars[v].m_score; }
|
||||
inline void inc_score(bool_var v) { m_vars[v].m_score++; }
|
||||
inline void dec_score(bool_var v) { m_vars[v].m_score--; }
|
||||
|
@ -223,48 +228,58 @@ namespace sat {
|
|||
void extract_model();
|
||||
void add_clause(unsigned sz, literal const* c);
|
||||
void add_unit(literal lit, literal explain);
|
||||
|
||||
std::ostream& display(std::ostream& out) const;
|
||||
std::ostream& display(std::ostream& out, constraint const& c) const;
|
||||
std::ostream& display(std::ostream& out, unsigned v, var_info const& vi) const;
|
||||
|
||||
lbool check();
|
||||
|
||||
unsigned num_vars() const { return m_vars.size() - 1; } // var index from 1 to num_vars
|
||||
|
||||
public:
|
||||
|
||||
local_search();
|
||||
|
||||
reslimit& rlimit() { return m_limit; }
|
||||
~local_search() override;
|
||||
|
||||
reslimit& rlimit() override { return m_limit; }
|
||||
|
||||
~local_search();
|
||||
lbool check(unsigned sz, literal const* assumptions, parallel* p) override;
|
||||
|
||||
unsigned num_non_binary_clauses() const override { return m_num_non_binary_clauses; }
|
||||
|
||||
void add(solver const& s) override { import(s, false); }
|
||||
|
||||
model const& get_model() const override { return m_model; }
|
||||
|
||||
void collect_statistics(statistics& st) const override;
|
||||
|
||||
void updt_params(params_ref const& p) override {}
|
||||
|
||||
void set_seed(unsigned n) override { config().set_random_seed(n); }
|
||||
|
||||
void reinit(solver& s) override;
|
||||
|
||||
// used by unit-walk
|
||||
void set_phase(bool_var v, bool f);
|
||||
|
||||
void set_bias(bool_var v, lbool f);
|
||||
|
||||
bool get_best_phase(bool_var v) const { return m_best_phase[v]; }
|
||||
|
||||
inline bool cur_solution(bool_var v) const { return m_vars[v].m_value; }
|
||||
|
||||
double get_priority(bool_var v) const override { return m_vars[v].m_break_prob; }
|
||||
|
||||
void import(solver const& s, bool init);
|
||||
|
||||
void add_cardinality(unsigned sz, literal const* c, unsigned k);
|
||||
|
||||
void add_pb(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k);
|
||||
|
||||
lbool check();
|
||||
|
||||
lbool check(unsigned sz, literal const* assumptions, parallel* p = nullptr);
|
||||
|
||||
local_search_config& config() { return m_config; }
|
||||
|
||||
unsigned num_vars() const { return m_vars.size() - 1; } // var index from 1 to num_vars
|
||||
|
||||
unsigned num_non_binary_clauses() const { return m_num_non_binary_clauses; }
|
||||
|
||||
void import(solver& s, bool init);
|
||||
|
||||
void set_phase(bool_var v, lbool f);
|
||||
|
||||
void set_bias(bool_var v, lbool f);
|
||||
|
||||
bool get_phase(bool_var v) const { return is_true(v); }
|
||||
|
||||
inline bool cur_solution(bool_var v) const { return m_vars[v].m_value; }
|
||||
|
||||
double break_count(bool_var v) const { return m_vars[v].m_slow_break; }
|
||||
|
||||
model& get_model() { return m_model; }
|
||||
|
||||
void collect_statistics(statistics& st) const;
|
||||
|
||||
};
|
||||
}
|
||||
|
||||
|
|
|
@ -102,7 +102,6 @@ namespace sat {
|
|||
literal l = lits.back();
|
||||
lits.pop_back();
|
||||
SASSERT(!m_binary[(~l).index()].empty());
|
||||
IF_VERBOSE(0, if (m_binary[(~l).index()].back() != ~to_literal(idx)) verbose_stream() << "pop bad literal: " << idx << " " << (~l).index() << "\n";);
|
||||
SASSERT(m_binary[(~l).index()].back() == ~to_literal(idx));
|
||||
m_binary[(~l).index()].pop_back();
|
||||
++m_stats.m_del_binary;
|
||||
|
@ -1655,6 +1654,77 @@ namespace sat {
|
|||
return result;
|
||||
}
|
||||
|
||||
void lookahead::get_clauses(literal_vector& clauses, unsigned max_clause_size) {
|
||||
// push binary clauses
|
||||
unsigned num_lits = m_s.num_vars() * 2;
|
||||
for (unsigned idx = 0; idx < num_lits; ++idx) {
|
||||
literal u = to_literal(idx);
|
||||
if (m_s.was_eliminated(u.var()) || is_false(u) || is_true(u)) continue;
|
||||
for (literal v : m_binary[idx]) {
|
||||
if (u.index() < v.index() && !m_s.was_eliminated(v.var()) && !is_false(v) && !is_true(v)) {
|
||||
clauses.push_back(~u);
|
||||
clauses.push_back(v);
|
||||
clauses.push_back(null_literal);
|
||||
}
|
||||
}
|
||||
}
|
||||
// push ternary clauses
|
||||
for (unsigned idx = 0; idx < num_lits; ++idx) {
|
||||
literal u = to_literal(idx);
|
||||
if (is_true(u) || is_false(u)) continue;
|
||||
unsigned sz = m_ternary_count[u.index()];
|
||||
for (binary const& b : m_ternary[u.index()]) {
|
||||
if (sz-- == 0) break;
|
||||
if (u.index() > b.m_v.index() || u.index() > b.m_u.index())
|
||||
continue;
|
||||
if (is_true(b.m_u) || is_true(b.m_v))
|
||||
continue;
|
||||
if (is_false(b.m_u) && is_false(b.m_v))
|
||||
continue;
|
||||
clauses.push_back(u);
|
||||
if (!is_false(b.m_u)) clauses.push_back(b.m_u);
|
||||
if (!is_false(b.m_v)) clauses.push_back(b.m_v);
|
||||
clauses.push_back(null_literal);
|
||||
}
|
||||
}
|
||||
|
||||
// push n-ary clauses
|
||||
for (unsigned idx = 0; idx < num_lits; ++idx) {
|
||||
literal u = to_literal(idx);
|
||||
unsigned sz = m_nary_count[u.index()];
|
||||
for (nary* n : m_nary[u.index()]) {
|
||||
if (sz-- == 0) break;
|
||||
unsigned sz0 = clauses.size();
|
||||
if (n->size() > max_clause_size) continue;
|
||||
for (literal lit : *n) {
|
||||
if (is_true(lit)) {
|
||||
clauses.shrink(sz0);
|
||||
break;
|
||||
}
|
||||
if (!is_false(lit)) {
|
||||
clauses.push_back(lit);
|
||||
}
|
||||
}
|
||||
if (clauses.size() > sz0) {
|
||||
clauses.push_back(null_literal);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
TRACE("sat",
|
||||
for (literal lit : clauses) {
|
||||
if (lit == null_literal) {
|
||||
tout << "\n";
|
||||
}
|
||||
else {
|
||||
tout << lit << " ";
|
||||
}
|
||||
}
|
||||
tout << "\n";
|
||||
m_s.display(tout);
|
||||
);
|
||||
}
|
||||
|
||||
void lookahead::propagate_binary(literal l) {
|
||||
literal_vector const& lits = m_binary[l.index()];
|
||||
TRACE("sat", tout << l << " => " << lits << "\n";);
|
||||
|
@ -1687,10 +1757,14 @@ namespace sat {
|
|||
unsigned base = 2;
|
||||
bool change = true;
|
||||
literal last_changed = null_literal;
|
||||
while (change && !inconsistent()) {
|
||||
unsigned ops = 0;
|
||||
m_max_ops = 100000;
|
||||
while (change && !inconsistent() && ops < m_max_ops) {
|
||||
change = false;
|
||||
for (unsigned i = 0; !inconsistent() && i < m_lookahead.size(); ++i) {
|
||||
IF_VERBOSE(10, verbose_stream() << "(sat.lookahead :compute-reward " << m_lookahead.size() << ")\n");
|
||||
for (unsigned i = 0; !inconsistent() && i < m_lookahead.size() && ops < m_max_ops; ++i) {
|
||||
checkpoint();
|
||||
++ops;
|
||||
literal lit = m_lookahead[i].m_lit;
|
||||
if (lit == last_changed) {
|
||||
SASSERT(!change);
|
||||
|
@ -1714,13 +1788,11 @@ namespace sat {
|
|||
num_units += do_double(lit, dl_lvl);
|
||||
if (dl_lvl > level) {
|
||||
base = dl_lvl;
|
||||
//SASSERT(get_level(m_trail.back()) == base + m_lookahead[i].m_offset);
|
||||
SASSERT(get_level(m_trail.back()) == base);
|
||||
}
|
||||
unsat = inconsistent();
|
||||
pop_lookahead1(lit, num_units);
|
||||
}
|
||||
// VERIFY(!missed_propagation());
|
||||
if (unsat) {
|
||||
TRACE("sat", tout << "backtracking and setting " << ~lit << "\n";);
|
||||
lookahead_backtrack();
|
||||
|
@ -2165,6 +2237,29 @@ namespace sat {
|
|||
return l_undef;
|
||||
}
|
||||
|
||||
|
||||
void lookahead::display_lookahead_scores(std::ostream& out) {
|
||||
scoped_ext _scoped_ext(*this);
|
||||
m_select_lookahead_vars.reset();
|
||||
init_search();
|
||||
scoped_level _sl(*this, c_fixed_truth);
|
||||
m_search_mode = lookahead_mode::searching;
|
||||
literal l = choose_base();
|
||||
if (l == null_literal) {
|
||||
out << "null\n";
|
||||
return;
|
||||
}
|
||||
for (auto const& l : m_lookahead) {
|
||||
literal lit = l.m_lit;
|
||||
if (!lit.sign() && is_undef(lit)) {
|
||||
double diff1 = get_lookahead_reward(lit);
|
||||
double diff2 = get_lookahead_reward(~lit);
|
||||
out << lit << " " << diff1 << " " << diff2 << "\n";
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
void lookahead::init_model() {
|
||||
m_model.reset();
|
||||
for (unsigned i = 0; i < m_num_vars; ++i) {
|
||||
|
@ -2255,7 +2350,13 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
literal lookahead::choose() {
|
||||
return choose_base();
|
||||
}
|
||||
|
||||
literal lookahead::choose_base() {
|
||||
literal l = null_literal;
|
||||
while (l == null_literal && !inconsistent()) {
|
||||
pre_select();
|
||||
|
@ -2284,7 +2385,7 @@ namespace sat {
|
|||
init(learned);
|
||||
if (inconsistent()) return;
|
||||
inc_istamp();
|
||||
choose();
|
||||
choose_base();
|
||||
if (inconsistent()) return;
|
||||
SASSERT(m_trail_lim.empty());
|
||||
unsigned num_units = 0;
|
||||
|
|
|
@ -20,9 +20,9 @@ Notes:
|
|||
#ifndef _SAT_LOOKAHEAD_H_
|
||||
#define _SAT_LOOKAHEAD_H_
|
||||
|
||||
// #define OLD_NARY 0
|
||||
|
||||
#include "sat_elim_eqs.h"
|
||||
#include "util/small_object_allocator.h"
|
||||
#include "sat/sat_elim_eqs.h"
|
||||
|
||||
namespace sat {
|
||||
|
||||
|
@ -247,6 +247,7 @@ namespace sat {
|
|||
stats m_stats;
|
||||
model m_model;
|
||||
cube_state m_cube_state;
|
||||
unsigned m_max_ops; // cap number of operations used to compute lookahead reward.
|
||||
//scoped_ptr<extension> m_ext;
|
||||
|
||||
// ---------------------------------------
|
||||
|
@ -510,6 +511,7 @@ namespace sat {
|
|||
void propagate_binary(literal l);
|
||||
void propagate();
|
||||
literal choose();
|
||||
literal choose_base();
|
||||
void compute_lookahead_reward();
|
||||
literal select_literal();
|
||||
void update_binary_clause_reward(literal l1, literal l2);
|
||||
|
@ -605,6 +607,13 @@ namespace sat {
|
|||
|
||||
std::ostream& display(std::ostream& out) const;
|
||||
std::ostream& display_summary(std::ostream& out) const;
|
||||
|
||||
/**
|
||||
\brief display lookahead scores as a sequence of:
|
||||
<variable_id:uint> <true_branch_score:double> <false_branch_score:double>\n
|
||||
*/
|
||||
void display_lookahead_scores(std::ostream& out);
|
||||
|
||||
model const& get_model();
|
||||
|
||||
void collect_statistics(statistics& st) const;
|
||||
|
@ -612,6 +621,12 @@ namespace sat {
|
|||
double literal_occs(literal l);
|
||||
double literal_big_occs(literal l);
|
||||
|
||||
/**
|
||||
\brief retrieve clauses as one vector of literals.
|
||||
clauses are separated by null-literal
|
||||
*/
|
||||
void get_clauses(literal_vector& clauses, unsigned max_clause_size);
|
||||
|
||||
sat::config const& get_config() const { return m_s.get_config(); }
|
||||
|
||||
};
|
||||
|
|
|
@ -16,10 +16,9 @@ Author:
|
|||
Revision History:
|
||||
|
||||
--*/
|
||||
#include "sat_parallel.h"
|
||||
#include "sat_clause.h"
|
||||
#include "sat_solver.h"
|
||||
|
||||
#include "sat/sat_parallel.h"
|
||||
#include "sat/sat_clause.h"
|
||||
#include "sat/sat_solver.h"
|
||||
|
||||
namespace sat {
|
||||
|
||||
|
@ -205,27 +204,7 @@ namespace sat {
|
|||
return (c.size() <= 40 && c.glue() <= 8) || c.glue() <= 2;
|
||||
}
|
||||
|
||||
void parallel::_set_phase(solver& s) {
|
||||
if (!m_phase.empty()) {
|
||||
m_phase.reserve(s.num_vars(), l_undef);
|
||||
for (unsigned i = 0; i < s.num_vars(); ++i) {
|
||||
if (s.value(i) != l_undef) {
|
||||
m_phase[i] = s.value(i);
|
||||
continue;
|
||||
}
|
||||
switch (s.m_phase[i]) {
|
||||
case POS_PHASE:
|
||||
m_phase[i] = l_true;
|
||||
break;
|
||||
case NEG_PHASE:
|
||||
m_phase[i] = l_false;
|
||||
break;
|
||||
default:
|
||||
m_phase[i] = l_undef;
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
void parallel::_from_solver(solver& s) {
|
||||
if (m_consumer_ready && (m_num_clauses == 0 || (m_num_clauses > s.m_clauses.size()))) {
|
||||
// time to update local search with new clauses.
|
||||
// there could be multiple local search engines running at the same time.
|
||||
|
@ -236,47 +215,53 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
|
||||
void parallel::set_phase(solver& s) {
|
||||
std::lock_guard<std::mutex> lock(m_mux);
|
||||
_set_phase(s);
|
||||
|
||||
bool parallel::_to_solver(solver& s) {
|
||||
if (m_priorities.empty()) {
|
||||
return false;
|
||||
}
|
||||
for (bool_var v = 0; v < m_priorities.size(); ++v) {
|
||||
s.update_activity(v, m_priorities[v]);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
void parallel::get_phase(solver& s) {
|
||||
void parallel::from_solver(solver& s) {
|
||||
std::lock_guard<std::mutex> lock(m_mux);
|
||||
_get_phase(s);
|
||||
_from_solver(s);
|
||||
}
|
||||
|
||||
void parallel::_get_phase(solver& s) {
|
||||
if (!m_phase.empty()) {
|
||||
m_phase.reserve(s.num_vars(), l_undef);
|
||||
for (unsigned i = 0; i < s.num_vars(); ++i) {
|
||||
switch (m_phase[i]) {
|
||||
case l_false: s.m_phase[i] = NEG_PHASE; break;
|
||||
case l_true: s.m_phase[i] = POS_PHASE; break;
|
||||
default: break;
|
||||
}
|
||||
}
|
||||
bool parallel::to_solver(solver& s) {
|
||||
std::lock_guard<std::mutex> lock(m_mux);
|
||||
return _to_solver(s);
|
||||
}
|
||||
|
||||
void parallel::_to_solver(i_local_search& s) {
|
||||
m_priorities.reset();
|
||||
for (bool_var v = 0; m_solver_copy && v < m_solver_copy->num_vars(); ++v) {
|
||||
m_priorities.push_back(s.get_priority(v));
|
||||
}
|
||||
}
|
||||
|
||||
bool parallel::get_phase(local_search& s) {
|
||||
bool parallel::_from_solver(i_local_search& s) {
|
||||
bool copied = false;
|
||||
{
|
||||
std::lock_guard<std::mutex> lock(m_mux);
|
||||
m_consumer_ready = true;
|
||||
if (m_solver_copy && s.num_non_binary_clauses() > m_solver_copy->m_clauses.size()) {
|
||||
copied = true;
|
||||
s.import(*m_solver_copy.get(), true);
|
||||
}
|
||||
for (unsigned i = 0; i < m_phase.size(); ++i) {
|
||||
s.set_phase(i, m_phase[i]);
|
||||
m_phase[i] = l_undef;
|
||||
}
|
||||
m_phase.reserve(s.num_vars(), l_undef);
|
||||
m_consumer_ready = true;
|
||||
if (m_solver_copy) {
|
||||
copied = true;
|
||||
s.reinit(*m_solver_copy.get());
|
||||
}
|
||||
return copied;
|
||||
}
|
||||
|
||||
bool parallel::from_solver(i_local_search& s) {
|
||||
std::lock_guard<std::mutex> lock(m_mux);
|
||||
return _from_solver(s);
|
||||
}
|
||||
|
||||
void parallel::to_solver(i_local_search& s) {
|
||||
std::lock_guard<std::mutex> lock(m_mux);
|
||||
_to_solver(s);
|
||||
}
|
||||
|
||||
bool parallel::copy_solver(solver& s) {
|
||||
bool copied = false;
|
||||
|
|
|
@ -28,8 +28,6 @@ Revision History:
|
|||
|
||||
namespace sat {
|
||||
|
||||
class local_search;
|
||||
|
||||
class parallel {
|
||||
|
||||
// shared pool of learned clauses.
|
||||
|
@ -54,8 +52,10 @@ namespace sat {
|
|||
|
||||
bool enable_add(clause const& c) const;
|
||||
void _get_clauses(solver& s);
|
||||
void _get_phase(solver& s);
|
||||
void _set_phase(solver& s);
|
||||
void _from_solver(solver& s);
|
||||
bool _to_solver(solver& s);
|
||||
bool _from_solver(i_local_search& s);
|
||||
void _to_solver(i_local_search& s);
|
||||
|
||||
typedef hashtable<unsigned, u_hash, u_eq> index_set;
|
||||
literal_vector m_units;
|
||||
|
@ -65,10 +65,10 @@ namespace sat {
|
|||
std::mutex m_mux;
|
||||
|
||||
// for exchange with local search:
|
||||
svector<lbool> m_phase;
|
||||
unsigned m_num_clauses;
|
||||
scoped_ptr<solver> m_solver_copy;
|
||||
bool m_consumer_ready;
|
||||
svector<double> m_priorities;
|
||||
|
||||
scoped_limits m_scoped_rlimit;
|
||||
vector<reslimit> m_limits;
|
||||
|
@ -102,13 +102,13 @@ namespace sat {
|
|||
// receive clauses from shared clause pool
|
||||
void get_clauses(solver& s);
|
||||
|
||||
// exchange phase of variables.
|
||||
void set_phase(solver& s);
|
||||
|
||||
void get_phase(solver& s);
|
||||
// exchange from solver state to local search and back.
|
||||
void from_solver(solver& s);
|
||||
bool to_solver(solver& s);
|
||||
|
||||
bool from_solver(i_local_search& s);
|
||||
void to_solver(i_local_search& s);
|
||||
|
||||
bool get_phase(local_search& s);
|
||||
|
||||
bool copy_solver(solver& s);
|
||||
};
|
||||
|
||||
|
|
|
@ -2,10 +2,11 @@ def_module_params('sat',
|
|||
export=True,
|
||||
description='propositional SAT solver',
|
||||
params=(max_memory_param(),
|
||||
('phase', SYMBOL, 'caching', 'phase selection strategy: always_false, always_true, caching, random'),
|
||||
('phase.caching.on', UINT, 400, 'phase caching on period (in number of conflicts)'),
|
||||
('phase.caching.off', UINT, 100, 'phase caching off period (in number of conflicts)'),
|
||||
('phase.sticky', BOOL, False, 'use sticky phase caching for local search'),
|
||||
('phase', SYMBOL, 'caching', 'phase selection strategy: always_false, always_true, basic_caching, random, caching'),
|
||||
('phase.sticky', BOOL, True, 'use sticky phase caching'),
|
||||
('search.unsat.conflicts', UINT, 400, 'period for solving for unsat (in number of conflicts)'),
|
||||
('search.sat.conflicts', UINT, 400, 'period for solving for sat (in number of conflicts)'),
|
||||
('rephase.base', UINT, 1000, 'number of conflicts per rephase '),
|
||||
('propagate.prefetch', BOOL, True, 'prefetch watch lists for assigned literals'),
|
||||
('restart', SYMBOL, 'ema', 'restart strategy: static, luby, ema or geometric'),
|
||||
('restart.initial', UINT, 2, 'initial restart (number of conflicts)'),
|
||||
|
@ -36,6 +37,8 @@ def_module_params('sat',
|
|||
('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'),
|
||||
('core.minimize', BOOL, False, 'minimize computed core'),
|
||||
('core.minimize_partial', BOOL, False, 'apply partial (cheap) core minimization'),
|
||||
('backtrack.scopes', UINT, 100, 'number of scopes to enable chronological backtracking'),
|
||||
('backtrack.conflicts', UINT, 4000, 'number of conflicts before enabling chronological backtracking'),
|
||||
('threads', UINT, 1, 'number of parallel threads to use'),
|
||||
('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'),
|
||||
('drat.file', SYMBOL, '', 'file to dump DRAT proofs'),
|
||||
|
@ -48,12 +51,20 @@ def_module_params('sat',
|
|||
('cardinality.encoding', SYMBOL, 'grouped', 'encoding used for at-most-k constraints: grouped, bimander, ordered, unate, circuit'),
|
||||
('pb.resolve', SYMBOL, 'cardinality', 'resolution strategy for boolean algebra solver: cardinality, rounding'),
|
||||
('pb.lemma_format', SYMBOL, 'cardinality', 'generate either cardinality or pb lemmas'),
|
||||
('ddfw_search', BOOL, False, 'use ddfw local search instead of CDCL'),
|
||||
('ddfw.init_clause_weight', UINT, 8, 'initial clause weight for DDFW local search'),
|
||||
('ddfw.use_reward_pct', UINT, 15, 'percentage to pick highest reward variable when it has reward 0'),
|
||||
('ddfw.restart_base', UINT, 100000, 'number of flips used a starting point for hessitant restart backoff'),
|
||||
('ddfw.reinit_base', UINT, 10000, 'increment basis for geometric backoff scheme of re-initialization of weights'),
|
||||
('ddfw.threads', UINT, 0, 'number of ddfw threads to run in parallel with sat solver'),
|
||||
('prob_search', BOOL, False, 'use probsat local search instead of CDCL'),
|
||||
('local_search', BOOL, False, 'use local search instead of CDCL'),
|
||||
('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'),
|
||||
('local_search_mode', SYMBOL, 'wsat', 'local search algorithm, either default wsat or qsat'),
|
||||
('local_search_dbg_flips', BOOL, False, 'write debug information for number of flips'),
|
||||
('unit_walk', BOOL, False, 'use unit-walk search instead of CDCL'),
|
||||
('unit_walk_threads', UINT, 0, 'number of unit-walk search threads to find satisfiable solution'),
|
||||
('binspr', BOOL, False, 'enable SPR inferences of binary propagation redundant clauses. This inprocessing step eliminates models'),
|
||||
('lookahead.cube.cutoff', SYMBOL, 'depth', 'cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat'),
|
||||
# - depth: the maximal cutoff is fixed to the value of lookahead.cube.depth.
|
||||
# So if the value is 10, at most 1024 cubes will be generated of length 10.
|
||||
|
@ -64,6 +75,7 @@ def_module_params('sat',
|
|||
# - adaptive_freevars: Cut if the number of current unassigned variables drops below a fraction of free variables
|
||||
# at the time of the last conflict. The fraction is increased every time the cutoff is created.
|
||||
# - adative_psat: Cut based on psat_heur in an adaptive way.
|
||||
|
||||
('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. Used when lookahead.cube.cutoff is adaptive_freevars or adaptive_psat'),
|
||||
('lookahead.cube.depth', UINT, 1, 'cut-off depth to create cubes. Used when lookahead.cube.cutoff is depth.'),
|
||||
('lookahead.cube.freevars', DOUBLE, 0.8, 'cube free variable fraction. Used when lookahead.cube.cutoff is freevars'),
|
||||
|
@ -72,6 +84,7 @@ def_module_params('sat',
|
|||
('lookahead.cube.psat.trigger', DOUBLE, 5, 'trigger value to create lookahead cubes for PSAT cutoff. Used when lookahead.cube.cutoff is psat'),
|
||||
('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'),
|
||||
('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'),
|
||||
('lookahead_scores', BOOL, False, 'extract lookahead scores. A utility that can only be used from the DIMACS front-end'),
|
||||
('lookahead.double', BOOL, True, 'enable doubld lookahead'),
|
||||
('lookahead.use_learned', BOOL, False, 'use learned clauses when selecting lookahead literal'),
|
||||
('lookahead_simplify.bca', BOOL, True, 'add learned binary clauses as part of lookahead simplification'),
|
||||
|
|
296
src/sat/sat_prob.cpp
Normal file
296
src/sat/sat_prob.cpp
Normal file
|
@ -0,0 +1,296 @@
|
|||
/*++
|
||||
Copyright (c) 2019 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
sat_prob.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
PROB Local search module for clauses
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner 2019-4-23
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
|
||||
#include "sat/sat_prob.h"
|
||||
#include "sat/sat_solver.h"
|
||||
#include "util/luby.h"
|
||||
|
||||
namespace sat {
|
||||
|
||||
prob::~prob() {
|
||||
for (clause* cp : m_clause_db) {
|
||||
m_alloc.del_clause(cp);
|
||||
}
|
||||
}
|
||||
|
||||
lbool prob::check(unsigned n, literal const* assumptions, parallel* p) {
|
||||
VERIFY(n == 0);
|
||||
init();
|
||||
while (m_limit.inc() && m_best_min_unsat > 0) {
|
||||
if (should_restart()) do_restart();
|
||||
else flip();
|
||||
}
|
||||
if (m_best_min_unsat == 0) {
|
||||
return l_true;
|
||||
}
|
||||
return l_undef;
|
||||
}
|
||||
|
||||
void prob::flip() {
|
||||
bool_var v = pick_var();
|
||||
flip(v);
|
||||
if (m_unsat.size() < m_best_min_unsat) {
|
||||
save_best_values();
|
||||
}
|
||||
}
|
||||
|
||||
bool_var prob::pick_var() {
|
||||
unsigned cls_idx = m_unsat.elem_at(m_rand() % m_unsat.size());
|
||||
double sum_prob = 0;
|
||||
unsigned i = 0;
|
||||
clause const& c = get_clause(cls_idx);
|
||||
for (literal lit : c) {
|
||||
double prob = m_prob_break[m_breaks[lit.var()]];
|
||||
m_probs[i++] = prob;
|
||||
sum_prob += prob;
|
||||
}
|
||||
double lim = sum_prob * ((double)m_rand() / m_rand.max_value());
|
||||
do {
|
||||
lim -= m_probs[--i];
|
||||
}
|
||||
while (lim >= 0 && i > 0);
|
||||
return c[i].var();
|
||||
}
|
||||
|
||||
void prob::flip(bool_var v) {
|
||||
++m_flips;
|
||||
literal lit = literal(v, !m_values[v]);
|
||||
literal nlit = ~lit;
|
||||
SASSERT(is_true(lit));
|
||||
for (unsigned cls_idx : use_list(*this, lit)) {
|
||||
clause_info& ci = m_clauses[cls_idx];
|
||||
ci.del(lit);
|
||||
switch (ci.m_num_trues) {
|
||||
case 0:
|
||||
m_unsat.insert(cls_idx);
|
||||
dec_break(lit);
|
||||
break;
|
||||
case 1:
|
||||
inc_break(to_literal(ci.m_trues));
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
}
|
||||
for (unsigned cls_idx : use_list(*this, nlit)) {
|
||||
clause_info& ci = m_clauses[cls_idx];
|
||||
switch (ci.m_num_trues) {
|
||||
case 0:
|
||||
m_unsat.remove(cls_idx);
|
||||
inc_break(nlit);
|
||||
break;
|
||||
case 1:
|
||||
dec_break(to_literal(ci.m_trues));
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
ci.add(nlit);
|
||||
}
|
||||
m_values[v] = !m_values[v];
|
||||
}
|
||||
|
||||
void prob::add(unsigned n, literal const* c) {
|
||||
clause* cls = m_alloc.mk_clause(n, c, false);
|
||||
unsigned idx = m_clause_db.size();
|
||||
m_clause_db.push_back(cls);
|
||||
m_clauses.push_back(clause_info());
|
||||
for (literal lit : *cls) {
|
||||
m_values.reserve(lit.var()+1);
|
||||
m_breaks.reserve(lit.var()+1);
|
||||
m_use_list.reserve(lit.index()+1);
|
||||
m_use_list[lit.index()].push_back(idx);
|
||||
}
|
||||
m_probs.reserve(n+1);
|
||||
}
|
||||
|
||||
void prob::add(solver const& s) {
|
||||
unsigned trail_sz = s.init_trail_size();
|
||||
for (unsigned i = 0; i < trail_sz; ++i) {
|
||||
add(1, s.m_trail.c_ptr() + i);
|
||||
}
|
||||
unsigned sz = s.m_watches.size();
|
||||
for (unsigned l_idx = 0; l_idx < sz; ++l_idx) {
|
||||
literal l1 = ~to_literal(l_idx);
|
||||
watch_list const & wlist = s.m_watches[l_idx];
|
||||
for (watched const& w : wlist) {
|
||||
if (!w.is_binary_non_learned_clause())
|
||||
continue;
|
||||
literal l2 = w.get_literal();
|
||||
if (l1.index() > l2.index())
|
||||
continue;
|
||||
literal ls[2] = { l1, l2 };
|
||||
add(2, ls);
|
||||
}
|
||||
}
|
||||
for (clause* c : s.m_clauses) {
|
||||
add(c->size(), c->begin());
|
||||
}
|
||||
}
|
||||
|
||||
void prob::save_best_values() {
|
||||
m_best_min_unsat = m_unsat.size();
|
||||
m_best_values.reserve(m_values.size());
|
||||
m_model.reserve(m_values.size());
|
||||
for (unsigned i = 0; i < m_values.size(); ++i) {
|
||||
m_best_values[i] = m_values[i];
|
||||
m_model[i] = to_lbool(m_values[i]);
|
||||
}
|
||||
}
|
||||
|
||||
void prob::flatten_use_list() {
|
||||
m_use_list_index.reset();
|
||||
m_flat_use_list.reset();
|
||||
for (auto const& ul : m_use_list) {
|
||||
m_use_list_index.push_back(m_flat_use_list.size());
|
||||
m_flat_use_list.append(ul);
|
||||
}
|
||||
m_use_list_index.push_back(m_flat_use_list.size());
|
||||
}
|
||||
|
||||
void prob::init_clauses() {
|
||||
for (unsigned& b : m_breaks) {
|
||||
b = 0;
|
||||
}
|
||||
m_unsat.reset();
|
||||
for (unsigned i = 0; i < m_clauses.size(); ++i) {
|
||||
clause_info& ci = m_clauses[i];
|
||||
ci.m_num_trues = 0;
|
||||
ci.m_trues = 0;
|
||||
clause const& c = get_clause(i);
|
||||
for (literal lit : c) {
|
||||
if (is_true(lit)) {
|
||||
ci.add(lit);
|
||||
}
|
||||
}
|
||||
switch (ci.m_num_trues) {
|
||||
case 0:
|
||||
m_unsat.insert(i);
|
||||
break;
|
||||
case 1:
|
||||
inc_break(to_literal(ci.m_trues));
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void prob::auto_config() {
|
||||
unsigned max_len = 0;
|
||||
for (clause* cp : m_clause_db) {
|
||||
max_len = std::max(max_len, cp->size());
|
||||
}
|
||||
// ProbSat magic constants
|
||||
switch (max_len) {
|
||||
case 0: case 1: case 2: case 3: m_config.m_cb = 2.5; break;
|
||||
case 4: m_config.m_cb = 2.85; break;
|
||||
case 5: m_config.m_cb = 3.7; break;
|
||||
case 6: m_config.m_cb = 5.1; break;
|
||||
default: m_config.m_cb = 5.4; break;
|
||||
}
|
||||
|
||||
unsigned max_num_occ = 0;
|
||||
for (auto const& ul : m_use_list) {
|
||||
max_num_occ = std::max(max_num_occ, ul.size());
|
||||
}
|
||||
// vodoo from prob-sat
|
||||
m_prob_break.reserve(max_num_occ+1);
|
||||
for (int i = 0; i <= static_cast<int>(max_num_occ); ++i) {
|
||||
m_prob_break[i] = pow(m_config.m_cb, -i);
|
||||
}
|
||||
}
|
||||
|
||||
void prob::log() {
|
||||
double sec = m_stopwatch.get_current_seconds();
|
||||
double kflips_per_sec = m_flips / (1000.0 * sec);
|
||||
IF_VERBOSE(0, verbose_stream()
|
||||
<< sec << " sec. "
|
||||
<< (m_flips/1000) << " kflips "
|
||||
<< m_best_min_unsat << " unsat "
|
||||
<< kflips_per_sec << " kflips/sec "
|
||||
<< m_restart_count << " restarts\n");
|
||||
}
|
||||
|
||||
void prob::init() {
|
||||
flatten_use_list();
|
||||
init_random_values();
|
||||
init_clauses();
|
||||
auto_config();
|
||||
save_best_values();
|
||||
m_restart_count = 1;
|
||||
m_flips = 0;
|
||||
m_next_restart = m_config.m_restart_offset;
|
||||
m_stopwatch.start();
|
||||
}
|
||||
|
||||
void prob::init_random_values() {
|
||||
for (unsigned v = 0; v < m_values.size(); ++v) {
|
||||
m_values[v] = (m_rand() % 2 == 0);
|
||||
}
|
||||
}
|
||||
|
||||
void prob::init_best_values() {
|
||||
for (unsigned v = 0; v < m_values.size(); ++v) {
|
||||
m_values[v] = m_best_values[v];
|
||||
}
|
||||
}
|
||||
|
||||
void prob::init_near_best_values() {
|
||||
for (unsigned v = 0; v < m_values.size(); ++v) {
|
||||
if (m_rand(100) < m_config.m_prob_random_init) {
|
||||
m_values[v] = !m_best_values[v];
|
||||
}
|
||||
else {
|
||||
m_values[v] = m_best_values[v];
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void prob::do_restart() {
|
||||
reinit_values();
|
||||
init_clauses();
|
||||
m_next_restart += m_config.m_restart_offset*get_luby(m_restart_count++);
|
||||
log();
|
||||
}
|
||||
|
||||
bool prob::should_restart() {
|
||||
return m_flips >= m_next_restart;
|
||||
}
|
||||
|
||||
void prob::reinit_values() {
|
||||
init_near_best_values();
|
||||
}
|
||||
|
||||
std::ostream& prob::display(std::ostream& out) const {
|
||||
unsigned num_cls = m_clauses.size();
|
||||
for (unsigned i = 0; i < num_cls; ++i) {
|
||||
out << get_clause(i) << " ";
|
||||
auto const& ci = m_clauses[i];
|
||||
out << ci.m_num_trues << "\n";
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
||||
void prob::invariant() {
|
||||
|
||||
}
|
||||
|
||||
}
|
||||
|
160
src/sat/sat_prob.h
Normal file
160
src/sat/sat_prob.h
Normal file
|
@ -0,0 +1,160 @@
|
|||
/*++
|
||||
Copyright (c) 2019 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
sat_prob.h
|
||||
|
||||
Abstract:
|
||||
|
||||
PROB Local search module for clauses
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner 2019-4-23
|
||||
|
||||
Notes:
|
||||
|
||||
http://www.ict.griffith.edu.au/~johnt/publications/CP2006raouf.pdf
|
||||
|
||||
--*/
|
||||
#ifndef _SAT_PROB_
|
||||
#define _SAT_PROB_
|
||||
|
||||
#include "util/uint_set.h"
|
||||
#include "util/rlimit.h"
|
||||
#include "sat/sat_clause.h"
|
||||
#include "sat/sat_types.h"
|
||||
|
||||
namespace sat {
|
||||
class solver;
|
||||
|
||||
class prob : public i_local_search {
|
||||
|
||||
struct clause_info {
|
||||
clause_info(): m_trues(0), m_num_trues(0) {}
|
||||
unsigned m_trues; // set of literals that are true
|
||||
unsigned m_num_trues; // size of true set
|
||||
bool is_true() const { return m_num_trues > 0; }
|
||||
void add(literal lit) { ++m_num_trues; m_trues += lit.index(); }
|
||||
void del(literal lit) { SASSERT(m_num_trues > 0); --m_num_trues; m_trues -= lit.index(); }
|
||||
};
|
||||
|
||||
struct config {
|
||||
unsigned m_prob_random_init;
|
||||
unsigned m_restart_offset;
|
||||
double m_cb;
|
||||
double m_eps;
|
||||
config() { reset(); }
|
||||
void reset() {
|
||||
m_prob_random_init = 4;
|
||||
m_restart_offset = 1000000;
|
||||
m_cb = 2.85;
|
||||
m_eps = 0.9;
|
||||
}
|
||||
};
|
||||
|
||||
config m_config;
|
||||
reslimit m_limit;
|
||||
clause_allocator m_alloc;
|
||||
clause_vector m_clause_db;
|
||||
svector<clause_info> m_clauses;
|
||||
svector<bool> m_values, m_best_values;
|
||||
unsigned m_best_min_unsat;
|
||||
vector<unsigned_vector> m_use_list;
|
||||
unsigned_vector m_flat_use_list;
|
||||
unsigned_vector m_use_list_index;
|
||||
svector<double> m_prob_break;
|
||||
svector<double> m_probs;
|
||||
indexed_uint_set m_unsat;
|
||||
random_gen m_rand;
|
||||
unsigned_vector m_breaks;
|
||||
uint64_t m_flips;
|
||||
uint64_t m_next_restart;
|
||||
unsigned m_restart_count;
|
||||
stopwatch m_stopwatch;
|
||||
model m_model;
|
||||
|
||||
class use_list {
|
||||
prob& p;
|
||||
unsigned i;
|
||||
public:
|
||||
use_list(prob& p, literal lit):
|
||||
p(p), i(lit.index()) {}
|
||||
unsigned const* begin() { return p.m_flat_use_list.c_ptr() + p.m_use_list_index[i]; }
|
||||
unsigned const* end() { return p.m_flat_use_list.c_ptr() + p.m_use_list_index[i+1]; }
|
||||
};
|
||||
|
||||
void flatten_use_list();
|
||||
|
||||
bool is_true(literal lit) const { return m_values[lit.var()] != lit.sign(); }
|
||||
|
||||
inline clause const& get_clause(unsigned idx) const { return *m_clause_db[idx]; }
|
||||
|
||||
inline bool is_true(unsigned idx) const { return m_clauses[idx].is_true(); }
|
||||
|
||||
inline void inc_break(literal lit) { m_breaks[lit.var()]++; }
|
||||
|
||||
inline void dec_break(literal lit) { m_breaks[lit.var()]--; }
|
||||
|
||||
void flip();
|
||||
|
||||
bool_var pick_var();
|
||||
|
||||
void flip(bool_var v);
|
||||
|
||||
void reinit_values();
|
||||
|
||||
void save_best_values();
|
||||
|
||||
void init();
|
||||
|
||||
void init_random_values();
|
||||
|
||||
void init_best_values();
|
||||
|
||||
void init_near_best_values();
|
||||
|
||||
void init_clauses();
|
||||
|
||||
void auto_config();
|
||||
|
||||
bool should_restart();
|
||||
|
||||
void do_restart();
|
||||
|
||||
void invariant();
|
||||
|
||||
void log();
|
||||
|
||||
void add(unsigned sz, literal const* c);
|
||||
|
||||
public:
|
||||
prob() {}
|
||||
|
||||
~prob() override;
|
||||
|
||||
lbool check(unsigned sz, literal const* assumptions, parallel* p) override;
|
||||
|
||||
void set_seed(unsigned n) override { m_rand.set_seed(n); }
|
||||
|
||||
reslimit& rlimit() override { return m_limit; }
|
||||
|
||||
void add(solver const& s) override;
|
||||
|
||||
model const& get_model() const override { return m_model; }
|
||||
|
||||
std::ostream& display(std::ostream& out) const;
|
||||
|
||||
void updt_params(params_ref const& p) override {}
|
||||
|
||||
unsigned num_non_binary_clauses() const override { return 0; }
|
||||
|
||||
void collect_statistics(statistics& st) const override {}
|
||||
|
||||
void reinit(solver& s) override { UNREACHABLE(); }
|
||||
|
||||
};
|
||||
}
|
||||
|
||||
#endif
|
|
@ -189,7 +189,7 @@ namespace sat {
|
|||
return;
|
||||
if (!m_subsumption && !bce_enabled() && !bca_enabled() && !elim_vars_enabled())
|
||||
return;
|
||||
|
||||
|
||||
initialize();
|
||||
|
||||
CASSERT("sat_solver", s.check_invariant());
|
||||
|
@ -352,12 +352,7 @@ namespace sat {
|
|||
s.del_clause(c);
|
||||
break;
|
||||
default:
|
||||
if (s.m_config.m_drat && sz0 != sz) {
|
||||
s.m_drat.add(c, true);
|
||||
c.restore(sz0);
|
||||
s.m_drat.del(c);
|
||||
c.shrink(sz);
|
||||
}
|
||||
s.shrink(c, sz0, sz);
|
||||
*it2 = *it;
|
||||
it2++;
|
||||
if (!c.frozen()) {
|
||||
|
@ -613,7 +608,12 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
if (j < sz && !r) {
|
||||
c.shrink(j);
|
||||
if (j > 2) {
|
||||
s.shrink(c, sz, j);
|
||||
}
|
||||
else {
|
||||
c.shrink(j);
|
||||
}
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
@ -715,12 +715,6 @@ namespace sat {
|
|||
remove_clause(c, sz0 != sz);
|
||||
break;
|
||||
default:
|
||||
if (s.m_config.m_drat && sz0 != sz) {
|
||||
s.m_drat.add(c, true);
|
||||
c.restore(sz0);
|
||||
s.m_drat.del(c);
|
||||
c.shrink(sz);
|
||||
}
|
||||
TRACE("elim_lit", tout << "result: " << c << "\n";);
|
||||
m_sub_todo.insert(c);
|
||||
break;
|
||||
|
@ -911,12 +905,6 @@ namespace sat {
|
|||
remove_clause(c, sz != sz0);
|
||||
continue;
|
||||
default:
|
||||
if (s.m_config.m_drat && sz != sz0) {
|
||||
s.m_drat.add(c, true);
|
||||
c.restore(sz0);
|
||||
s.m_drat.del(c);
|
||||
c.shrink(sz);
|
||||
}
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
@ -1981,7 +1969,7 @@ namespace sat {
|
|||
model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v);
|
||||
save_clauses(mc_entry, m_pos_cls);
|
||||
save_clauses(mc_entry, m_neg_cls);
|
||||
s.m_eliminated[v] = true;
|
||||
s.set_eliminated(v, true);
|
||||
m_elim_counter -= num_pos * num_neg + before_lits;
|
||||
|
||||
for (auto & c1 : m_pos_cls) {
|
||||
|
|
File diff suppressed because it is too large
Load diff
|
@ -19,7 +19,7 @@ Revision History:
|
|||
#ifndef SAT_SOLVER_H_
|
||||
#define SAT_SOLVER_H_
|
||||
|
||||
|
||||
#include <cmath>
|
||||
#include "sat/sat_types.h"
|
||||
#include "sat/sat_clause.h"
|
||||
#include "sat/sat_watched.h"
|
||||
|
@ -71,6 +71,8 @@ namespace sat {
|
|||
unsigned m_elim_var_res;
|
||||
unsigned m_elim_var_bdd;
|
||||
unsigned m_units;
|
||||
unsigned m_backtracks;
|
||||
unsigned m_backjumps;
|
||||
stats() { reset(); }
|
||||
void reset();
|
||||
void collect_statistics(statistics & st) const;
|
||||
|
@ -80,6 +82,8 @@ namespace sat {
|
|||
public:
|
||||
struct abort_solver {};
|
||||
protected:
|
||||
enum search_state { s_sat, s_unsat };
|
||||
|
||||
bool m_checkpoint_enabled;
|
||||
config m_config;
|
||||
stats m_stats;
|
||||
|
@ -116,7 +120,9 @@ namespace sat {
|
|||
svector<char> m_lit_mark;
|
||||
svector<char> m_eliminated;
|
||||
svector<char> m_external;
|
||||
svector<unsigned> m_level;
|
||||
unsigned_vector m_touched;
|
||||
unsigned m_touch_index;
|
||||
literal_vector m_replay_assign;
|
||||
// branch variable selection:
|
||||
svector<unsigned> m_activity;
|
||||
unsigned m_activity_inc;
|
||||
|
@ -128,17 +134,27 @@ namespace sat {
|
|||
int m_action;
|
||||
double m_step_size;
|
||||
// phase
|
||||
svector<char> m_phase;
|
||||
svector<char> m_prev_phase;
|
||||
svector<bool> m_phase;
|
||||
svector<bool> m_best_phase;
|
||||
svector<bool> m_prev_phase;
|
||||
svector<char> m_assigned_since_gc;
|
||||
bool m_phase_cache_on;
|
||||
search_state m_search_state;
|
||||
unsigned m_search_unsat_conflicts;
|
||||
unsigned m_search_sat_conflicts;
|
||||
unsigned m_search_next_toggle;
|
||||
unsigned m_phase_counter;
|
||||
unsigned m_best_phase_size;
|
||||
unsigned m_rephase_lim;
|
||||
unsigned m_rephase_inc;
|
||||
var_queue m_case_split_queue;
|
||||
unsigned m_qhead;
|
||||
unsigned m_scope_lvl;
|
||||
unsigned m_search_lvl;
|
||||
ema m_fast_glue_avg;
|
||||
ema m_slow_glue_avg;
|
||||
ema m_fast_glue_backup;
|
||||
ema m_slow_glue_backup;
|
||||
ema m_trail_avg;
|
||||
literal_vector m_trail;
|
||||
clause_wrapper_vector m_clauses_to_reinit;
|
||||
std::string m_reason_unknown;
|
||||
|
@ -163,7 +179,7 @@ namespace sat {
|
|||
bool m_par_syncing_clauses;
|
||||
|
||||
class lookahead* m_cuber;
|
||||
class local_search* m_local_search;
|
||||
class i_local_search* m_local_search;
|
||||
|
||||
statistics m_aux_stats;
|
||||
|
||||
|
@ -174,6 +190,7 @@ namespace sat {
|
|||
friend class simplifier;
|
||||
friend class scc;
|
||||
friend class big;
|
||||
friend class binspr;
|
||||
friend class elim_eqs;
|
||||
friend class asymm_branch;
|
||||
friend class probing;
|
||||
|
@ -184,6 +201,8 @@ namespace sat {
|
|||
friend class parallel;
|
||||
friend class lookahead;
|
||||
friend class local_search;
|
||||
friend class ddfw;
|
||||
friend class prob;
|
||||
friend class unit_walk;
|
||||
friend struct mk_stat;
|
||||
friend class elim_vars;
|
||||
|
@ -251,6 +270,7 @@ namespace sat {
|
|||
void attach_clause(clause & c, bool & reinit);
|
||||
void attach_clause(clause & c) { bool reinit; attach_clause(c, reinit); }
|
||||
void set_learned(clause& c, bool learned);
|
||||
void shrink(clause& c, unsigned old_sz, unsigned new_sz);
|
||||
void set_learned(literal l1, literal l2, bool learned);
|
||||
void set_learned1(literal l1, literal l2, bool learned);
|
||||
void add_ate(clause& c) { m_mc.add_ate(c); }
|
||||
|
@ -285,7 +305,7 @@ namespace sat {
|
|||
// -----------------------
|
||||
public:
|
||||
bool inconsistent() const override { return m_inconsistent; }
|
||||
unsigned num_vars() const override { return m_level.size(); }
|
||||
unsigned num_vars() const override { return m_justification.size(); }
|
||||
unsigned num_clauses() const override;
|
||||
void num_binary(unsigned& given, unsigned& learned) const;
|
||||
unsigned num_restarts() const { return m_restarts; }
|
||||
|
@ -293,7 +313,7 @@ namespace sat {
|
|||
void set_external(bool_var v) override;
|
||||
void set_non_external(bool_var v) override;
|
||||
bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; }
|
||||
void set_eliminated(bool_var v, bool f) override { m_eliminated[v] = f; }
|
||||
void set_eliminated(bool_var v, bool f) override;
|
||||
bool was_eliminated(literal l) const { return was_eliminated(l.var()); }
|
||||
unsigned scope_lvl() const { return m_scope_lvl; }
|
||||
unsigned search_lvl() const { return m_search_lvl; }
|
||||
|
@ -301,40 +321,55 @@ namespace sat {
|
|||
bool at_base_lvl() const override { return m_scope_lvl == 0; }
|
||||
lbool value(literal l) const { return static_cast<lbool>(m_assignment[l.index()]); }
|
||||
lbool value(bool_var v) const { return static_cast<lbool>(m_assignment[literal(v, false).index()]); }
|
||||
unsigned lvl(bool_var v) const { return m_level[v]; }
|
||||
unsigned lvl(literal l) const { return m_level[l.var()]; }
|
||||
unsigned lvl(bool_var v) const { return m_justification[v].level(); }
|
||||
unsigned lvl(literal l) const { return m_justification[l.var()].level(); }
|
||||
unsigned init_trail_size() const override { return at_base_lvl() ? m_trail.size() : m_scopes[0].m_trail_lim; }
|
||||
unsigned trail_size() const { return m_trail.size(); }
|
||||
literal trail_literal(unsigned i) const override { return m_trail[i]; }
|
||||
literal scope_literal(unsigned n) const { return m_trail[m_scopes[n].m_trail_lim]; }
|
||||
void assign(literal l, justification j) {
|
||||
TRACE("sat_assign", tout << l << " previous value: " << value(l) << "\n";);
|
||||
TRACE("sat_assign", tout << l << " previous value: " << value(l) << " j: " << j << "\n";);
|
||||
switch (value(l)) {
|
||||
case l_false: set_conflict(j, ~l); break;
|
||||
case l_undef: assign_core(l, scope_lvl(), j); break;
|
||||
case l_undef: assign_core(l, j); break;
|
||||
case l_true: return;
|
||||
}
|
||||
}
|
||||
void assign_core(literal l, unsigned lvl, justification jst);
|
||||
void assign_unit(literal l) { assign(l, justification()); }
|
||||
void assign_scoped(literal l) { assign(l, justification()); }
|
||||
void assign_unit(literal l) { assign(l, justification(0)); }
|
||||
void assign_scoped(literal l) { assign(l, justification(scope_lvl())); }
|
||||
void assign_core(literal l, justification jst);
|
||||
void set_conflict(justification c, literal not_l);
|
||||
void set_conflict(justification c) { set_conflict(c, null_literal); }
|
||||
void set_conflict() { set_conflict(justification()); }
|
||||
void set_conflict() { set_conflict(justification(0)); }
|
||||
lbool status(clause const & c) const;
|
||||
clause_offset get_offset(clause const & c) const { return cls_allocator().get_offset(&c); }
|
||||
void checkpoint() {
|
||||
if (!m_checkpoint_enabled) return;
|
||||
|
||||
bool limit_reached() {
|
||||
if (!m_rlimit.inc()) {
|
||||
m_mc.reset();
|
||||
m_model_is_current = false;
|
||||
TRACE("sat", tout << "canceled\n";);
|
||||
m_reason_unknown = "sat.canceled";
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
bool memory_exceeded() {
|
||||
++m_num_checkpoints;
|
||||
if (m_num_checkpoints < 10) return false;
|
||||
m_num_checkpoints = 0;
|
||||
return memory::get_allocation_size() > m_config.m_max_memory;
|
||||
}
|
||||
|
||||
void checkpoint() {
|
||||
if (!m_checkpoint_enabled) return;
|
||||
if (limit_reached()) {
|
||||
throw solver_exception(Z3_CANCELED_MSG);
|
||||
}
|
||||
++m_num_checkpoints;
|
||||
if (m_num_checkpoints < 10) return;
|
||||
m_num_checkpoints = 0;
|
||||
if (memory::get_allocation_size() > m_config.m_max_memory) throw solver_exception(Z3_MAX_MEMORY_MSG);
|
||||
if (memory_exceeded()) {
|
||||
throw solver_exception(Z3_MAX_MEMORY_MSG);
|
||||
}
|
||||
}
|
||||
void set_par(parallel* p, unsigned id);
|
||||
bool canceled() { return !m_rlimit.inc(); }
|
||||
|
@ -358,7 +393,6 @@ namespace sat {
|
|||
void unmark_lit(literal l) { SASSERT(is_marked_lit(l)); m_lit_mark[l.index()] = false; }
|
||||
bool check_inconsistent();
|
||||
|
||||
|
||||
// -----------------------
|
||||
//
|
||||
// Propagation
|
||||
|
@ -369,6 +403,7 @@ namespace sat {
|
|||
bool propagate(bool update);
|
||||
|
||||
protected:
|
||||
bool should_propagate() const;
|
||||
bool propagate_core(bool update);
|
||||
|
||||
// -----------------------
|
||||
|
@ -391,6 +426,8 @@ namespace sat {
|
|||
void set_activity(bool_var v, unsigned act);
|
||||
|
||||
lbool cube(bool_var_vector& vars, literal_vector& lits, unsigned backtrack_level);
|
||||
|
||||
void display_lookahead_scores(std::ostream& out);
|
||||
|
||||
protected:
|
||||
|
||||
|
@ -398,6 +435,7 @@ namespace sat {
|
|||
unsigned m_restarts;
|
||||
unsigned m_restart_next_out;
|
||||
unsigned m_conflicts_since_restart;
|
||||
bool m_force_conflict_analysis;
|
||||
unsigned m_simplifications;
|
||||
unsigned m_restart_threshold;
|
||||
unsigned m_luby_idx;
|
||||
|
@ -427,22 +465,28 @@ namespace sat {
|
|||
void reinit_assumptions();
|
||||
bool tracking_assumptions() const;
|
||||
bool is_assumption(literal l) const;
|
||||
void simplify_problem();
|
||||
bool should_simplify() const;
|
||||
void do_simplify();
|
||||
void mk_model();
|
||||
bool check_model(model const & m) const;
|
||||
void restart(bool to_base);
|
||||
void do_restart(bool to_base);
|
||||
svector<size_t> m_last_positions;
|
||||
unsigned m_last_position_log;
|
||||
unsigned m_restart_logs;
|
||||
unsigned restart_level(bool to_base);
|
||||
void log_stats();
|
||||
bool should_cancel();
|
||||
bool should_restart() const;
|
||||
void set_next_restart();
|
||||
void update_activity(bool_var v, double p);
|
||||
bool reached_max_conflicts();
|
||||
void sort_watch_lits();
|
||||
void exchange_par();
|
||||
lbool check_par(unsigned num_lits, literal const* lits);
|
||||
lbool do_local_search(unsigned num_lits, literal const* lits);
|
||||
lbool do_ddfw_search(unsigned num_lits, literal const* lits);
|
||||
lbool do_prob_search(unsigned num_lits, literal const* lits);
|
||||
lbool invoke_local_search(unsigned num_lits, literal const* lits);
|
||||
lbool do_unit_walk();
|
||||
|
||||
// -----------------------
|
||||
|
@ -451,7 +495,8 @@ namespace sat {
|
|||
//
|
||||
// -----------------------
|
||||
protected:
|
||||
void gc();
|
||||
bool should_gc() const;
|
||||
void do_gc();
|
||||
void gc_glue();
|
||||
void gc_psm();
|
||||
void gc_glue_psm();
|
||||
|
@ -492,18 +537,31 @@ namespace sat {
|
|||
unsigned m_conflict_lvl;
|
||||
literal_vector m_lemma;
|
||||
literal_vector m_ext_antecedents;
|
||||
bool use_backjumping(unsigned num_scopes);
|
||||
bool resolve_conflict();
|
||||
bool resolve_conflict_core();
|
||||
lbool resolve_conflict_core();
|
||||
void learn_lemma_and_backjump();
|
||||
unsigned get_max_lvl(literal consequent, justification js);
|
||||
inline unsigned update_max_level(literal lit, unsigned lvl2, bool& unique_max) {
|
||||
unsigned lvl1 = lvl(lit);
|
||||
if (lvl1 < lvl2) return lvl2;
|
||||
unique_max = lvl1 > lvl2;
|
||||
return lvl1;
|
||||
}
|
||||
unsigned get_max_lvl(literal consequent, justification js, bool& unique_max);
|
||||
void process_antecedent(literal antecedent, unsigned & num_marks);
|
||||
void resolve_conflict_for_unsat_core();
|
||||
void process_antecedent_for_unsat_core(literal antecedent);
|
||||
void process_consequent_for_unsat_core(literal consequent, justification const& js);
|
||||
void fill_ext_antecedents(literal consequent, justification js);
|
||||
unsigned skip_literals_above_conflict_level();
|
||||
void forget_phase_of_vars(unsigned from_lvl);
|
||||
void updt_phase_of_vars();
|
||||
void updt_phase_counters();
|
||||
void do_toggle_search_state();
|
||||
bool should_toggle_search_state();
|
||||
bool is_sat_phase() const;
|
||||
bool is_two_phase() const;
|
||||
bool should_rephase();
|
||||
void do_rephase();
|
||||
svector<char> m_diff_levels;
|
||||
unsigned num_diff_levels(unsigned num, literal const * lits);
|
||||
bool num_diff_levels_below(unsigned num, literal const* lits, unsigned max_glue, unsigned& glue);
|
||||
|
@ -518,8 +576,9 @@ namespace sat {
|
|||
bool implied_by_marked(literal lit);
|
||||
void reset_unmark(unsigned old_size);
|
||||
void updt_lemma_lvl_set();
|
||||
void reset_lemma_var_marks();
|
||||
bool minimize_lemma();
|
||||
bool minimize_lemma_binres();
|
||||
void reset_lemma_var_marks();
|
||||
bool dyn_sub_res();
|
||||
|
||||
// -----------------------
|
||||
|
@ -531,7 +590,7 @@ namespace sat {
|
|||
void pop(unsigned num_scopes);
|
||||
void pop_reinit(unsigned num_scopes);
|
||||
|
||||
void unassign_vars(unsigned old_sz);
|
||||
void unassign_vars(unsigned old_sz, unsigned new_lvl);
|
||||
void reinit_clauses(unsigned old_sz);
|
||||
|
||||
literal_vector m_user_scope_literals;
|
||||
|
@ -556,7 +615,7 @@ namespace sat {
|
|||
//
|
||||
// -----------------------
|
||||
public:
|
||||
void cleanup(bool force);
|
||||
bool do_cleanup(bool force);
|
||||
void simplify(bool learned = true);
|
||||
void asymmetric_branching();
|
||||
unsigned scc_bin();
|
||||
|
|
|
@ -29,6 +29,10 @@ Revision History:
|
|||
#include "util/stopwatch.h"
|
||||
#include<iomanip>
|
||||
|
||||
class params_ref;
|
||||
class reslimit;
|
||||
class statistics;
|
||||
|
||||
namespace sat {
|
||||
#define SAT_VB_LVL 10
|
||||
|
||||
|
@ -120,11 +124,8 @@ namespace sat {
|
|||
|
||||
typedef approx_set_tpl<bool_var, u2u, unsigned> var_approx_set;
|
||||
|
||||
enum phase {
|
||||
POS_PHASE, NEG_PHASE, PHASE_NOT_AVAILABLE
|
||||
};
|
||||
|
||||
class solver;
|
||||
class parallel;
|
||||
class lookahead;
|
||||
class unit_walk;
|
||||
class clause;
|
||||
|
@ -257,6 +258,22 @@ namespace sat {
|
|||
inline std::ostream & operator<<(std::ostream & out, literal_vector const & ls) {
|
||||
return out << mk_lits_pp(ls.size(), ls.c_ptr());
|
||||
}
|
||||
|
||||
class i_local_search {
|
||||
public:
|
||||
virtual ~i_local_search() {}
|
||||
virtual void add(solver const& s) = 0;
|
||||
virtual void updt_params(params_ref const& p) = 0;
|
||||
virtual void set_seed(unsigned s) = 0;
|
||||
virtual lbool check(unsigned sz, literal const* assumptions, parallel* par) = 0;
|
||||
virtual void reinit(solver& s) = 0;
|
||||
virtual unsigned num_non_binary_clauses() const = 0;
|
||||
virtual reslimit& rlimit() = 0;
|
||||
virtual model const& get_model() const = 0;
|
||||
virtual void collect_statistics(statistics& st) const = 0;
|
||||
virtual double get_priority(bool_var v) const { return 0; }
|
||||
|
||||
};
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
|
@ -45,8 +45,10 @@ namespace sat {
|
|||
while (m_head < m_vars.size()) {
|
||||
bool_var v = m_vars[m_head];
|
||||
unsigned idx = literal(v, false).index();
|
||||
if (s.m_assignment[idx] == l_undef)
|
||||
if (s.m_assignment[idx] == l_undef) {
|
||||
// IF_VERBOSE(0, verbose_stream() << "pop " << v << "\n");
|
||||
return v;
|
||||
}
|
||||
++m_head;
|
||||
}
|
||||
for (bool_var v : m_vars) {
|
||||
|
@ -54,17 +56,21 @@ namespace sat {
|
|||
IF_VERBOSE(0, verbose_stream() << "unassigned: " << v << "\n");
|
||||
}
|
||||
}
|
||||
IF_VERBOSE(0, verbose_stream() << "#vars: " << m_vars.size() << "\n");
|
||||
IF_VERBOSE(0, verbose_stream() << "(sat.unit-walk sat)\n");
|
||||
return null_bool_var;
|
||||
}
|
||||
|
||||
void unit_walk::var_priority::set_vars(solver& s) {
|
||||
m_vars.reset();
|
||||
s.pop_to_base_level();
|
||||
|
||||
for (unsigned v = 0; v < s.num_vars(); ++v) {
|
||||
if (!s.was_eliminated(v) && s.m_assignment[v] == l_undef) {
|
||||
if (!s.was_eliminated(v) && s.value(v) == l_undef) {
|
||||
add(v);
|
||||
}
|
||||
}
|
||||
IF_VERBOSE(0, verbose_stream() << "num vars " << m_vars.size() << "\n";);
|
||||
}
|
||||
|
||||
bool_var unit_walk::var_priority::next(solver& s) {
|
||||
|
@ -215,7 +221,7 @@ namespace sat {
|
|||
switch (is_sat) {
|
||||
case l_true:
|
||||
for (unsigned v = 0; v < s.num_vars(); ++v) {
|
||||
s.m_assignment[v] = m_ls.get_phase(v) ? l_true : l_false;
|
||||
s.m_assignment[v] = m_ls.get_best_phase(v) ? l_true : l_false;
|
||||
}
|
||||
return l_true;
|
||||
case l_false:
|
||||
|
@ -239,8 +245,7 @@ namespace sat {
|
|||
local_search& ls;
|
||||
compare_break(local_search& ls): ls(ls) {}
|
||||
int operator()(bool_var v, bool_var w) const {
|
||||
double diff = ls.break_count(v) - ls.break_count(w);
|
||||
return diff > 0;
|
||||
return ls.get_priority(v) > ls.get_priority(w);
|
||||
}
|
||||
};
|
||||
|
||||
|
@ -249,22 +254,14 @@ namespace sat {
|
|||
std::sort(pqueue().begin(), pqueue().end(), cb);
|
||||
for (bool_var v : pqueue()) {
|
||||
m_phase_tf[v].update(m_ls.cur_solution(v) ? 100 : 0);
|
||||
m_phase[v] = m_ls.cur_solution(v);
|
||||
m_phase[v] = l_true == m_ls.cur_solution(v);
|
||||
}
|
||||
pqueue().rewind();
|
||||
}
|
||||
|
||||
void unit_walk::init_phase() {
|
||||
for (bool_var v : pqueue()) {
|
||||
if (s.m_phase[v] == POS_PHASE) {
|
||||
m_phase[v] = true;
|
||||
}
|
||||
else if (s.m_phase[v] == NEG_PHASE) {
|
||||
m_phase[v] = false;
|
||||
}
|
||||
else {
|
||||
m_phase[v] = m_rand(100) < m_phase_tf[v];
|
||||
}
|
||||
m_phase[v] = s.m_phase[v];
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -421,7 +421,7 @@ namespace smt {
|
|||
return m_activity[v];
|
||||
}
|
||||
|
||||
void set_activity(bool_var v, double const & act) {
|
||||
void set_activity(bool_var v, double act) {
|
||||
m_activity[v] = act;
|
||||
}
|
||||
|
||||
|
|
|
@ -165,11 +165,18 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, p
|
|||
}
|
||||
catch (tactic_exception & ex) {
|
||||
reason_unknown = ex.msg();
|
||||
if (r.size() > 0) pr = r[0]->pr(0);
|
||||
return l_undef;
|
||||
}
|
||||
TRACE("tactic_check_sat",
|
||||
TRACE("tactic",
|
||||
tout << "r.size(): " << r.size() << "\n";
|
||||
for (unsigned i = 0; i < r.size(); i++) r[i]->display(tout););
|
||||
for (unsigned i = 0; i < r.size(); i++) r[i]->display_with_dependencies(tout););
|
||||
|
||||
if (r.size() > 0) {
|
||||
pr = r[0]->pr(0);
|
||||
TRACE("tactic", tout << pr << "\n";);
|
||||
}
|
||||
|
||||
|
||||
if (is_decided_sat(r)) {
|
||||
model_converter_ref mc = r[0]->mc();
|
||||
|
@ -192,7 +199,7 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, p
|
|||
}
|
||||
else {
|
||||
if (models_enabled && !r.empty()) {
|
||||
model_converter_ref mc = r[0]->mc();
|
||||
model_converter_ref mc = r[0]->mc();
|
||||
model_converter2model(m, mc.get(), md);
|
||||
if (mc)
|
||||
(*mc)(labels);
|
||||
|
|
|
@ -46,7 +46,6 @@ static bool build_instance(char const * filename, sat::solver& s, sat::local_sea
|
|||
std::cout << "Objective function format error. They have different lengths.\n";
|
||||
return false;
|
||||
}
|
||||
|
||||
|
||||
// read the constraints, one at a time
|
||||
int k;
|
||||
|
@ -124,6 +123,6 @@ void tst_sat_local_search(char ** argv, int argc, int& i) {
|
|||
cancel_eh<reslimit> eh(local_search.rlimit());
|
||||
scoped_ctrl_c ctrlc(eh, false, true);
|
||||
scoped_timer timer(cutoff_time*1000, &eh);
|
||||
local_search.check();
|
||||
local_search.check(0, nullptr, nullptr);
|
||||
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue