Incorrect solution to forall problem

[cgd8d]

Input:

(set-logic QF_NRA)
(set-info :precision 0.001)

(declare-fun x () Real [-1, 2])
(declare-fun forall y () Real [-1, 2])

(assert (
     forall (
           (y Real)
     )
     (or
           (or
                (>= y 1)
                (<= y 0)
           )
           (>= x y)
     )
))
(check-sat)
(exit)

Output:

Solution:
x : [-1, 2] = [0.500732421875, 0.50146484375]
delta-sat with delta = 0.00100000000000000

This result is incorrect (eg. by selecting y = 0.75); x should be in the range [1, 2] for the problem to be satisfied.

I think the reason is partly because of the nested ORs, which the function “find_CE_via_underapprox” doesn’t traverse. The following patch should fix that part of the issue, but is not a complete fix; it changes the result from an incorrect solution to unsat, which is still wrong. The partial patch I’ve written is:

--- a/src/contractor/contractor_generic_forall.cpp
+++ b/src/contractor/contractor_generic_forall.cpp
@@ -374,7 +374,19 @@ box find_CE_via_underapprox(box const & b, unordered_set<Enode*> const & forall_
             e = e->get1st();
             polarity = !polarity;
         }
-        if (e->isOr() || e->isAnd()) {
+
+        if (e->isOr()) {
+            vector<Enode*> local_vec;
+            assert(!e->getCdr()->isEnil());
+            assert(!e->getCdr()->getCdr()->isEnil());
+            assert(e->getCdr()->getCdr()->getCdr()->isEnil()); // Verify there are only two arguments.
+            local_vec.push_back(e->getCdr()->getCar());
+            local_vec.push_back(e->getCdr()->getCdr()->getCar());
+            counterexample = find_CE_via_underapprox(counterexample, unordered_set<Enode*>(), local_vec, p, config);
+            continue;
+        }
+
+        if (e->isAnd()) {
             break;
         }
         nonlinear_constraint ctr(e, var_set, polarity);
@@ -395,9 +407,6 @@ box find_CE_via_underapprox(box const & b, unordered_set<Enode*> const & forall_
             throw runtime_error(ss.str());
         }
     }
-    if (!iv.is_empty()) {
-        iv = iv.mid();
-    }
     return counterexample;
}

