From f009dfcc007b654b192b3c070ecf056c6ce34bb1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 27 Nov 2017 17:05:08 -0800 Subject: [PATCH] update scoring approach Signed-off-by: Nikolaj Bjorner --- src/sat/sat_lookahead.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index b50d7aa2f..fbd237339 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -1452,9 +1452,9 @@ namespace sat { for (nary* n : m_nary[(~l).index()]) { if (sz-- == 0) break; unsigned nonfixed = n->dec_size(); - if (is_true(n->get_head())) continue; + // if (is_true(n->get_head())) continue; if (inconsistent()) continue; - if (nonfixed <= 1) { + if (nonfixed <= 1 && !is_true(n->get_head())) { bool found_conflict = true; for (literal lit : *n) { if (!is_fixed(lit)) { @@ -1473,7 +1473,7 @@ namespace sat { continue; } } - else if (m_search_mode == lookahead_mode::lookahead1) { + if (m_search_mode == lookahead_mode::lookahead1) { SASSERT(nonfixed >= 2); switch (m_config.m_reward_type) { case heule_schur_reward: {