From 686973b4d755e522fc85114218c14fd0b879354c Mon Sep 17 00:00:00 2001 From: Benjamin Kaufmann Date: Sun, 1 Oct 2023 08:10:07 +0200 Subject: [PATCH] Issue #96: Fix LevelWeight comparison. * MinimizeBuilder::CmpWeight failed to handle missing levels correctly. In particular, if a tuple R with *negative* weight w at level p was compared to a tuple L with missing weight at p, RHS was incorrectly considered to be greater than L. Fix this so that now the weight at p is compared to 0 (no weight at p). --- src/minimize_constraint.cpp | 4 +++- tests/minimize_test.cpp | 32 ++++++++++++++++++++++++++++++++ 2 files changed, 35 insertions(+), 1 deletion(-) diff --git a/src/minimize_constraint.cpp b/src/minimize_constraint.cpp index 498c1ff..f6fa29d 100644 --- a/src/minimize_constraint.cpp +++ b/src/minimize_constraint.cpp @@ -617,7 +617,9 @@ bool MinimizeBuilder::CmpWeight::operator()(const MLit& lhs, const MLit& rhs) co const SharedData::LevelWeight* wLhs = &(*weights)[lhs.weight]; const SharedData::LevelWeight* wRhs = &(*weights)[rhs.weight]; for (;; ++wLhs, ++wRhs) { - if (wLhs->level != wRhs->level) { return wLhs->level < wRhs->level; } + if (wLhs->level != wRhs->level) { + return wLhs->level < wRhs->level ? wLhs->weight > 0 : 0 > wRhs->weight; + } if (wLhs->weight != wRhs->weight){ return wLhs->weight > wRhs->weight; } if (!wLhs->next) { return wRhs->next && (++wRhs)->weight < 0; } if (!wRhs->next) { ++wLhs; break; } diff --git a/tests/minimize_test.cpp b/tests/minimize_test.cpp index 394f164..6e3bd7a 100644 --- a/tests/minimize_test.cpp +++ b/tests/minimize_test.cpp @@ -247,6 +247,38 @@ TEST_CASE("Model-guided minimize", "[constraint][asp]") { REQUIRE((newMin->shared()->weights[0].weight == 1)); REQUIRE((newMin->shared()->weights[1].weight == -5)); } + SECTION("testSparseCompare") { + mb.add(0, WeightLiteral(b, 1)); + mb.add(1, WeightLiteral(a, 1)); + mb.add(2, WeightLiteral(c, -1)); + mb.add(2, WeightLiteral(b, -2)); + mb.add(2, WeightLiteral(a, -2)); + + newMin = test.buildAndAttach(mb); + MinimizeConstraint::SharedDataP shared = newMin->shared(); + +#define CHECK_LEVEL_WEIGHT(idx, w, l, n) \ + CHECK(shared->weights.at(idx).weight == w); \ + CHECK(shared->weights.at(idx).level == l); \ + CHECK(shared->weights.at(idx).next == n) + + REQUIRE(test.countMinLits() == 3); + + CHECK(shared->lits[0] == WeightLiteral(~b, 0)); + CHECK_LEVEL_WEIGHT(0, 2, 0, 1); + CHECK_LEVEL_WEIGHT(1, -1, 2, 0); + + CHECK(shared->lits[1] == WeightLiteral(~a, 2)); + CHECK_LEVEL_WEIGHT(2, 2, 0, 1); + CHECK_LEVEL_WEIGHT(3, -1, 1, 0); + + CHECK(shared->lits[2] == WeightLiteral(~c, 4)); + CHECK_LEVEL_WEIGHT(4, 1, 0, 0); + + CHECK(shared->adjust(0) == -5); + CHECK(shared->adjust(1) == 1); + CHECK(shared->adjust(2) == 1); + } SECTION("testInitFromOther") { min.push_back( WeightLiteral(~a, 2) ); min.push_back( WeightLiteral(~a, -3));