astra-uu-se / atlantis

CBLS solver
2 stars 1 forks source link

Bug in the Linear invariant #75

Closed maartenflippo closed 2 years ago

maartenflippo commented 2 years ago

After 4 days of debugging mysterious behavior, I believe to have found a bug in the Linear invariant implementation. Below is a test case which should pass, but doesn't. It is an NQueens model with 2 moves performed on it, and transitions through the following assignments.

   (A)              (B)              (C)
+-+-+-+-+        +-+-+-+-+        +-+-+-+-+
|x|x|x|x|        |x| | | |        | | | | |
+-+-+-+-+        +-+-+-+-+        +-+-+-+-+
| | | | |        | | | | |        | | | | |
+-+-+-+-+   ->   +-+-+-+-+   ->   +-+-+-+-+
| | | | |        | | |x|x|        |x| |x|x|
+-+-+-+-+        +-+-+-+-+        +-+-+-+-+
| | | | |        | |x| | |        | |x| | |
+-+-+-+-+        +-+-+-+-+        +-+-+-+-+

From the testcase we can see the AllDifferent constraints actually produce the correct results. However, at the end of the test case, the error becomes obvious: 2 + 1 + 1 != 2. From my time spent in the debugger it seems like the _localVarArray does not stay up to date with the actually variable values.

#include <gtest/gtest.h>

#include "constraints/allDifferent.hpp"
#include "core/propagationEngine.hpp"
#include "invariants/linear.hpp"
#include "views/intOffsetView.hpp"

TEST(NQueens, some_test) {
  PropagationEngine engine;

  std::vector<VarId> queens;
  std::vector<VarId> q_offset_plus;
  std::vector<VarId> q_offset_minus;

  const int n = 4;

  engine.open();
  for (Int i = 0; i < n; ++i) {
    const VarId q = engine.makeIntVar(1, 1, n);
    queens.push_back(q);
    q_offset_minus.push_back(engine.makeIntView<IntOffsetView>(q, -i));
    q_offset_plus.push_back(engine.makeIntView<IntOffsetView>(q, i));
  }

  auto violation1 = engine.makeIntVar(0, 0, n);
  auto violation2 = engine.makeIntVar(0, 0, n);
  auto violation3 = engine.makeIntVar(0, 0, n);

  engine.makeConstraint<AllDifferent>(violation1, queens);
  engine.makeConstraint<AllDifferent>(violation2, q_offset_minus);
  engine.makeConstraint<AllDifferent>(violation3, q_offset_plus);

  auto total_violation = engine.makeIntVar(0, 0, 3 * n);

  engine.makeInvariant<Linear>(
      std::vector<VarId>{violation1, violation2, violation3}, total_violation);

  engine.close();

  engine.beginMove();
  std::vector<Int> initial{1, 4, 3, 3};
  for (size_t i = 0; i < queens.size(); i++)
    engine.setValue(queens[i], initial[i]);
  engine.endMove();

  engine.beginCommit();
  engine.query(total_violation);
  engine.endCommit();

  EXPECT_EQ(engine.committedValue(violation1), 1); // OK!
  EXPECT_EQ(engine.committedValue(violation2), 1); // OK!
  EXPECT_EQ(engine.committedValue(violation3), 1); // OK!
  EXPECT_EQ(engine.committedValue(total_violation), 3); // OK!

  engine.beginMove();
  engine.setValue(queens[0], 3);
  engine.endMove();

  engine.beginCommit();
  engine.query(total_violation);
  engine.endCommit();

  EXPECT_EQ(engine.committedValue(violation1), 2); // OK!
  EXPECT_EQ(engine.committedValue(violation2), 1); // OK!
  EXPECT_EQ(engine.committedValue(violation3), 1); // OK!
  EXPECT_EQ(engine.committedValue(total_violation), 4); // Fail - Actual value: 2
}
frejknutarlewander commented 2 years ago

Fixed with: https://github.com/astra-uu-se/cbls/pull/77