From 8db3b537b1dd132fe2f31ee47ff7f294061d6df9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 17 Apr 2023 16:21:58 -0700 Subject: [PATCH] commenting on anachornistic propagation code --- src/math/polysat/solver.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 9d4d615dc..e9cf339a3 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -259,6 +259,14 @@ namespace polysat { // - When building the viable lemma, one of the linking constraints happens to be L // - L is bool-true but eval-false --> we actually have a bool/eval conflict that we didn't detect // - the viable lemma is problematic because L is bool-true + + // NSB comment: + // It seems the core of the issue is that conflict resolution should have identified + // L as the top-most literal that the conflict depends on instead of using L'. + // The conflict state includes the propagation of values that could be triggered by L. + // Take the SAT solver analogy, conflict resolution walks the assignment stack to find the + // youngest assignment that is part of the conflict. It then starts resolving against the youngest + // literal assignment. auto const& item = m_search[eval_qhead++]; if (item.is_assignment()) { // LOG_H1("P2: eval pvar v" << item.var());