From d26f0e1c28e9784e5c931dc326cc300089d8d03b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 9 Apr 2013 08:42:14 -0700 Subject: [PATCH 1/2] Fix bug in the SAT solver. Signed-off-by: Leonardo de Moura --- src/sat/sat_solver.cpp | 54 ++++++++++++++++++++++++++++++++++++++---- 1 file changed, 50 insertions(+), 4 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 399fb2c61..3e9b60260 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1745,6 +1745,12 @@ namespace sat { mark_lit(m_lemma[i]); } + literal l0 = m_lemma[0]; + // l0 is the FUIP, and we never remove the FUIP. + // + // In the following loop, we use unmark_lit(l) to remove a + // literal from m_lemma. + for (unsigned i = 0; i < sz; i++) { literal l = m_lemma[i]; if (!is_marked_lit(l)) @@ -1754,9 +1760,15 @@ namespace sat { watch_list::const_iterator it = wlist.begin(); watch_list::const_iterator end = wlist.end(); for (; it != end; ++it) { + // In this for-loop, the conditions l0 != ~l2 and l0 != ~l3 + // are not really needed if the solver does not miss unit propagations. + // However, we add them anyway because we don't want to rely on this + // property of the propagator. + // For example, if this property is relaxed in the future, then the code + // without the conditions l0 != ~l2 and l0 != ~l3 may remove the FUIP if (it->is_binary_clause()) { literal l2 = it->get_literal(); - if (is_marked_lit(~l2)) { + if (is_marked_lit(~l2) && l0 != ~l2) { // eliminate ~l2 from lemma because we have the clause l \/ l2 unmark_lit(~l2); } @@ -1764,11 +1776,11 @@ namespace sat { else if (it->is_ternary_clause()) { literal l2 = it->get_literal1(); literal l3 = it->get_literal2(); - if (is_marked_lit(l2) && is_marked_lit(~l3)) { + if (is_marked_lit(l2) && is_marked_lit(~l3) && l0 != ~l3) { // eliminate ~l3 from lemma because we have the clause l \/ l2 \/ l3 unmark_lit(~l3); } - else if (is_marked_lit(~l2) && is_marked_lit(l3)) { + else if (is_marked_lit(~l2) && is_marked_lit(l3) && l0 != ~l2) { // eliminate ~l2 from lemma because we have the clause l \/ l2 \/ l3 unmark_lit(~l2); } @@ -1786,7 +1798,41 @@ namespace sat { literal_vector::iterator end = implied_lits->end(); for (; it != end; ++it) { literal l2 = *it; - if (is_marked_lit(~l2)) { + // Here, we must check l0 != ~l2. + // l \/ l2 is an implied binary clause. + // However, it may have been deduced using a lemma that has been deleted. + // For example, consider the following sequence of events: + // + // 1. Initial clause database: + // + // l \/ ~p1 + // p1 \/ ~p2 + // p2 \/ ~p3 + // p3 \/ ~p4 + // q1 \/ q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2 + // q1 \/ ~q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2 + // ~q1 \/ q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2 + // ~q1 \/ ~q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2 + // ... + // + // 2. Now suppose we learned the lemma + // + // p1 \/ p2 \/ p3 \/ p4 \/ l2 (*) + // + // 3. Probing is executed and we notice hat (~l => l2) when we assign l to false. + // That is, l \/ l2 is an implied clause. Note that probing does not add + // this clause to the clause database (there are too many). + // + // 4. Lemma (*) is deleted (garbage collected). + // + // 5. l is decided to be false, p1, p2, p3 and p4 are propagated using BCP, + // but l2 is not since the lemma (*) was deleted. + // + // Probing module still "knows" that l \/ l2 is valid binary clause + // + // 6. A new lemma is created where ~l2 is the FUIP and the lemma also contains l. + // If we remove l0 != ~l2 may try to delete the FUIP. + if (is_marked_lit(~l2) && l0 != ~l2) { // eliminate ~l2 from lemma because we have the clause l \/ l2 unmark_lit(~l2); } From d5a14c0b51bf5a7a25dc450b81288dda56c915fb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 9 Apr 2013 08:49:04 -0700 Subject: [PATCH 2/2] Fix problem reported at http://stackoverflow.com/questions/15882140/z3-smt2-in-get-z3-version/15882868#comment22637420_15882868 Signed-off-by: Leonardo de Moura --- src/cmd_context/basic_cmds.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 21a986fda..9f18608d3 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -568,7 +568,7 @@ public: ctx.regular_stream() << "(:authors \"Leonardo de Moura and Nikolaj Bjorner\")" << std::endl; } else if (opt == m_version) { - ctx.regular_stream() << "(:version \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "\")" << std::endl; + ctx.regular_stream() << "(:version \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "\")" << std::endl; } else if (opt == m_status) { ctx.regular_stream() << "(:status " << ctx.get_status() << ")" << std::endl;