Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Possible improvements to abs/1 #6

Open
JCumin opened this issue Oct 27, 2016 · 4 comments
Open

Possible improvements to abs/1 #6

JCumin opened this issue Oct 27, 2016 · 4 comments

Comments

@JCumin
Copy link

JCumin commented Oct 27, 2016

(Tested on SWI's CLP(FD), though I assume the same problem exists in CLP(Z))

Weak propagation

?- X #= abs(X) + 1.
X in 2..sup,
_G2048+1#=X,
_G2048#=abs(X),
_G2048 in 2..sup.

This could directly fail. As a result it takes a long time for this to fail, even though it is obvious that it will:

?- time((X #= abs(X) + 1, X in 1..100000, indomain(X))).
% 17,551,054 inferences, 65.037 CPU in 65.061 seconds (100% CPU, 269863 Lips)
false.

Redundant constraint

?- X #= abs(X).
X in 0..sup,
X#=abs(X).

This correctly constrains X to 0..sup from inf..sup, but then the X#=abs(X) constraint is completely unnecessary.

@JCumin JCumin changed the title Various problems with abs/1 Possible improvements to abs/1 Oct 27, 2016
@triska
Copy link
Owner

triska commented Oct 29, 2016

These are very good observations, thank you!

Do these issues arise an actual use cases? The reason I ask is the following:

Please tell me the (still reasonable) most general pattern of these types that you would like CLP(Z) to handle more efficiently.

For example, X #= abs(X) + 1 is clearly of the form X #= abs(X) + N, where N is a positive integer. Would this cover most of your cases? Or is there something more general for which you need stronger propagation too?

I will start working on this issue by making X #= abs(X) + N stronger, please think in the meantime about further cases like this.

And: Yes, for X #= abs(X) and X #= abs(X) + 0, the abs constraint is clearly entailed. I will also work on this.

@triska
Copy link
Owner

triska commented Oct 30, 2016

Please try the latest version: I have implemented this suggestion and would greatly appreciate your feedback.

@JCumin
Copy link
Author

JCumin commented Nov 5, 2016

I'm not quite sure what you actually implemented; in anycase here's the following observation:

  • abs(X) #= 1+X, X in 1..10000, indomain(X) still takes a few seconds
  • abs(X) #= 2*X, X in 1..100000000000000, indomain(X) is instantaneous

Seems that addition does not propagate as strongly as multiplication in that case. Though note that 2*(1+X) is instant while 1*(1+X) is not, even though both are impossible. I'm not sure if this is easily imporovable without propagating too strongly in other cases.

Another note:

?- abs(X) #= -X.
clpz:(_A#=abs(X)),
clpz:(-1*X#=_A),
clpz:(X in inf..0),
clpz:(_A in 0..sup) ? 
yes

Like abs(X) #= X, this could be simplified into X in inf..0.

(I am definitely not a fan of SICStus REPL...)

@triska
Copy link
Owner

triska commented Nov 5, 2016

So far, I have implemented specifically the cases you mentioned in your original post.

For example, the following is now instantaneous:

?- X #= abs(X) + 1, X in 1..10000, indomain(X).

This is because the specific form of the constraint is now handled via a dedicated propagator, which is applied if the posted constraint is subsumed by the symbolic pattern:

Var #= abs(Var) + Expr

where Var is a variable.

CLP(Z) has dedicated propagators for patterns of constraints that frequently occur in practice, and which can be handled more efficiently when they are taken into account in their entirety instead of decomposing them.

Ongoing work on CLP(Z) also involves extending the recognizer with further patterns that users request. This is the usual way of constraint-based development: We extend and improve the solver so that it handles these patterns more efficiently.

The challenge here is to generalize such patterns as far as possible, so that a small number of patterns suffice to recognize the cases that are important for you in practice.

For example, to capture the constraints you originally reported, I added to matches/1 the following lines:

         m_c(var(X) #= abs(var(Y)) + any(V0), X == Y) => [d(V0,V),p(x_eq_abs_plus_v(X,V))],
         m_c(var(X) #= abs(var(Y)) - any(V0), X == Y) => [d(-V0,V),p(x_eq_abs_plus_v(X,V))],

The syntax of these rules is explained in my thesis, please have a look.

You have now reported an additional case for which you would like to have stronger propagation, which is not captured by the pattern above:

abs(X) #= 1 + X

It is easy to extend the recognizer accordingly, please try it out so that you see how to extend and adapt CLP(Z) for your use cases.

The other new example, abs(X) #= -X, can also be handled with a dedicated rule, please try it out.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants