MiniZinc with Strings

TL;DR

This paper introduces native string support in MiniZinc, enabling modeling and solving of string constraints in combinatorial problems using existing solvers, thus broadening the applicability of constraint programming.

Contribution

It adds string variables and constraints as built-in features to MiniZinc and provides an interpreter to convert models into FlatZinc with only integer variables.

Findings

Enables modeling of string constraints in MiniZinc.

Allows existing solvers to handle string problems.

Facilitates applications in software analysis and security.

Abstract

Strings are extensively used in modern programming languages and constraints over strings of unknown length occur in a wide range of real-world applications such as software analysis and verification, testing, model checking, and web security. Nevertheless, practically no CP solver natively supports string constraints. We introduce string variables and a suitable set of string constraints as builtin features of the MiniZinc modelling language. Furthermore, we define an interpreter for converting a MiniZinc model with strings into a FlatZinc instance relying on only integer variables. This provides a user-friendly interface for modelling combinatorial problems with strings, and enables both string and non-string solvers to actually solve such problems.