choco-solver icon indicating copy to clipboard operation
choco-solver copied to clipboard

Improve Expression Compilation

Open arnaud-m opened this issue 2 years ago • 7 comments

Hi choco team,

I hope that you are doing well.

Is your feature request related to a problem? Please describe.

Choco provides a convenient expression builder that is then compiled into a set of constraints. It is a complicated task, but some improvements seems possible. For instance, reification is not needed when there is a simple conjunction of constraint.

Let us consider the following model.

Model model = new Model();
IntVar x = model.intVar("x", 1, 9);
IntVar y = model.intVar("y", 0, 9);
IntVar z = model.intVar("z", 0, 9);

x.le(y).and(z.ge(x)).post();
// x.le(y).and(z.ge(x)).decompose().post(); // do not change anything here
System.out.println(model);

The output is the following.

satisfaction  : undefined
== variables ==
x = {1..9}
y = {0..9}
z = {0..9}
LE_exp_1 = [0,1]
GE_exp_2 = [0,1]
cste -- 2 = 2
== constraints ==
BASIC_REIF ([(x < y + 1) <=> LE_exp_1])
BASIC_REIF ([(x < z + 1) <=> GE_exp_2])
ARITHM ([LE_exp_1 = [0,1] + GE_exp_2 = [0,1] = 2])

Describe the solution you'd like I want the conjunction to be posted as independent constraints.

x.le(y).post()
z.ge(x)).post();

Describe alternatives you've considered

The immediate answer is to post multiple constraints, but, in my case, the expression is also built automatically.

arnaud-m avatar Oct 20 '22 08:10 arnaud-m

Hello

First of all, using post() or decompose().post() on a relational expression makes no difference. Indeed, as specified in the Javadoc of post() : Post the decomposition of this expression in the solver (Ok, I agree, it could be more precise, with a link to decompose()). The alternative to decompose() is extension(), but that doesn't answer your question.

About the decomposition itself: on a call to decompose() there is no indication wether or not the constraint will be posted or reified thereafter. That's why the method returns a Constraint object which can possibly reified (while keeping the overall relation correct).

I can see one possible solution, but it seems very specific. NaLoExpression could override the post() method only for the AND case to bypass the call to decompose(). But in that case, there would be a different result calling re.post() or re.decompose().post(), I don't thing that a good idea.

That said, I agree that there is a need for a deep analysis of expressions. For instance, scalar product could be detected and posted. One could also think of a behavior close to what is done for continuous expressions. They can either be turned into Ibex constraints or embedded into an equation constraint that applies HC4 algorithm.

cprudhom avatar Oct 20 '22 11:10 cprudhom

Hi Charles,

I missed your answer, but my investigation leads me to the same conclusion. I understand that it is risky to have different behaviours of post and decompose.post only for AND.

I also encounters the lack of detection for scalar/sum constraints.

Thanks. Now, I am sure about how to solve my main problem (AND).

Do you have any references about the simplification of an arithmetic expression ?

arnaud-m avatar Oct 20 '22 15:10 arnaud-m

Hi,

I have another question related to the expression. What has changed since version 4.10.6 ? In 4.10.10, I have some tests that now raise an exception stating that I must reduce the bounds ?

Thanks.

arnaud-m avatar Oct 21 '22 06:10 arnaud-m

Many things :) Can you share an example?

cprudhom avatar Oct 21 '22 07:10 cprudhom

Do you have any references about the simplification of an arithmetic expression ?

I didn't find anything really useful, but I admit I didn't look very long.

cprudhom avatar Oct 21 '22 07:10 cprudhom

Can you share an example?

Not now because it it not immediate to extract a minimal complete example from my code. But, I will do it for Monday.

arnaud-m avatar Oct 21 '22 07:10 arnaud-m

Do you have any references about the simplification of an arithmetic expression ?

You can have a look at this thread, which maybe a good starting point.

But, it seems that a rewriting rules system is needed

cprudhom avatar Oct 21 '22 08:10 cprudhom