@@ -430,6 +439,9 @@ box contractor_generic_forall::find_CE(box const & b, unordered_set<Enode*> cons
     // static unsigned over_approx = 0;
     box counterexample = find_CE_via_underapprox(b, forall_vars, vec, p, config);
     if (!counterexample.is_empty()) {
+
+        counterexample.get_values() = counterexample.get_values().mid();
+
         // ++under_approx;
         // cerr << "WE USE UNDERAPPROX: " << under_approx << "/" << over_approx<< "/" << (under_approx + over_approx) << endl;
         // cerr << counterexample << endl;

I’m unsure why the code, patched this way, still reports unsat rather than a correct solution.

[soonhokong]

It's related to the previous problem. In short, we need to do pre-processing and only handle a conjunction of theory literals inside of find_CE_via_underapprox.

[cgd8d]

Thanks. I'm sorry if I keep filing different forms of the same issue, but I'm not sure I understand in this case what the preprocessing should generate. In #272 you mentioned problems should be provided in CNF form; I think this problem is already in CNF, since it consists of only disjunctions.

[cgd8d]

I believe I’ve found a patch which addresses this issue, though it’s probably not the best one. It does two things.

First, flattens long sequences of ORs, so that handle_disjunction is not presented with an enode which is itself an OR. (This can happen even for expressions which are already in CNF form, as I believe the current example shows.)

Second, for this input ibex’s ibwd operation returns an interval which is larger than the input argument, which I think is unintended behavior from ibex. The patch works around that by explicitly enforcing the behavior that in find_CE_via_underapprox, ibwd should never enlarge counterexample.

The patch I’ve written is:

diff --git a/src/contractor/contractor_generic_forall.cpp b/src/contractor/contractor_generic_forall.cpp
index e6db4dc..13e559b 100644
--- a/src/contractor/contractor_generic_forall.cpp
+++ b/src/contractor/contractor_generic_forall.cpp
@@ -383,6 +383,7 @@ box find_CE_via_underapprox(box const & b, unordered_set<Enode*> const & forall_
         }
         auto numctr = ctr.get_numctr();
         // Construct iv from box b
+        ibex::IntervalVector iv_copy = iv;
         if (numctr->op == ibex::CmpOp::GT || numctr->op == ibex::CmpOp::GEQ) {
             numctr->f.ibwd(ibex::Interval(0.0, POS_INFINITY), iv);
         } else if (numctr->op == ibex::CmpOp::LT || numctr->op == ibex::CmpOp::LEQ) {
@@ -394,6 +395,7 @@ box find_CE_via_underapprox(box const & b, unordered_set<Enode*> const & forall_
             ss << "find_CE_via_underapprox: unknown constraint type, " << *numctr;
             throw runtime_error(ss.str());
         }
+        iv &= iv_copy;
         if (iv.is_empty()) {
             // stop when counterexample is already empty;
             return counterexample;
@@ -458,6 +460,23 @@ void contractor_generic_forall::handle_disjunction(contractor_status & cs, vecto
         forall_vars.insert(vars.begin(), vars.end());
     }

+    // If any of the enodes in vec is an OR, break it apart and call this function recursively.
+    for(size_t i = 0; i < vec.size(); i++) {
+        if(vec.at(i)->isOr()) {
+            assert(!vec.at(i)->getCdr()->isEnil());
+            assert(!vec.at(i)->getCdr()->getCdr()->isEnil());
+            assert( vec.at(i)->getCdr()->getCdr()->getCdr()->isEnil()); // Verify vec.at(i) has exactly two arguments to OR.
+            Enode* e1 = vec.at(i)->getCdr()->getCar();
+            Enode* e2 = vec.at(i)->getCdr()->getCdr()->getCar();
+            std::vector<Enode*> local_vec = vec;
+            local_vec[i] = e1;
+            local_vec.push_back(e2);
+            handle_disjunction(cs, local_vec, p);
+            return;
+        }
+    }
+
+    // vec does not contain any nested OR terms; continue.
     unordered_map<Enode*, ibex::Interval> subst;
     if (!forall_vars.empty()) {
         // Step 2. Find a counter-example

Does this seem like the right approach to patching this issue?

[soonhokong]

@cgd8d, thanks for the patches. I'll take a closer look at them and merge them into the repository.

[soonhokong]

Could you give us a small example where ibex contractor violates monotonicity property? I can take a look and possibly fix the problem on ibex side (or report the problem to the team).

[cgd8d]

Applying the patch so that nested ORs are traversed (the part of the diff which is applied to handle_disjunction), I found that the input at the top of the thread did exactly that. Maybe this could be confirmed by replacing "iv &= iv_copy" in the patch with an assertion that iv is a subset of iv_copy?

[soonhokong]

@cgd8d, sorry for the delay. I'll check it soon.

[soonho-tri]

@cgd8d, I'll do the flattening at the parsing time so that the rest do not need to worry about it.

[soonho-tri]

Closed by 4ac1aa86048d144c488aa9cdd2c001a465ac1d5d. Related Issue: #284.

[soonho-tri]

@cgd8d, please check out the latest source code and try the example at the top. When I tested it, it returned unsat which is the correct answer.

I still have a concern with your comment on IBEX:

Second, for this input ibex’s ibwd operation returns an interval which is larger than the input argument, which I think is unintended behavior from ibex.

If this is still the case, I'd like to fix it. Could you give me a reproducible example? For instance, with a box B1 and a constraint C1, IBEX returns B2 which is not included in B1.

[cgd8d]

@soonho-tri , thanks for tackling the flattening issue! Unfortunately unsat is not the right answer -- the problem is satisfied, for example, by x = 1.5.

To trigger an appropriate assertion, try applying the following diff (tested against 5ba4d8a):

diff --git a/src/contractor/contractor_generic_forall.cpp b/src/contractor/contractor_generic_forall.cpp
index e6db4dc..9720a6b 100644
--- a/src/contractor/contractor_generic_forall.cpp
+++ b/src/contractor/contractor_generic_forall.cpp
@@ -384,7 +384,9 @@ box find_CE_via_underapprox(box const & b, unordered_set<Enode*> const & forall_
         auto numctr = ctr.get_numctr();
         // Construct iv from box b
         if (numctr->op == ibex::CmpOp::GT || numctr->op == ibex::CmpOp::GEQ) {
+            ibex::IntervalVector iv_copy = iv;
             numctr->f.ibwd(ibex::Interval(0.0, POS_INFINITY), iv);
+            assert(iv.is_subset(iv_copy));
         } else if (numctr->op == ibex::CmpOp::LT || numctr->op == ibex::CmpOp::LEQ) {
             numctr->f.ibwd(ibex::Interval(NEG_INFINITY, 0.0), iv);
         } else if (numctr->op == ibex::CmpOp::EQ) {

Run on the testcase above, this triggers an assertion. Is this enough to reproduce?

[soonho-tri]

Oh, I see. I'll check that.

[soonho-tri]

I think that the current behavior of IBEX is correct according to the documentation http://www.ibex-lib.org/doc/interval.html?highlight=backward%20operator#backward-operators. It's just the case that we need to take an intersection between the result and the input. I just added a patch aee385f73a02e252112fe2c305d1e38192699930. After applying the patch, it should return delta-sat for the example.

[cgd8d]

OK, that's great -- thanks!