diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp
index 869b4ac4c..8e5e556e3 100644
--- a/src/sat/sat_asymm_branch.cpp
+++ b/src/sat/sat_asymm_branch.cpp
@@ -59,7 +59,7 @@ namespace sat {
}
};
- void asymm_branch::process(scc& scc, clause_vector& clauses) {
+ void asymm_branch::process(scc* scc, clause_vector& clauses) {
int64 limit = -m_asymm_branch_limit;
std::stable_sort(clauses.begin(), clauses.end(), clause_size_lt());
m_counter -= clauses.size();
@@ -83,7 +83,7 @@ namespace sat {
}
s.checkpoint();
clause & c = *(*it);
- if (m_asymm_branch_sampled ? !process_sampled(scc, c) : !process(c)) {
+ if (scc ? !process_sampled(*scc, c) : !process(c)) {
continue; // clause was removed
}
*it2 = *it;
@@ -106,7 +106,7 @@ namespace sat {
++m_calls;
if (m_calls <= m_asymm_branch_delay)
return;
- if (!m_asymm_branch && !m_asymm_branch_all)
+ if (!m_asymm_branch && !m_asymm_branch_all && !m_asymm_branch_sampled)
return;
s.propagate(false); // must propagate, since it uses s.push()
if (s.m_inconsistent)
@@ -119,13 +119,18 @@ namespace sat {
TRACE("asymm_branch_detail", s.display(tout););
report rpt(*this);
svector<char> saved_phase(s.m_phase);
+ if (m_asymm_branch) {
+ m_counter = 0;
+ process(nullptr, s.m_clauses);
+ m_counter = -m_counter;
+ }
if (m_asymm_branch_sampled) {
scc scc(s, m_params);
while (true) {
unsigned elim = m_elim_literals;
scc.init_big(true);
- process(scc, s.m_clauses);
- process(scc, s.m_learned);
+ process(&scc, s.m_clauses);
+ process(&scc, s.m_learned);
s.propagate(false);
if (s.m_inconsistent)
break;
@@ -134,12 +139,6 @@ namespace sat {
break;
}
}
- else {
- scc scc(s, m_params);
- m_counter = 0;
- process(scc, s.m_clauses);
- m_counter = -m_counter;
- }
s.m_phase = saved_phase;
m_asymm_branch_limit *= 2;
if (m_asymm_branch_limit > UINT_MAX)
diff --git a/src/sat/sat_asymm_branch.h b/src/sat/sat_asymm_branch.h
index b7e2b0218..4510aaddf 100644
--- a/src/sat/sat_asymm_branch.h
+++ b/src/sat/sat_asymm_branch.h
@@ -41,6 +41,7 @@ namespace sat {
bool m_asymm_branch;
unsigned m_asymm_branch_delay;
bool m_asymm_branch_sampled;
+ bool m_asymm_branch_propagate;
bool m_asymm_branch_all;
int64 m_asymm_branch_limit;
@@ -64,7 +65,7 @@ namespace sat {
bool process_sampled(scc& scc, clause & c);
- void process(scc& scc, clause_vector & c);
+ void process(scc* scc, clause_vector & c);
bool process_all(clause & c);
diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index b0797dae9..87d84f133 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -38,8 +38,6 @@ namespace sat {
m_glue_psm("glue_psm"),
m_psm_glue("psm_glue") {
m_num_threads = 1;
- m_local_search = 0;
- m_lookahead_search = false;
m_lookahead_simplify = false;
m_lookahead_simplify_bca = false;
m_elim_vars = false;
@@ -92,7 +90,6 @@ namespace sat {
m_local_search_threads = p.local_search_threads();
m_lookahead_simplify = p.lookahead_simplify();
m_lookahead_simplify_bca = p.lookahead_simplify_bca();
- m_lookahead_search = p.lookahead_search();
if (p.lookahead_reward() == symbol("heule_schur")) {
m_lookahead_reward = heule_schur_reward;
}
@@ -214,7 +211,6 @@ namespace sat {
else {
throw sat_param_exception("invalid PB solver: solver, totalizer, circuit, sorting");
}
- m_dimacs_inprocess_display = p.dimacs_inprocess_display();
sat_simplifier_params sp(_p);
m_elim_vars = sp.elim_vars();
diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h
index 1529466ee..ed7802cef 100644
--- a/src/sat/sat_config.h
+++ b/src/sat/sat_config.h
@@ -89,7 +89,6 @@ namespace sat {
unsigned m_num_threads;
unsigned m_local_search_threads;
bool m_local_search;
- bool m_lookahead_search;
bool m_lookahead_simplify;
bool m_lookahead_simplify_bca;
cutoff_t m_lookahead_cube_cutoff;
@@ -124,8 +123,6 @@ namespace sat {
bool m_drat_check_unsat;
bool m_drat_check_sat;
- bool m_dimacs_inprocess_display;
-
symbol m_always_true;
symbol m_always_false;
symbol m_caching;
diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp
index ea44c870d..d0166b64e 100644
--- a/src/sat/sat_elim_eqs.cpp
+++ b/src/sat/sat_elim_eqs.cpp
@@ -94,10 +94,11 @@ namespace sat {
if (!c.frozen())
m_solver.detach_clause(c);
// apply substitution
- for (i = 0; i < sz; i++) {
- c[i] = norm(roots, c[i]);
+ for (i = 0; i < sz; i++) {
+ literal lit = c[i];
+ c[i] = norm(roots, lit);
VERIFY(c[i] == norm(roots, c[i]));
- VERIFY(!m_solver.was_eliminated(c[i].var()));
+ VERIFY(!m_solver.was_eliminated(c[i].var()) || lit == c[i]);
}
std::sort(c.begin(), c.end());
for (literal l : c) VERIFY(l == norm(roots, l));
diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp
index 3feb9455d..a9ae3b641 100644
--- a/src/sat/sat_lookahead.cpp
+++ b/src/sat/sat_lookahead.cpp
@@ -2408,6 +2408,8 @@ namespace sat {
++disconnected1;
uf.merge(u.index(), v.index());
uf.merge((~u).index(), (~v).index());
+ VERIFY(!m_s.was_eliminated(u.var()));
+ VERIFY(!m_s.was_eliminated(v.var()));
m_s.mk_clause(~u, v, true);
}
else {
diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg
index 565c6dbcc..0e6823030 100644
--- a/src/sat/sat_params.pyg
+++ b/src/sat/sat_params.pyg
@@ -35,8 +35,8 @@ def_module_params('sat',
('pb.solver', SYMBOL, 'circuit', 'method for handling Pseudo-Boolean constraints: circuit (arithmetical circuit), sorting (sorting circuit), totalizer (use totalizer encoding), solver (use SMT solver)'),
('xor.solver', BOOL, False, 'use xor solver'),
('atmost1_encoding', SYMBOL, 'grouped', 'encoding used for at-most-1 constraints grouped, bimander, ordered'),
- ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'),
('local_search', BOOL, False, 'use local search instead of CDCL'),
+ ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'),
('lookahead.cube.cutoff', SYMBOL, 'adaptive', 'cutoff type used to create lookahead cubes: adaptive, fixed_depth, fixed_freevars, psat'),
('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. Used when lookahead.cube.cutoff is adaptive'),
('lookahead.cube.depth', UINT, 10, 'cut-off depth to create cubes. Used when lookahead.cube.cutoff is fixed_depth.'),
@@ -49,6 +49,5 @@ def_module_params('sat',
('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'),
('lookahead_simplify.bca', BOOL, False, 'add learned binary clauses as part of lookahead simplification'),
('lookahead.global_autarky', BOOL, False, 'prefer to branch on variables that occur in clauses that are reduced'),
- ('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu'),
- ('dimacs.inprocess.display', BOOL, False, 'display SAT instance in DIMACS format if unsolved after inprocess.max inprocessing passes')))
+ ('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu')))
diff --git a/src/sat/sat_scc.cpp b/src/sat/sat_scc.cpp
index 7615a19a3..59c53304d 100644
--- a/src/sat/sat_scc.cpp
+++ b/src/sat/sat_scc.cpp
@@ -303,16 +303,16 @@ namespace sat {
else {
SASSERT(m_left[u.index()] == 0);
m_left[u.index()] = ++dfs_num;
- for (literal v : m_dag[u.index()]) {
- if (m_left[v.index()] == 0) {
- todo.push_back(pframe(u, v));
- }
- }
literal p = todo.back().parent();
if (p != null_literal) {
m_root[u.index()] = m_root[p.index()];
m_parent[u.index()] = p;
}
+ for (literal v : m_dag[u.index()]) {
+ if (m_left[v.index()] == 0) {
+ todo.push_back(pframe(u, v));
+ }
+ }
}
}
for (unsigned i = 0; i < num_lits; ++i) {
@@ -339,7 +339,7 @@ namespace sat {
watch_list::iterator end = wlist.end();
for (; it != end; ++it) {
watched& w = *it;
- if (learned ? w.is_binary_learned_clause() : w.is_binary_unblocked_clause()) {
+ if (learned ? w.is_binary_learned_clause() : w.is_binary_clause()) {
literal v = w.get_literal();
if (reaches(u, v) && u != get_parent(v)) {
++m_num_elim_bin;
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 5a7e234e9..b3fc95f47 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -159,17 +159,20 @@ namespace sat {
}
}
// copy high quality lemmas
+ unsigned num_learned = 0;
for (clause* c : src.m_learned) {
if (c->glue() <= 2 || (c->size() <= 40 && c->glue() <= 8)) {
buffer.reset();
for (literal l : *c) buffer.push_back(l);
clause* c1 = mk_clause_core(buffer.size(), buffer.c_ptr(), true);
if (c1) {
+ ++num_learned;
c1->set_glue(c->glue());
c1->set_psm(c->psm());
}
}
}
+ IF_VERBOSE(1, verbose_stream() << "(sat.copy :learned " << num_learned << ")\n";);
}
m_user_scope_literals.reset();
@@ -879,9 +882,6 @@ namespace sat {
m_stats.m_units = init_trail_size();
IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver)\n";);
SASSERT(at_base_lvl());
- if (m_config.m_lookahead_search && num_lits == 0) {
- return lookahead_search();
- }
if (m_config.m_local_search) {
return do_local_search(num_lits, lits);
@@ -950,12 +950,6 @@ namespace sat {
if (m_config.m_inprocess_max <= m_simplifications) {
m_reason_unknown = "sat.max.inprocess";
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-inprocess\")\n";);
- if (m_config.m_dimacs_inprocess_display) {
- display_dimacs(std::cout);
- for (unsigned i = 0; i < num_lits; ++lits) {
- std::cout << dimacs_lit(lits[i]) << " 0\n";
- }
- }
return l_undef;
}
@@ -984,21 +978,6 @@ namespace sat {
return r;
}
- lbool solver::lookahead_search() {
- lookahead lh(*this);
- lbool r = l_undef;
- try {
- r = lh.check();
- m_model = lh.get_model();
- }
- catch (z3_exception&) {
- lh.collect_statistics(m_aux_stats);
- throw;
- }
- lh.collect_statistics(m_aux_stats);
- return r;
- }
-
lbool solver::check_par(unsigned num_lits, literal const* lits) {
scoped_ptr_vector<local_search> ls;
int num_threads = static_cast<int>(m_config.m_num_threads + m_config.m_local_search_threads);
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 602850487..135d9e067 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -394,7 +394,6 @@ namespace sat {
void sort_watch_lits();
void exchange_par();
lbool check_par(unsigned num_lits, literal const* lits);
- lbool lookahead_search();
lbool do_local_search(unsigned num_lits, literal const* lits);
// -----------------------