You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
A few examples of models finding a constant function on a domain of fixed size (in this case 64, but easily modified):
a)
letting m be 64
find dmap : function int(1..m) --> int(0..0)
such that forAll p : int(1..m) . dmap(p) = 0
b)
letting m be 64
find d : set of int(1..m)
maximising |d|
find dmap : function int(1..m) --> int(0..0)
such that forAll p in d . dmap(p) = 0
d)
letting n be 6
find dmap : function set of int(1..n) --> int(0..0)
such that forAll p : set of int(1..n) . dmap(p) = 0
c)
find dmap : function set of int(0..5) --> int(0..0)
such that forAll p in powerSet({0,1,2,3,4,5}) . dmap(p) = 0
Using the size of the generated minion model as a very rough, easy benchmark of performance, these examples behave very differently:
Model (a) does not scale with m: the generated minion model is of fixed size.
Model (b) grows linearly as m increases - roughly 16kb for m=64 on my system.
Models (c) and (d) grow quadratically with the size of domain (i.e. fourth-power growth with n) - roughly 3.5mb for n=6 on my system. The two models differ slightly, but not by much.
Obviously on their own these are not hugely consequential examples, but I have found that when attempting to work with objects of actual interest, the file sizes quickly scale into hundreds of mb (and based on observed growth, beyond), becoming functionally unsolvable. It would be helpful if a much wider range of functions were supported efficiently.
From discussion with Oz, it seems this is due to the latter cases needing to fall back to FunctionAsRelation, rather than using Function1DPartial.
The text was updated successfully, but these errors were encountered:
A few examples of models finding a constant function on a domain of fixed size (in this case 64, but easily modified):
a)
b)
d)
c)
Using the size of the generated minion model as a very rough, easy benchmark of performance, these examples behave very differently:
m
: the generated minion model is of fixed size.m
increases - roughly 16kb form=64
on my system.n
) - roughly 3.5mb forn=6
on my system. The two models differ slightly, but not by much.Obviously on their own these are not hugely consequential examples, but I have found that when attempting to work with objects of actual interest, the file sizes quickly scale into hundreds of mb (and based on observed growth, beyond), becoming functionally unsolvable. It would be helpful if a much wider range of functions were supported efficiently.
From discussion with Oz, it seems this is due to the latter cases needing to fall back to
FunctionAsRelation
, rather than usingFunction1DPartial
.The text was updated successfully, but these errors were encountered: