ILP-based solvers that intake a line planning, an infrastructure and a set of constraints and then output a cyclic train timetable have been researched extensively in the world of trains. However, these types of solvers are not able to automatically output a timetable when the problem gets overconstrained and no feasible solution exists.

It is possible to transform the timetabling problem into an equivalent Satisfiability problem that can be solved by SAT-solvers. In a recent thesis performed at NS, this has proven fruitful in cases where pre-chosen route choices prevent the model from finding a feasible solution.
This is because the increased solving speed makes for a quicker discovery that no feasible solution is possible within the preset routes. It is then possible to iteratively call the solver, adding more route options in each iteration. By doing so, feasible timetables can be sought out within a reasonable time frame. Nonetheless, complications due to overconstraining still occur within these newer models, in particular when it comes to constraints that enforce train
series to depart on set intervals, frequency constraints.

This thesis focuses on overcoming the problem of overconstraining due to frequency constraints and on consistently producing a timetable by using a maxSAT solver that can distinguish hard and soft constraints and assign them weights accordingly. Its aim is to minimize the total weight of violated soft constraints while maintaining all hard constraints, and this objective value can be compared to the total weight of violated clauses in solutions found by previous models. The resulting model does not always reach a better objective value after an hour of optimizing than the model it tries to improve. Nevertheless it is able to handle a set of conflicting constraints and always delivers a timetable that is as least as good as the
one produced by the previous model. Additionally, it is capable of taking into account user preference for specific constraints through the weights.