Re: [eclipse-clp-users] Time out issue with long integer

From: Joachim Schimpf <jschimpf_at_...311...>
Date: Wed, 10 Dec 2014 14:52:42 +0000
On 10/12/14 02:13, Edgaonkar, Shrirang wrote:
> Dear clp users,
>     I have the following problem. I am trying to get the value for IN_FORMULA1.
> Here I need to use indomain_min since I need the minimum value satisfying the
> equation. I could use indomain_split but it wont ensure the value is minimum.
> But using indomain_min, it takes infinite time to resolve the equation. Any
> pointers on this?
> :-lib(ic).
> solve(IN_FORMULA1):-
> %%Domain
> IN_FORMULA1 :: [-9223372036854775808 .. 9223372036854775807],
> %%Constraints
> (IN_FORMULA1 $> 115000000000),
> %%Search
> search([IN_FORMULA1], 0, input_order, indomain_min, complete, []).

You seem to have run into quite a curious bug, related to the size (~10^19) of 
your variable domain.  I'll look into fixing this later.

Generally speaking, when working with integers, you should make your variable 
domains as tight as possible.  Any enumeration-based search method is likely to 
be hopeless when applied to such domain sizes.  Remember that the size of the 
search space is the product of all the domain sizes, which quickly becomes 
astronomical.  Is there a particular reason you are choosing these initial 
bounds of 2^63?  The ic-library represents bounds as double floats, therefore it 
is more efficient (and avoids the bug you have encountered) when you keep 
integer bounds in the range -2^51..2^51.  In practice, integer bounds should be 
much lower than that for a tractable constraint model.

As to your remark about the enumeration order: indomain_split (which doesn't 
exhibit the bug) will generate solutions in the same order as indomain_min, so 
there is no reason not to use it.  On large domains, splitting is usually 
advantageous, because it can eliminate large ranges of search space in one step.

-- Joachim
Received on Wed Dec 10 2014 - 14:52:52 CET

This archive was generated by hypermail 2.2.0 : Mon Jul 09 2018 - 02:05:30 CEST