[Yadi]

Oh I saw this on reddit! This is an awesome way to understand what the SMT solvers are good at and what not to use them for. I'm a fan of EPL and Man UTD, I've given some thought few times to try figuring out if there would be a away to approach this sort of solution.

I wonder if this can be applied to other set of fixtures! For example in the FA cup, more accuracy with winning and lower rate of teams. Or the other leagues like La Liga.

[microarchitect]

I'm not sure if I understand what you mean by accuracy. This is not a probabilistic analysis. The solver considers the space of all possible outcomes for each match and returns satisfiable if there is some set of outcomes that satisfies the constraints. For example, it says that Stoke City can still qualify for the CL, but this requires that all of the current top 4 will need to pretty much lose every match while the teams below them win every match. This is obviously so unlikely to happen that you might as well disregard it it, but it is still a mathematical possibility and so the solver returns satisfiable.

As far as la liga is concerned, yes, you can definitely do a similar analysis. You will have to change the code that calculates the league positions, because in la liga if two teams are level on points then the first tie-breaker is head to head record, and then goal difference if the head to head is also equal. This should be a pretty straightforward change.