The MiniZinc-SAT Compiler

Combinatorial (optimization) problems occur in nature and society. Constraint modeling languages such as MiniZinc allow the user to declaratively specify such problems in terms of its decision variables and constraints. Subsequently, the MiniZinc model can be compiled into an equivalent (Boolean) SAT formula to be solved by a SAT solver. This thesis reports on the design, implementation and experimental evaluation of the new MiniZinc-SAT compiler, which supports single or even mixed usage of three distinct integer variable encoding methods