Erlang/Elixir interface to MiniZinc.
Inspired by MiniZinc Python.
View docs here.
Disclaimer: This project is in its very early stages, and has only been used in a single production application. Use at your own risk.
You will need to install MiniZinc. Please refer to https://www.minizinc.org/software.html for details.
The code was only tested on macOS Catalina and Ubuntu 18.04 with MiniZinc v2.4.3.
minizinc executable is expected to be in its default location, or in a folder in the $PATH env variable.
Otherwise, you can use the minizinc_executable option (see Solver Options).
The package can be installed by adding solverl to your list of dependencies in mix.exs:
def deps do
[
{:solverl, ">= 1.0.0"}
]
end#################
# Solving
#################
#
# Asynchronous solving.
# Creates a solver process and processes solutions as they come in.
{:ok, solver_pid} = MinizincSolver.solve(model, data, solver_opts, server_opts)
# Synchronous solving.
# Starts the solver and gets the results (solutions and/or solver stats) once the solver finishes.
solver_results = MinizincSolver.solve_sync(model, data, solver_opts, server_opts), where
model- specification of MiniZinc model;data (optional)- specification of data passed tomodel;solver_opts (optional)- solver options.server_opts (optional)- GenServer options for solver process
############################
# Monitoring and controlling
# the solving process at runtime
############################
#
## Get runtime solver status
MinizincSolver.solver_status(pid_or_name)## Update solution handler at runtime
MinizincSolver.update_solution_handler(pid_or_name, solution_handler) ## Stop the solver gracefully (it'll produce a summary before shutting down)
MinizincSolver.stop_solver(pid_or_name), where pid_or_name is either a PID or a registered (for instance, through GenServer :name option) name of the solver process.
Model could be either:
-
a string, in which case it represents a path for a file containing MiniZinc model.
Example: "mzn/sudoku.mzn"
-
or, a tuple {:model_text,
model_text}.Example (model as a multiline string):
""" array [1..5] of var 1..n: x; include "alldifferent.mzn"; constraint alldifferent(x); """
-
or a (mixed) list of the above. The code will build a model by concatenating bodies of model files and model texts, each with a trailing line break.
Example:
["mzn/test1.mzn", {:model_text, "constraint y[1] + y[2] <= 0;"}]
Data could be either:
-
a string, in which case it represents a path for a MiniZinc data file.
Example: "mzn/sudoku.dzn"
-
a map, in which case map keys/value represent model
parnames/values.Example:
%{n: 5, f: 3.44}
-
or a (mixed) list of the above. The code will build a data file by mapping elements of the list to bodies of data files and/or data maps, serialized as described in Support for MiniZinc data types, then concatenating the elements of the list, each with a trailing line break.
Example:
["mzn/test_data1.dzn", "mzn/test_data2.dzn", %{x: 2, y: -3, z: true}]
-
MiniZinc
arraytype corresponds to (nested) List. The code determines dimensions of the array based on its nested structure. Each level of the nested list has to contain lists of the same length, or the exception{:irregular_array, array}will be thrown. 6 levels of nesting are currently supported, in line with MiniZinc current limit.By default, the indices of the dimensions are 1-based.
Example:
arr2d = [ [0, 1, 0, 1, 0], [0, 1, 0, 1, 0], [0, 1, 0, 1, 0], [0, 1, 0, 1, 0], [0, 1, 0, 1, 0] ] MinizincData.to_dzn(%{a: arr2d})
Output:
"a = array2d(1..5,1..5,[0, 1, 0, 1, 0, 0, 1, 0, 1, 0, 0, 1, 0, 1, 0, 0, 1, 0, 1, 0, 0, 1, 0, 1, 0]);\n"You can explicitly specify bases for each dimension:
# Let 1st dimension be 0-based, 2nd dimension be 1-based MinizincData.to_dzn(%{a: {[0, 1], arr2d}})
Output:
"a = array2d(0..4,1..5,[0, 1, 0, 1, 0, 0, 1, 0, 1, 0, 0, 1, 0, 1, 0, 0, 1, 0, 1, 0, 0, 1, 0, 1, 0]);\n"There is an option to specify array's index sets through
enumnames specified in your model and/or data.Example: assume your model has a definition of
enumenum test_enum = {blue, red, white};You could then generate the data for the array that uses
enumas an index set:enum_arr2d = {["test_enum", "test_enum"], [[1, 2, 3], [4, 5, 6]]} MinizincData.to_dzn(%{enum_arr2d: enum_arr2d})
Output:
"enum_arr2d = array2d(test_enum, test_enum,[1, 2, 3, 4, 5, 6]);\n" -
MiniZinc
settype corresponds to MapSet.Example:
MinizincData.to_dzn(%{set1: MapSet.new([2, 1, 6])})
Output:
"set1 = {1, 2, 6};\n" -
MiniZinc
enumtype corresponds to Tuple. Tuple elements have to be either of strings, charlists or atoms.Example 1 (using strings, atoms and charlists for enum entries):
MinizincData.to_dzn(%{colors: {"blue", :BLACK, 'GREEN'}})
Output:
"colors = {blue, BLACK, GREEN};\n"Example 2 (solving for
enumvariable):enum_model = """ enum COLOR; var COLOR: color; constraint color = max(COLOR); """ {:ok, results} = MinizincSolver.solve_sync({:model_text, enum_model}, %{'COLOR': {"White", "Black", "Red", "BLue", "Green"}}) MinizincResults.get_last_solution(results)[:data]["color"]
Output:
"Green"
The solving process communicates to the outside through API calls. First argument of these calls will be either PID of the process (returned by MinizincSolver.solve/4), or the name of the GenServer process.
## Start long-running solving process named Graph1000...
{:ok, pid} = MinizincSolver.solve("mzn/graph_coloring.mzn", "mzn/gc_1000.dzn",
[time_limit: 60*60*1000],
name: Graph1000){:ok, #PID<0.995.0>}
## ... and check for its status
MinizincSolver.solver_status(Graph1000){:ok,
%{
running_time: 2064190,
solution_count: 0,
solving_time: nil,
stage: :compiling,
time_since_last_solution: nil
}}
## It's compiling now.
## Give it 5 mins or so and check again...
MinizincSolver.solver_status(Graph1000){:ok,
%{
running_time: 327998354,
solution_count: 108,
solving_time: 323612671,
stage: :solving,
time_since_last_solution: 1322186
}}## Replace current solution handler with the one that logs intermittent results...
MinizincSolver.update_solution_handler(Graph1000, GraphColoring.Handler)
### and watch it now logging 'Found XXX-coloring' messages...## Stop it now
MinizincSolver.stop_solver(Graph1000)
15:54:51.092 [debug] Request to stop the solver...
:ok
15:54:51.092 [debug] ** TERMINATE: :normal
-
solver: Solver id supported by your MiniZinc configuration.Default:
"gecode". -
time_limit: Time in msecs given for MiniZinc executable to run.Default:
300000(5 mins). Use[time_limit: nil]for unlimited time. -
solution_timeout: Time in msecs to wait for a next solution. -
fzn_timeout: Time in msecs to wait for the compilation (flattening) to finish. -
minizinc_executable: Full path to MiniZinc executable (you'd need it ifminizincexecutable cannot be located by your system). -
checker: Model specification for MiniZinc checker model. -
extra_flags: A string of command line flags supported by the solver. -
solution_handler: Module or function that controls processing of solutions and/or metadata.Default:
MinizincHandler.Default. Check out Solution handlers for more details. -
log_output: A function with arity 1. If specified, will be called and passed the output line as the MiniZinc process writes it tostdoutand/orstderr
Example:
## Solve "mzn/nqueens.mzn" for n = 4, using Gecode solver,
## time limit of 1 sec, NQueens.Handler as a solution handler,
## checker model at "mzn/nqueens.mzc.mzn".
## Extra flags: -O1 --verbose-compilation
MinizincSolver.solve_sync("mzn/nqueens.mzn", %{n: 4},
[solver: "gecode",
time_limit: 1000,
solution_handler: NQueens.Handler,
checker: "mzn/nqueens.mzc.mzn",
extra_flags: "-O1 --verbose-compilation"])Solution handler is a pluggable code created by the user in order to customize processing of solutions and metadata produced by MinizincSolver.solve/3 and MinizincSolver.solve_sync/3.
Solution handler is specified by solution_handler option.
Solution handler is either one of:
- a function
- or, a module that implements MinizincHandler behaviour.
Solution handler code acts as a callback for the solver events emitted by MinizincPort, which is a managing process for MiniZinc executable (see Under the hood for more details).
In case the solution handler is a function, its signature has to have 2 arguments, 1st one is an atom denoting the solver event type (i.e., :solution, :summary, :minizinc_error), 2nd being the event-specific data of that event.
In case the solution handler is a module that implements MinizincHandler behaviour,
its functions handle_solution/1, handle_summary/1, handle_minizinc_error/1 take an event-specific data.
Solver event is a tuple {event_type, event_data}.
Currently, there are following types of solver events:
:solution- the new solution detected;:summary- the summary was generated (usually because the solver had finished);:minizinc_error- the MiniZinc runtime error was detected.
- For
:solutionevent, data is a map with following keys:
[
:data, # Map of values keyed with their variable names
:timestamp, # Timestamp of the moment solution was parsed
:index, # Sequential number of the solution
:stats # Map of solution statistics values keyed with the field names
]- For
:summaryevent, data is a map with following keys:
[
:status, # Solver status (one of :satisfied, :unsatisfiable etc)
:fzn_stats, # Map of FlatZinc statistics values keyed with the field names
:solver_stats, # Map of solver statistics values keyed with the field names
:solution_count, # Total number of solutions found
:last_solution, # Data for last :solution event (see above)
:minizinc_output, # MiniZinc errors and warnings
:time_elapsed # Time elapsed, verbatim as reported by MiniZinc
]- For
:minizinc_errorevent, data is a map with following keys:
[
:error # MiniZinc output generated by runtime error
]Solution handlers can modify or ignore data passed by solver events, or interrupt the solver process early, by constructing their returns in desired form.
The return of the solution handler callback could be one of:
-
:breakSolution handler stops receiving solver events and asks solver to stop execution.
-
{:break, data}Same as above, but in case of synchronous solving,
datawill be added to solver results. -
:skipThe event will be ignored, i.e. in case of synchronous solving, the results will not be changed.
-
data :: any()In case of synchronous solving, data will be added to solver results.
Note: this is applicable only to a synchronous solving.
Solver results is a map with the following keys:
:solutions- list of data elements, accumulated by handling of:solutionevents:summary- data, produced by handling of:summaryevent:minizinc_error- data, produced by handling of:minizinc_errorevent
Please refer to Event-specific data for description of data for solver events.
Solution handler is a pluggable code that is typically created by a user. MinizincSolver catches exceptions from solution handlers
to make sure that the solver process is gracefully shut down. Moreover, in case of synchronous solving,
MinizincSolver preserves the solver results accumulated before the exception, and returns them to the calling process.
The exception value will be added to solver results under :handler_exception key.
## For any given solution handler, limit the number of solutions to `k`.
## This is done by 'wrapping' a handler into built-in MinizincSearch.find_k_handler/2.
## The resulting handler can then be used by the solving API.
MinizincSearch.find_k_handler(k, solution_handler)## Run LNS on a problem instance for a number of iterations, using a
## user-defined destruction function.
## Instance is a container that 'packs' arguments needed for calling the solving API.
## Destruction function applies to a current model and the solutions found in a previous
## iteration and modifies the model by refining its constraints for the objective
## and decision varables according to user-defined LNS strategy.
MinizincSearch.lns(instance, iterations, destruction_fun) ## Run BAB on a problem instance, using user-defined branch function.
## The model will be refined with the new objective constraint for every new iteration,
## until the objective couldn't be improved.
## (which will result in UNSATISFIABLE outcome).
## Branch function applies to a model and it's first solution found in a previous
## iteration and modifies the model for the next iteration by refining its objective constraint.
MinizincSearch.bab(instance, branch_fun)- Reindeer Ordering
- N-Queens
- Sudoku
- Graph Coloring
- Large Neighbourhood Search
- Finding the first k solutions
- Branch-and-Bound example
- Solver Race
- More examples in unit tests
The problem: Reindeer Ordering
Solve it:
ReindeerOrdering.solve()Output:
"Prancer, Cupid, Rudolph, Dasher, Blitzen, Vixen, Comet, Donder, Dancer"
The following code solves N-queens puzzle for N = 4:
NQueens.solve(4, [solution_handler: &NQueens.solution_handler/2])Output:
17:16:53.073 [warn] Command: /Applications/MiniZincIDE.app/Contents/Resources/minizinc --allow-multiple-assignments --output-mode json --output-time --output-objective --output-output-item -s -a --solver org.gecode.gecode --time-limit 300000 /var/folders/rn/_39sx1c12ws1x5k66n_cjjh00000gn/T/tmp.vFlJER37.mzn /var/folders/rn/_39sx1c12ws1x5k66n_cjjh00000gn/T/tmp.rxTZq96j.dzn
{:ok, #PID<0.766.0>}
iex(75)>
17:16:53.174 [info]
. . ♕ .
♕ . . .
. . . ♕
. ♕ . .
-----------------------
17:16:53.174 [info]
. ♕ . .
. . . ♕
♕ . . .
. . ♕ .
-----------------------
17:16:53.179 [info] Solution status: all_solutions
17:16:53.179 [info] Solver stats:
%{failures: 4, initTime: 0.007719, nSolutions: 2, nodes: 11, peakDepth: 2, propagations: 163, propagators: 11, restarts: 0, solutions: 2, solveTime: 0.002778, variables: 12}
17:16:53.179 [debug] ** TERMINATE: :normal
Sudoku.solve("85...24..72......9..4.........1.7..23.5...9...4...........8..7..17..........36.4.")The output:
17:19:28.109 [info] Sudoku puzzle:
17:19:28.109 [info]
+-------+-------+-------+
| 8 5 . | . . 2 | 4 . . |
| 7 2 . | . . . | . . 9 |
| . . 4 | . . . | . . . |
+-------+-------+-------+
| . . . | 1 . 7 | . . 2 |
| 3 . 5 | . . . | 9 . . |
| . 4 . | . . . | . . . |
+-------+-------+-------+
| . . . | . 8 . | . 7 . |
| . 1 7 | . . . | . . . |
| . . . | . 3 6 | . 4 . |
+-------+-------+-------+
17:19:28.154 [warn] Command: /Applications/MiniZincIDE.app/Contents/Resources/minizinc --allow-multiple-assignments --output-mode json --output-time --output-objective --output-output-item -s -a --solver org.gecode.gecode --time-limit 300000 /var/folders/rn/_39sx1c12ws1x5k66n_cjjh00000gn/T/tmp.uSF45sHN.mzn /var/folders/rn/_39sx1c12ws1x5k66n_cjjh00000gn/T/tmp.KjyUqmEa.dzn
{:ok, #PID<0.776.0>}
iex(79)>
17:19:28.219 [info]
+-------+-------+-------+
| 8 5 9 | 6 1 2 | 4 3 7 |
| 7 2 3 | 8 5 4 | 1 6 9 |
| 1 6 4 | 3 7 9 | 5 2 8 |
+-------+-------+-------+
| 9 8 6 | 1 4 7 | 3 5 2 |
| 3 7 5 | 2 6 8 | 9 1 4 |
| 2 4 1 | 5 9 3 | 7 8 6 |
+-------+-------+-------+
| 4 3 2 | 9 8 1 | 6 7 5 |
| 6 1 7 | 4 2 5 | 8 9 3 |
| 5 9 8 | 7 3 6 | 2 4 1 |
+-------+-------+-------+
17:19:28.219 [info] Solutions found: 1
17:19:28.224 [info] Status: all_solutions
17:19:28.224 [info] Solver statistics:
%{failures: 11, initTime: 0.001401, nSolutions: 1, nodes: 23, peakDepth: 5, propagations: 685, propagators: 27, restarts: 0, solutions: 1, solveTime: 0.001104, variables: 147}
17:19:28.224 [debug] ** TERMINATE: :normal
The model's objective is to minimize the number of colors for proper Graph Vertex Coloring.
edges = [
[0, 1], [1, 2], [1, 3]
]
vertices = 4
## Color graph with time limit of 1 sec:
GraphColoring.do_coloring({vertices, edges}, [time_limit: 1*1000]) Output:
22:43:01.318 [info] Found coloring to 2 colors
22:43:01.328 [info] Best coloring found: 2 colors
22:43:01.328 [info] Optimal? Yes
22:43:01.328 [info] Color 1 -> vertices: 0, 2, 3
22:43:01.328 [info] Color 2 -> vertices: 1
It's a Graph Coloring again, now on a graph with 1000 vertices.
We will use MinizincSearch.lns/5 built-in to implement Randomized LNS.
The following call runs 3 iterations with destruction rate of 0.8, and iteration time limit of 1 minute:
LNS.GraphColoring.do_lns("mzn/gc_1000.dzn", 3, 0.8, time_limit: 60*1000) Output:
14:20:27.990 [info] Iteration 1: 480-coloring
14:21:31.168 [info] Iteration 2: 433-coloring
14:22:34.130 [info] Iteration 3: 380-coloring
14:22:34.131 [info] LNS final: 380-coloring
For the same graph with 1000 vertices, we will use MinizincSearch.lns/5 built-in to implement a flavour of Adaptive LNS.
The following call runs 5 iterations with initial destruction rate of 0.7, increment of 0.05 and iteration time limit of 1 minute:
LNS.GraphColoring.do_adaptive_lns("mzn/gc_1000.dzn", 5, 0.7, 0.05, time_limit: 60*1000) Output:
23:07:59.956 [info] Iteration 1: 486-coloring, rate: 0.7
23:09:02.905 [info] Iteration 2: 432-coloring, rate: 0.75
23:10:06.097 [info] Iteration 3: 387-coloring, rate: 0.8
23:11:09.239 [info] Iteration 4: 355-coloring, rate: 0.85
23:12:12.373 [info] Iteration 5: 321-coloring, rate: 0.9
23:12:12.374 [info] LNS final: 321-coloring
:ok
We use the Sudoku code from the example above, but now with the built-in handler that limits the number of solutions.
## The puzzle below has 5 solutions...
sudoku_puzzle = "8..6..9.5.............2.31...7318.6.24.....73...........279.1..5...8..36..3......"
## ...but we only want 3
Sudoku.solve(sudoku_puzzle,
solution_handler: MinizincSearch.find_k_handler(3, Sudoku.Handler))Partial output (last solution and a final line only):
18:36:13.716 [info]
+-------+-------+-------+
| 8 1 4 | 6 3 7 | 9 2 5 |
| 3 2 5 | 1 4 9 | 6 8 7 |
| 7 9 6 | 8 2 5 | 3 1 4 |
+-------+-------+-------+
| 9 5 7 | 3 1 8 | 4 6 2 |
| 2 4 1 | 9 5 6 | 8 7 3 |
| 6 3 8 | 2 7 4 | 5 9 1 |
+-------+-------+-------+
| 4 6 2 | 7 9 3 | 1 5 8 |
| 5 7 9 | 4 8 1 | 2 3 6 |
| 1 8 3 | 5 6 2 | 7 4 9 |
+-------+-------+-------+
18:36:13.716 [info] Solutions found: 3
This is an implementation of Golomb Ruler example from MiniSearch distribution.
GolombBAB.solve(time_limit: 3000) Output:
22:53:33.915 [info] Intermediate solution with objective 80
22:53:34.179 [info] Intermediate solution with objective 75
22:53:34.439 [info] Intermediate solution with objective 73
22:53:34.699 [info] Intermediate solution with objective 72
22:53:34.959 [info] Intermediate solution with objective 70
22:53:35.224 [info] Intermediate solution with objective 68
22:53:35.491 [info] Intermediate solution with objective 66
22:53:35.757 [info] Intermediate solution with objective 62
22:53:36.110 [info] Intermediate solution with objective 60
22:53:36.960 [info] Intermediate solution with objective 55
22:53:38.499 [info] golomb 55
[0, 1, 6, 10, 23, 26, 34, 41, 53, 55]
Note that the model's output (last 2 rows) is being used, to show that it is present in the solver results.
We will simultaneously run Gecode and Chuffed on the same model. The results will be collected by the parent process, which will do logging of intermediate results and the final standing.
SolverRace.run(["chuffed", "gecode"])Output:
12:58:00.212 [info] chuffed started as #PID<0.3264.0>...
12:58:00.356 [info] gecode started as #PID<0.3267.0>...
12:58:00.356 [info] chuffed: Compiled!
12:58:00.461 [info] gecode: Compiled!
12:58:00.470 [info] gecode: 80
12:58:00.471 [info] gecode: 75
12:58:00.472 [info] gecode: 73
12:58:00.475 [info] gecode: 72
12:58:00.483 [info] gecode: 70
12:58:00.486 [info] chuffed: 80
12:58:00.486 [info] gecode: 68
12:58:00.488 [info] chuffed: 75
12:58:00.492 [info] chuffed: 73
12:58:00.496 [info] gecode: 66
12:58:00.500 [info] chuffed: 72
12:58:00.503 [info] gecode: 62
12:58:00.513 [info] chuffed: 70
12:58:00.524 [info] chuffed: 68
12:58:00.546 [info] chuffed: 66
12:58:00.562 [info] chuffed: 62
12:58:00.600 [info] gecode: 60
12:58:00.764 [info] chuffed: 60
12:58:01.117 [info] gecode: 55
12:58:01.883 [info] chuffed: 55
12:58:02.223 [info] Solver gecode finished with objective 55, status: optimal
12:58:02.223 [info] Shutting down chuffed...
12:58:02.223 [info] Solver chuffed finished with objective 55, status: satisfied
12:58:02.223 [info] Race results: [{"gecode", 55}, {"chuffed", 55}]
minizinc module mirrors all exported functions of MinizincSolver module.
Once you manage to make solverl dependency part of your Erlang application build (for instance with rebar_mix),
you should be able to use its interface.
Example:
results = minizinc:solve_sync(<<"mzn/nqueens.mzn">>,
#{n=> 4}, [{solution_handler, fun 'Elixir.NQueens':solution_handler/2}]).Note: Please use binary strings as opposed to char strings whenever you need to pass a string to API.
The API functions will always use binary strings whenever the function return needs to use strings.
Both MinizincSolver.solve/4 and MinizincSolver.solve_sync/4 spawn a separate GenServer process, which in turn spawns the external MiniZinc process,
and then asynchronously receives chunks of MiniZinc output, parses them into solver events and fires appropriate callbacks as described here.
This makes the handling of MiniZinc output completely asynchronous, even though solve_sync/4 is a blocking call that will wait for it to terminate.
As a consequence, this allows to control the solving process from outside regardless of whether solve/4 or solve_sync/4 is being used, as long as the PID or registered name of the process is known.
- Match MiniZinc Python and MiniSearch functionality
- API for parallel and distributed solving
- Better error and exception handling
The project extensively uses ideas and code examples from MiniZinc Python and MiniSearch.