Formula should not be satisfiable

[juliusbrehme]

Hello everyone,

Consider the following Code:

Box *box = new Box();
Variable x1{"x1", Variable::Type::INTEGER};
Variable x2{"x2", Variable::Type::INTEGER};

Formula f{(x1 != x2) && (x1 < 1) && (x2 < 1) && (0 <= x1) && (0 <= x2)};

bool result = CheckSatisfiability(f, 0.001, box);

The result should be false, because the formula f is not satisfiable, but the result is true. If I print the result from the box, I get the following:

x1 : [0, 0]
x2 : [0, 0]

But this should not be an appropriate result.

Maybe the Issue #304 has something to do with the result as well.

Thank you in advance.

[soonhokong]

Formula f{(x1 != x2) && (x1 < 1) && (x2 < 1) && (0 <= x1) && (0 <= x2)};

Let me rewrite this formula using a list of conjuncts:

• x1 != x2
• x1 < 1
• x2 < 1
• 0 <= x1
• 0 <= x2

The first conjunct x1 != x2 can be rewritten into (x1 > x2) or (x1 < x2) so we have:

• (x1 > x2) or (x1 < x2)
• x1 < 1
• x2 < 1
• 0 <= x1
• 0 <= x2

I'd like to show you that the found model (x1, x2) = (0.0, 0.0) is a solution to the delta-weakening of the original problem. FYI, here is the delta-weakening of the original problem where delta is 0.001.

• (x1 > x2 - 0.001) or (x1 - 0.001 < x2)
• x1 - 0.001 < 1
• x2 - 0.001 < 1
• -0.001 <= x1
• -0.001 <= x2

When x1, x2 = 0.0, 0.0, we have:

• (0 > 0 - 0.001) or (0 - 0.001 < 0)
• -0.001 < 1
• -0.001 < 1
• -0.001 <= 0
• -0.001 <= 0

You can check that all of these conjuncts are true. So this is a delta-sat solution.

[soonhokong]

Reference:

Delta-Decidability over the Reals [arXiv]
Sicun Gao, Jeremy Avigad, and Edmund Clarke
LICS (Logic in Computer Science) 2012