Modeling a timeline for task allocation: Arrays?

[AndrewJSchoen]

Hi all,

I am working on an algorithm that requires reasoning about a series of temporally-ordered steps for the purpose of scheduling some tasks. Currently, I have an implementation that uses a discrete number of time-stamps (Ints), and I impose ordered inequality constraints on them to specify ordering. I also have a set of tasks, which each have start and end times, and each of those values need to appear in the set of time-stamps. The times themselves are determined through the solve/optimize function. Thus, I could have a set of time-stamps of

[0, 100, 150, 400, 402, 500, ...]

Where the values are always increasing, but not by an equal amount each time.

However, one thing that is less than ideal about this representation is that while I am able to generate a discrete number of timestamps, this is an over-estimate, and the actual number of timestamps may vary depending on the solution found (since some tasks may start at the same time, etc). The nice capability of Z3's Array is that it supports series of arbitrary length, and you can also utilize capabilities like ForAll, which could conceptually make it cleaner when defining general rules. So, on the surface, it seems like Array might be a better option. Naïvely, this might look something like Array("timeline",IntSort(),StateSort()), using a custom "State" datatype. That being said, I have a couple issues/questions with how it would be implemented, and was wondering if anyone had any thoughts.

1. I read in numerous places that there are some performance costs associated with the Array approach compared to a discrete set. I have a relatively[?] small number of tasks right now (under 10), and things seem to get a bit slower as the number increases, even with the discrete approach. I'm not done, and am hoping that the additional rules help guide the search algorithm to improve this, but ideally I would like to handle many more tasks (e.g. 40+). Does this mean I should definitely stick with a discrete approach, even if it amounts to waste by overestimating the number of necessary time-stamps?
2. In the final version, the individual tasks will define preconditions and postconditions, which will obviously impose constraints about a state space tied to these timestamps. In other words, any state should be identical to the one before it, unless some attribute was modified by a task. However, in a case where the time stamps are irregularly increasing, is this type of reasoning even possible without recreating the current structure that I made in the discrete case, or some additional array that handles the mapping of indices to times? Not sure how intelligible that distinction is, so let me know if that could be clarified further.
3. For the States themselves, right now I am creating data structures in the binding language, which organize the different bools and ints, but presumably with this structure I would need to create a custom datatype for the state. Does this seem like a good idea? Would I still be able to reason about attributes across states, so as to enforce those pre/post conditions?

Thanks for any/all feedback!

[NikolajBjorner]

You want arrays if you are modeling volatile storage. Array entries can be updated.
You can use uninterpreted functions for cases where you don't compare arrays or use updates (the store function).

The most effective way to solve your approach may be a loop outside of z3 where you create models of increased size bounds.
You would need some way to transition from smaller model bounds to larger bounds without completely redoing your encoding, of course. If you can impose the model bound by an assumption, and have a limited number of conditions depend on the assumption the iterate deepening approach may outperform other approaches, especially if the encoding ends up being mostly finite domain.

[AndrewJSchoen]

So, if I am understanding correctly, a discretely-sized model that can grow under certain circumstances would probably be preferable in this case? E.g., start smaller and expand the bounds if necessary?

[NikolajBjorner]

what works totally depends on what is in your model. I am mentioning the iterative deepening approach because you should consider whether this applies.
Independently, I guess you don't need arrays but can use uninterpreted functions.