[gecode-users] Division by zero

[Christian Schulte]

Yes, that is the right definition: the values for x,y,z must be solutions of
div(x,y,z).

There is a standard trick: introduce a new variable y' and reify that if y
!= 0, then y=y' and post div(x,y',z). The problem is that you do not get
much propagation.

Christian

--
Christian Schulte, Professor of Computer Science, KTH,
www.ict.kth.se/~cschulte/


-----Original Message-----
From: users-bounces at gecode.org [mailto:users-bounces at gecode.org] On Behalf
Of Max Ostrowski
Sent: Tuesday, August 27, 2013 11:51 AM
To: users at gecode.org
Subject: [gecode-users] Division by zero

I recognized that the div constraint for integers removes the zero from the
domain of the second argument (to avoid division by zero).
This seems to be a problem as i want to express the following:


x/y+c > 7 reified b

So, if b1 is true, y should not be zero or otherwise some undefined
behaviour happens.
So  i add a constraint

y != 0 reified b

to avoid this case.
(Sometimes it happens that this is done via other boolean variables, more
complex constructs, own propagators etc..., but i always avoid the case that
y is zero if b is true).

To express this in gecode i currently use div(x,y,z); z + c > 7 refied b y
!= 0 reified b

This gives wrong results, as in the case where b is false, y is also
constraint to be != 0 via the div constraint.
I thought about reifying the division with b, but this would also lead to
wrong results.

So any idea how to express this?
Is removing the 0 from the domain via the div constraint really the right
way?
I could live with an undefined behaviour in the case that y \in {0}.

Any ideas?
Best Max

Sample Code follows


class TempSpace : public Space
{
public:

    TempSpace() : x_(*this,4), b_(*this,2)
    {
        x_[0] = IntVar(*this,1,3);
        x_[1] = IntVar(*this,-4,4);
        x_[2] = IntVar(*this, -10,10);
        x_[3] = IntVar(*this, -10,10);
        b_[0] = BoolVar(*this,0,1);
        b_[1] = BoolVar(*this,0,1);

        Gecode::div(*this,x_[0],x_[1],x_[2]);

        if (status()==SS_FAILED)
            std::cout << "failed " << std::endl;
        print();

        IntArgs intArgs;
        IntVarArgs intVarArgs;
        intArgs << 1;
        intVarArgs << x_[2];
        intArgs << 1;
        intVarArgs << x_[3];
        linear(*this, intArgs, intVarArgs, IRT_EQ,0,b_[0],ICL_DEF);

        rel(*this,x_[2],IRT_NQ,0, b_[0], ICL_DEF);

        //rel(*this, b_[0], IRT_EQ, b_[1], ICL_DEF);

        if (status()==SS_FAILED)
            std::cout << "failed " << std::endl;
        print();
        branch(*this, x_, branchVar, branchVal);
    }


    TempSpace(bool share, TempSpace& sp) : Space(share, sp)
    {
        x_.update(*this, share, sp.x_);
        b_.update(*this, share, sp.b_);
    }

    virtual TempSpace* copy(bool share)
    {
        return new TempSpace(share, *this);
    }

    void print()
    {
        std::cout << x_[0] << " " << x_[1] << " " << x_[2] << std::endl;
    }

    virtual ~TempSpace(){}
    void run()
    {
        dfsSearchEngine_ = new DFS<TempSpace>(this);
        while (enumerator_ = dfsSearchEngine_->next())
            enumerator_->print();
    }

    IntVarArray x_;
    BoolVarArray b_;
    DFS<TempSpace>* dfsSearchEngine_;
    TempSpace* enumerator_;
};


_______________________________________________
Gecode users mailing list
users at gecode.org
https://www.gecode.org/mailman/listinfo/gecode-users