I'm working on automated planning using a SAT solver and encountering a challenge in efficiently encoding an "at most one" constraint across multiple time steps. Specifically, the constraint ensures that a truck (t1) can be at only one city at any given time step. While encoding this constraint individually for each time step is straightforward, I'm seeking a method to abstract this encoding to avoid repetition for every time step.
Example scenario
In my model, I have variables like at_t1_c1__t, at_t1_c2__t, ..., at_t1_cn__t representing the truck being in one of n cities at time step t. For a single time step (say 0), I use at_most_one(at_t1_c1__0, at_t1_c2__0, ..., at_t1_cn__0) to indicate that a truck can only be at one city at a specific time step. However, as the number of time steps, the number of trucks and the number of cities increases in the planning problem, this approach becomes cumbersome.
Current approach
I am currently re-encoding the "at most one" constraint for each time step where I need it, leading to repetition and potential inefficiency as the number of time steps grows in the planning scenario.
Question
Is there a way to abstract the "at most one" constraint such that it can be defined once and then applied or linked to each time step without re-encoding it each time? I'm not concerned about how the "at most one" constraint is implemented (whether through pairwise comparisons, binary encoding, etc.). My primary goal is to find a method to generalize this rule and effectively apply it across multiple time steps.
I'm not sure at all that it can be possible, but if you have any insights, suggestions, or examples on how to approach this problem, it would be greatly appreciated.