MiniZinc

Last updated
MiniZinc
Paradigm Constraint programming / Logic Programming
Developer Monash University
First appearedMay 2, 2009;15 years ago (2009-05-02)
Stable release
2.8.5 / June 3, 2024;3 months ago (2024-06-03)
Implementation language C++
OS Linux, MacOS, and Windows
License MPLv2
Filename extensions .mzn, .dzn, .fzn
Website www.minizinc.org
Influenced by
Zinc

MiniZinc [1] is a constraint modelling language (or algebraic modeling language) to describe and solve high-complexity problems using a variety of well-known solving paradigms for combinatorial problems including constraint programming, integer programming, lazy clause generation, SAT, and SMT.

Contents

Following the constraint programming paradigm, in MiniZinc a problem is specified in terms of known values (parameters), unknown values (decision variables), and the relationship (constraints) between these values. MiniZinc promotes the use of global constraints to model well-known structures in problems. These global constraints improve the clarity of the model and allow solvers to use the most effective method to exploit the structure. A MiniZinc problem instance is translated (or flattened) to a level at which it only supports constraints that are supported by the target solver and then given to the solver using its preferred format. Currently MiniZinc can communicate with solver using its own format FlatZinc or .nl files.

A big advantage of MiniZinc is the possibility to use different solvers, and even different solvers, from the same MiniZinc instance. MiniZinc supports many solvers, both open source and commercial software, including CBC, [2] Choco, [3] Chuffed, Gurobi, IPOPT, and OR-Tools.

MiniZinc is interoperable with other languages such as R. [4]

Language

The following MiniZinc model can be used to solve the famous n-queens puzzle:

include "all_different.mzn"; % Include all_different globalint: n = 8; % The number of queens. (parameter)array [1..n] of var 1..n: q; % The height of the queens on the board. (decision variable)% No queen can be in a position where it can capture another queen. (constraints)constraint all_different(q); constraint all_different(i in 1..n)(q[i] + i); constraint all_different(i in 1..n)(q[i] - i); 

Related Research Articles

In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula. In other words, it asks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. If this is the case, the formula is called satisfiable. On the other hand, if no such assignment exists, the function expressed by the formula is FALSE for all possible variable assignments and the formula is unsatisfiable. For example, the formula "a AND NOT b" is satisfiable because one can find the values a = TRUE and b = FALSE, which make (a AND NOT b) = TRUE. In contrast, "a AND NOT a" is unsatisfiable.

A mathematical model is an abstract description of a concrete system using mathematical concepts and language. The process of developing a mathematical model is termed mathematical modeling. Mathematical models are used in applied mathematics and in the natural sciences and engineering disciplines, as well as in non-physical systems such as the social sciences. It can also be taught as a subject in its own right.

<span class="mw-page-title-main">Mathematical optimization</span> Study of mathematical algorithms for optimization problems

Mathematical optimization or mathematical programming is the selection of a best element, with regard to some criteria, from some set of available alternatives. It is generally divided into two subfields: discrete optimization and continuous optimization. Optimization problems arise in all quantitative disciplines from computer science and engineering to operations research and economics, and the development of solution methods has been of interest in mathematics for centuries.

A programming paradigm is a relatively high-level way to conceptualize and structure the implementation of a computer program. A programming language can be classified as supporting one or more paradigms.

Constraint programming (CP) is a paradigm for solving combinatorial problems that draws on a wide range of techniques from artificial intelligence, computer science, and operations research. In constraint programming, users declaratively state the constraints on the feasible solutions for a set of decision variables. Constraints differ from the common primitives of imperative programming languages in that they do not specify a step or sequence of steps to execute, but rather the properties of a solution to be found. In addition to constraints, users also need to specify a method to solve these constraints. This typically draws upon standard methods like chronological backtracking and constraint propagation, but may use customized code like a problem-specific branching heuristic.

Constraint satisfaction problems (CSPs) are mathematical questions defined as a set of objects whose state must satisfy a number of constraints or limitations. CSPs represent the entities in a problem as a homogeneous collection of finite constraints over variables, which is solved by constraint satisfaction methods. CSPs are the subject of research in both artificial intelligence and operations research, since the regularity in their formulation provides a common basis to analyze and solve problems of many seemingly unrelated families. CSPs often exhibit high complexity, requiring a combination of heuristics and combinatorial search methods to be solved in a reasonable time. Constraint programming (CP) is the field of research that specifically focuses on tackling these kinds of problems. Additionally, the Boolean satisfiability problem (SAT), satisfiability modulo theories (SMT), mixed integer programming (MIP) and answer set programming (ASP) are all fields of research focusing on the resolution of particular forms of the constraint satisfaction problem.

Backtracking is a class of algorithms for finding solutions to some computational problems, notably constraint satisfaction problems, that incrementally builds candidates to the solutions, and abandons a candidate ("backtracks") as soon as it determines that the candidate cannot possibly be completed to a valid solution.

