From ff2cdc0e3f75bcecd549a27db1cd451c1aa9fee3 Mon Sep 17 00:00:00 2001 From: Miguel Angelo Da Terra Neves Date: Wed, 27 Sep 2017 17:18:28 -0700 Subject: [PATCH] local updates Signed-off-by: Miguel Angelo Da Terra Neves --- src/sat/sat_config.cpp | 2 ++ src/sat/sat_config.h | 2 ++ src/sat/sat_params.pyg | 4 +++- src/sat/sat_simplifier.cpp | 2 +- src/sat/sat_solver.cpp | 20 ++++++++++++++++---- src/sat/sat_solver.h | 1 + 6 files changed, 25 insertions(+), 6 deletions(-) diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 0248b5b0b..49a146489 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -72,6 +72,7 @@ namespace sat { m_restart_initial = p.restart_initial(); m_restart_factor = p.restart_factor(); m_restart_max = p.restart_max(); + m_inprocess_max = p.inprocess_max(); m_random_freq = p.random_freq(); m_random_seed = p.random_seed(); @@ -183,6 +184,7 @@ namespace sat { throw sat_param_exception("invalid PB solver: solver, totalizer, circuit, sorting"); } m_dimacs_display = p.dimacs_display(); + m_dimacs_inprocess_display = p.dimacs_inprocess_display(); } void config::collect_param_descrs(param_descrs & r) { diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index ba68b7901..a7c8590fb 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -73,6 +73,7 @@ namespace sat { unsigned m_restart_initial; double m_restart_factor; // for geometric case unsigned m_restart_max; + unsigned m_inprocess_max; double m_random_freq; unsigned m_random_seed; unsigned m_burst_search; @@ -106,6 +107,7 @@ namespace sat { bool m_drat_check; bool m_dimacs_display; + bool m_dimacs_inprocess_display; symbol m_always_true; symbol m_always_false; diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index ab35b3c56..67659aa24 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -9,6 +9,7 @@ def_module_params('sat', ('restart.initial', UINT, 100, 'initial restart (number of conflicts)'), ('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'), ('restart.factor', DOUBLE, 1.5, 'restart increment factor for geometric strategy'), + ('inprocess.max', UINT, UINT_MAX, 'maximal number of inprocessing passes'), ('branching.heuristic', SYMBOL, 'vsids', 'branching heuristic vsids, lrb or chb'), ('branching.anti_exploration', BOOL, False, 'apply anti-exploration heuristic for branch selection'), ('random_freq', DOUBLE, 0.01, 'frequency of random case splits'), @@ -40,5 +41,6 @@ def_module_params('sat', ('lookahead_search', BOOL, False, 'use lookahead solver'), ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'), ('lookahead.reward', SYMBOL, 'heuleu', 'select lookahead heuristic: ternary, hs (Heule Schur), heuleu (Heule Unit), or unit'), - ('dimacs.display', BOOL, False, 'display SAT instance in DIMACS format and return unknown instead of solving'))) + ('dimacs.display', BOOL, False, 'display SAT instance in DIMACS format and return unknown instead of solving'), + ('dimacs.inprocess.display', BOOL, False, 'display SAT instance in DIMACS format if unsolved after inprocess.max inprocessing passes'))) diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 7ef9a7338..4d5946795 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -73,7 +73,7 @@ namespace sat { inline bool simplifier::is_external(bool_var v) const { return s.is_assumption(v) || - (s.is_external(v) && + (s.is_external(v) && s.m_ext && (!m_ext_use_list.get(literal(v, false)).empty() || !m_ext_use_list.get(literal(v, true)).empty())); } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index d42243a06..e15cddbd6 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -62,6 +62,7 @@ namespace sat { m_conflicts_since_init = 0; m_next_simplify = 0; m_num_checkpoints = 0; + m_simplifications = 0; } solver::~solver() { @@ -797,7 +798,6 @@ namespace sat { keep = m_ext->propagate(l, it->get_ext_constraint_idx()); if (m_inconsistent) { if (!keep) { - std::cout << "CONFLICT - but throw away current watch literal\n"; ++it; } CONFLICT_CLEANUP(); @@ -925,6 +925,17 @@ namespace sat { IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-restarts\")\n";); return l_undef; } + 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; + } } } @@ -1411,7 +1422,8 @@ namespace sat { if (m_conflicts_since_init < m_next_simplify) { return; } - IF_VERBOSE(2, verbose_stream() << "(sat.simplify)\n";); + m_simplifications++; + IF_VERBOSE(2, verbose_stream() << "(sat.simplify :simplifications " << m_simplifications << ")\n";); TRACE("sat", tout << "simplify\n";); @@ -1424,11 +1436,11 @@ namespace sat { m_scc(); CASSERT("sat_simplify_bug", check_invariant()); - + m_simplifier(false); CASSERT("sat_simplify_bug", check_invariant()); CASSERT("sat_missed_prop", check_missed_propagation()); - + if (!m_learned.empty()) { m_simplifier(true); CASSERT("sat_missed_prop", check_missed_propagation()); diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 581f557a7..fd8de1ad3 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -367,6 +367,7 @@ namespace sat { unsigned m_conflicts_since_init; unsigned m_restarts; unsigned m_conflicts_since_restart; + unsigned m_simplifications; unsigned m_restart_threshold; unsigned m_luby_idx; unsigned m_conflicts_since_gc;