Auto-Planning
We use OR tools for this. https://developers.google.com/optimization/cp/cp_solver
This generates a constraint statisfaction problem for autoplanning, which is then solved by our solver provided by google.
This was recommended by @Martin Knezevic (Unlicensed) over in Notangles, who used it in their implementation of anhttps://devsoc.atlassian.net/wiki/pages/createpage.action?spaceKey=N&title=Autotimetabler . I also saw https://www.unsw.edu.au/staff/abdallah-saffidine Implement a similar solver last year in an old project I was working on. He used a different solver though.
This solver is a Satisfiability (SAT) Solver which uses a constraint satisfaction problem (CSP) interface.
for further motivation, look at my blog post: https://dev.csesoc.org.au/p/54a4cb34-ff8c-4564-b7cc-4b68b3c07d65/ where I go into excruciating detail about why this is the most appropriate tool, and what it is.
Why?
there are a few reasons why using this instead of a greedy but unoptimal solution is better.
If the solution exists, we will find it.
this solver actually serves 2 purposes. It will find the solution if it exists, and will only terminate if it can guarantee that your problem has no solutions.We can target optimization of certain parameters.
It is easy to extend this implementation of auto-planning to minimise the number of terms taken, the average number of courses in a term, etc. https://developers.google.com/optimization/cp/cp_example#objectiveIt’s cool
how?
there are 4 sets of constraints that we need to enforce:
There is some max UoC that can be allocated to a term,
A course is only offered in some terms,
The course has some prerequisites that have to be met,
Some courses must be taken consecutively.
All of these have have to be expressed in a way CP-SAT understands.
These all use a combination of the core concepts I will introduce. I will then explain how I compose them together for each one.
Core Concepts Used
variables
https://developers.google.com/optimization/cp/cp_solver
It is probably best to check out the actual documentation here for the best guidance, but in our model, our main variables are created right at the beginning, and are named after the courses they represent. The number they are assigned is the term they are allocated to. The terms are numbered from 0 sequentially, where 0 is the first term in our model, and each term is followed. There is also a cap in the number of terms that can be set, which is the parameter end
. there is also UoC max, which is a list of ints which define the maximum number of uoc that can be done every term.
Remember that in all cases, this includes summer term.
channeled constraint
https://developers.google.com/optimization/cp/channeling
This constraint is a concept I exploit heavily in the codebase. You can also call this a “Boolean condition gadget”. It sorta looks like this:
b = model.NewBoolVar('hi')
model.Add(v == index).OnlyEnforceIf(b)
model.Add(v != index).OnlyEnforceIf(b.Not())
this is a little wierd, because i am using .OnlyEnforceIf()
in a way that isn’t really expressing what I want. The point for this though is not to actually enforce that my variable is already equal to something. Instead, I will only enforce that my variable is equal to something if the boolean is satisfied. On the other hand, I will enforce the negation of this if the condition is not satisfied. What I actually wanted to do here was to enforce the contra-positive of this IFF relation! If my boolean is true, then it implies that my variable is equal to an index, and if it is false, it means that it is not.
Formally I have defined:
P => b
~P => ~b
The contrapositive of line 2 is
b => P
So, we have that
P <=> b
Which is what I wanted to do. Just set b if P is true, and if b is false, P is guaranteed to be false.
So, since my model has to decide what b
is, it is forced to set it to the correct value when the solution it comes up with it decides what the variable will be.
TLDR: this Isn't a constraint, this is a way to force my model to give me a boolean variable which is bound to a certain condition. I can then use this boolean to actually enforce something, like for example to enforce that one of the booleans I made must be true (like in my OR CompositeCondtion
method).
reservoir constraint
A commonly used constraint in our solver is the “reservoir constraint with active.” This takes in the following args:
a list of CSP variables of size n
a list of numbers of size n
a list of CSP boolean variables of size n
a minimal level of the reservoir
a maximal level of the reservoir
The 3 lists are heavily related to each other, and it is better to imagine them as 1 unit zipped together ie zip(variables, numbers, booleans)
.
The above list expresses what happens to the reservoir. If the boolean is 1, then it will fill the reservoir by size number. Else, it wont fill the reservoir. So, I have a common pattern in my code which exploits this:
I will channel the booleans to a certain constraint (the concept above).
This means that the booleans will only be 1 if the constraint is met. Then, I will set the numbers to be the amount to fill the reservoir by. Now, this means that only some number of my variables can fit in a certain constraint. So i can say for example, only 3 courses can get the same term allocation, because otherwise my reservoir is breached.
I actually think this constraint is more customisable than I am making it out to be – but for our purposes, this description is powerful enough
.OnlyEnforceIf() and how it relates to our AST
One of the most worrying challenges was how we can reuse our AST for this auto-planner. The worst bit was that model.Add() directly incorporates your constraint into the model, mutating it in the process. This means that if we want to mess with constraints after the fact (like we do in CompositeCondtion
) it would get messy.
Luckily though, we can use this function signature combined with .OnlyEnforceIf
to combat this:
def condition_to_model(
self, model: cp_model.CpModel,
user: User,
courses: list[Tuple[cp_model.IntVar, Course]],
course_variable: cp_model.IntVar
) -> list[cp_model.Constraint]:
The most important part of this signature is the return type list[cp_model.Constraint]
. This should return every constraint generated by the method. This means that after the fact, we can manipulate our constraints with .OnlyEnforceIf
arbitrarily. We can disable them, or enforce them conditionally using our channeled constraints from before.
The best demonstration of this in action is in CompositeCondition
, where I will attach channeled variables into my returned constraints from the conditions lower down in the tree, then assert that one of the channeled variables must be true.
This thus correctly implements our Or condition.
hiccup - condition_negation
we also need to make condition_negation
as a method to support the above. You notice that with channeling, we actually need to define what the negation of a constraint or set of constraints is. Only when the condition is actually the negation of the other will there be correct channeling. Now, in our OR section of CompositeCondition
, we are trying to channel arbitrary constraints. We cant easily do this unfortunately – OR tools doesn't provide a way to give the negation of a constraint. So, we instead need to make condition_negation
to define what it means to negate the constraint we have.
For more guidance, check out the code. I have heavily commented it to help others out.