In the field of mathematical optimization, stochastic programming is a framework for modeling optimization problems that involve uncertainty. A stochastic program is an optimization problem in which some or all problem parameters are uncertain, but follow known probability distributions. This framework contrasts with deterministic optimization, in which all problem parameters are assumed to be known exactly. The goal of stochastic programming is to find a decision which both optimizes some criteria chosen by the decision maker, and appropriately accounts for the uncertainty of the problem parameters. Because many real-world decisions involve uncertainty, stochastic programming has found applications in a broad range of areas ranging from finance to transportation to energy optimization.

In mathematics, nonlinear programming (NLP) is the process of solving an optimization problem where some of the constraints are not linear equalities or the objective function is not a linear function. An optimization problem is one of calculation of the extrema of an objective function over a set of unknown real variables and conditional to the satisfaction of a system of equalities and inequalities, collectively termed constraints. It is the sub-field of mathematical optimization that deals with problems that are not linear.

In artificial intelligence and operations research, constraint satisfaction is the process of finding a solution through a set of constraints that impose conditions that the variables must satisfy. A solution is therefore an assignment of values to the variables that satisfies all constraints—that is, a point in the feasible region.

Answer set programming (ASP) is a form of declarative programming oriented towards difficult search problems. It is based on the stable model semantics of logic programming. In ASP, search problems are reduced to computing stable models, and answer set solvers—programs for generating stable models—are used to perform search. The computational process employed in the design of many answer set solvers is an enhancement of the DPLL algorithm and, in principle, it always terminates.

ECLiPSe is a software system for the development and deployment of constraint logic programming applications, e.g., in the areas of optimization, planning, scheduling, resource allocation, timetabling, transport, etc. It is also suited for teaching most aspects of combinatorial problem solving, e.g., problem modeling, constraint programming, mathematical programming, and search techniques. It contains constraint solver libraries, a high-level modeling and control language, interfaces to third-party solvers, an integrated development environment and interfaces for embedding into host environments.

Constraint logic programming is a form of constraint programming, in which logic programming is extended to include concepts from constraint satisfaction. A constraint logic program is a logic program that contains constraints in the body of clauses. An example of a clause including a constraint is A(X,Y):-X+Y>0,B(X),C(Y). In this clause, X+Y>0 is a constraint; A(X,Y), B(X), and C(Y) are literals as in regular logic programming. This clause states one condition under which the statement A(X,Y) holds: X+Y is greater than zero and both B(X) and C(Y) are true.

Distributed constraint optimization is the distributed analogue to constraint optimization. A DCOP is a problem in which a group of agents must distributedly choose values for a set of variables such that the cost of a set of constraints over the variables is minimized.

In mathematics, a constraint is a condition of an optimization problem that the solution must satisfy. There are several types of constraints—primarily equality constraints, inequality constraints, and integer constraints. The set of candidate solutions that satisfy all constraints is called the feasible set.

Algebraic modeling languages (AML) are high-level computer programming languages for describing and solving high complexity problems for large scale mathematical computation. One particular advantage of some algebraic modeling languages like AIMMS, AMPL, GAMS, Gekko, MathProg, Mosel, and OPL is the similarity of their syntax to the mathematical notation of optimization problems. This allows for a very concise and readable definition of problems in the domain of optimization, which is supported by certain language elements like sets, indices, algebraic expressions, powerful sparse index and data handling variables, constraints with arbitrary names. The algebraic formulation of a model does not contain any hints how to process it.

In computer science and formal methods, a SAT solver is a computer program which aims to solve the Boolean satisfiability problem. On input a formula over Boolean variables, such as "(x or y) and (x or not y)", a SAT solver outputs whether the formula is satisfiable, meaning that there are possible values of x and y which make the formula true, or unsatisfiable, meaning that there are no such values of x and y. In this case, the formula is satisfiable when x is true, so the solver should return "satisfiable". Since the introduction of algorithms for SAT in the 1960s, modern SAT solvers have grown into complex software artifacts involving a large number of heuristics and program optimizations to work efficiently.

PROSE was the mathematical 4GL virtual machine that established the holistic modeling paradigm known as Synthetic Calculus. A successor to the SLANG/CUE simulation and optimization language developed at TRW Systems, it was introduced in 1974 on Control Data supercomputers. It was the first commercial language to employ automatic differentiation (AD), which was optimized to loop in the instruction-stack of the CDC 6600 CPU.

<span class="mw-page-title-main">OR-Tools</span> Open source software suite by Google

Google OR-Tools is a free and open-source software suite developed by Google for solving linear programming (LP), mixed integer programming (MIP), constraint programming (CP), vehicle routing (VRP), and related optimization problems.

References

  1. Nethercote, Nicholas; Stuckey, Peter J.; Becket, Ralph; Brand, Sebastian; Duck, Gregory J.; Tack, Guido (2007). Bessière, Christian (ed.). "MiniZinc: Towards a Standard CP Modelling Language". Principles and Practice of Constraint Programming – CP 2007. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer: 529–543. doi:10.1007/978-3-540-74970-7_38. ISBN   978-3-540-74970-7.
  2. "COIN-OR Branch-and-Cut MIP Solver". projects.coin-or.org. Retrieved 2020-09-14.
  3. "Choco-solver". Choco-solver. Retrieved 2020-09-14.
  4. https://cran.r-project.org/web/packages/rminizinc/vignettes/R_MiniZinc.html