Solverl

Erlang/Elixir interface to MiniZinc.

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.

Installation
Usage
Examples
Erlang interface
Roadmap
Credits

Installation

You will need to install MiniZinc. Please refer to https://www.minizinc.org/software.html for details.

Note:

The code was only tested on macOS Catalina and Ubuntu 18.04 with MiniZinc v2.4.3.

Note:

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

Usage

API

#################
# 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 to model;
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 specification

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 specification

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 par names/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}]
```

Support for MiniZinc data types

Arrays

MiniZinc array type 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 enum names specified in your model and/or data.

Example: assume your model has a definition of enum
```
enum test_enum = {blue, red, white};
```
You could then generate the data for the array that uses enum as 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"
```

Sets

MiniZinc set type corresponds to MapSet.

Example:

MinizincData.to_dzn(%{set1: MapSet.new([2, 1, 6])})

Output:

"set1 = {1, 2, 6};\n"

Enums

MiniZinc enum type 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 enum variable):

  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"

Monitoring and controlling the solving process

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 options

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 if minizinc executable cannot be located by your system).
checker: Model specification for MiniZinc checker model.
extra_flags: A string of command line flags supp

Solverl

Install / Use

README

Solverl

Installation

Note:

Note:

Usage

API

Model specification

Data specification

Support for MiniZinc data types

Arrays

Sets

Enums

Monitoring and controlling the solving process

Solver options