Discrete optimisation problems make decisions from a finite set of choices. They encompass many important problem classes such as scheduling, rostering and resource allocation. MiniZinc is a leading modelling language for discrete optimisation. It allows the expression of discrete optimisation problems succinctly using high level global constraints, and automatically translates them to run on constraint programming (CP), mixed integer programming (MIP), Boolean satisfiability (SAT), SAT modulo theories (SMT), and local search solvers. Integers are a key type in MiniZinc since they are used represent all the finite decisions made during solving. Indeed, handling integer constraints efficiently is one of the key challenges in discrete optimisation solving. Each solving technology tackles this differently: CP by building specific integer propagation techniques for each different global constraint, MIP by relaxing integrality and using branching to enforce it, SAT by encoding integers using Boolean variables, SMT using a mix of all three methods above, and local search by converting constraints to penalty functions and using local moves. All the approaches require search, and for difficult problems this search can be enormous, requiring millions of decisions or moves to be explored. But in the latest development version of MiniZinc, we recommend never using integers in models. Why?

Finding errors in discrete optimisation models can be very challenging. In the worst case when a solver simply returns no answer, we don’t know if this is because the problem we want to ask is too hard (for this solver) or the problem we actually asked (because of errors in the model) is too hard. Looking through solver traces of millions of events to find a problem is very hard work, and indeed there may be no error. Any errors we can detect before sending a model to the solver are invaluable. Hence, strong type systems are crucial for discrete optimisation models, since errors spotted by the type system may save us a huge amount of debugging work. How can we model discrete optimisation problems without integers? Many discrete optimisation problems reason about sets of named objects. Since version 2.1 MiniZinc has supported (ordered) enumerated types (enums), which allow decisions over a such sets. This immediately improves type safety. But we also need to be able to reason about two or more sets of objects jointly. Enumerated type extension allows us to build a supertype that includes both types of objects. Unordered enumerated types allow us to further strengthen models, if it makes no sense to rank two different objects. With these tools we never confuse reasoning about different sets of objects. But what about the many remaining integers in models, that don’t represent objects? For these we rely on unit types to differentiate between different integers appearing in the model. All integer decisions in models are either about a set of objects or some measurable resource type. Using unit types we can add more type safety for our models by avoiding confusion of different types of decisions. Unit types in MiniZinc are somewhat unusual, since often models deal with multiple granularity of the same resource, e.g. scheduling to the minute, but doing resource allocation on the half day; or use an unspecified granularity, e.g. the same job-shop scheduling model could use task durations given in minutes or days. Unit types in MiniZinc also differentiate between absolute unit types, e.g. the time when an event occurred, and delta unit types, e.g. the time difference between two events. Errors arising from mixing absolute and delta can be very hard to debug, so we extend the type system to track this for us. In a high-level modelling language like MiniZinc, the compiler ensures that models are type-safe. The underlying solvers can of course remain completely unaware of complex concepts like enums or unit types, since the MiniZinc compiler translates them into simple integers. Overall, armed with a type system that supports enumerated types, type extension, unit types, and delta unit types, we find that no discrete optimisation model needs to include raw, unsafe integer variables.