Finding diverse solution for MiniZinc instances (#87)

* Initial commit on diversity

* Fix the formatting and types

* Make MznAnalyse.find consistent with Driver.find

* Simplify the assignment of previous solutions

* Remove the requirement of numpy

* Remove unused argument MznAnalyse.run

* Refactor code to be in more logical places

* Additional refactoring of diverse_solutions function

* Change Instance.diverse_solutions to be async

* Add a more programmatic interface for the mzn-analyse tool

* Add solver argument for Instance.diverse_solutions

* Change solution assertions in Instance.diverse_solutions to early return

* Add initial diversity library file

* Diversity MZN: Added description of annotations. Removed unused annotations.

* Diversity MZN: more description to annotations

* Diversity: Added documentation entry for diversity functionality

* Move diversity.mzn file into the MiniZinc standard library

* Fix typing issues

---------

Co-authored-by: Jip J. Dekker <[email protected]>
Co-authored-by: Kevin Leo <[email protected]>

docs/advanced_usage.rst

@@ -159,6 +159,79 @@ better solution is found in the last 3 iterations, it will stop.
             else:
                 i += 1
 
+Getting Diverse Solutions
+-------------------------
+
+It is sometimes useful to find multiple solutions to a problem
+that exhibit some desired measure of diversity.  For example, in a
+satisfaction problem, we may wish to have solutions that differ in
+the assignments to certain variables but we might not care about some
+others.  Another important case is where we wish to find a diverse set
+of close-to-optimal solutions.
+
+The following example demonstrates a simple optimisation problem where
+we wish to find a set of 5 diverse, close to optimal solutions.
+First, to define the diversity metric, we annotate the solve item with
+the :func:`diverse_pairwise(x, "hamming_distance")` annotation to indicate that
+we wish to find solutions that have the most differences to each other.
+The `diversity.mzn` library also defines the "manhattan_distance"
+diversity metric which computes the sum of the absolution difference
+between solutions.
+Second, to define how many solutions, and how close to optimal we wish the
+solutions to be, we use the :func:`diversity_incremental(5, 1.0)` annotation.
+This indicates that we wish to find 5 diverse solutions, and we will
+accept solutions that differ from the optimal by 100% (Note that this is
+the ratio of the optimal solution, not an optimality gap).
+
+..  code-block:: minizinc
+
+    % AllDiffOpt.mzn
+    include "alldifferent.mzn";
+    include "diversity.mzn";
+
+    array[1..5] of var 1..5: x;
+    constraint alldifferent(x);
+
+    solve :: diverse_pairwise(x, "hamming_distance")
+          :: diversity_incremental(5, 1.0) % number of solutions, gap %
+          minimize x[1];
+
+The :func:`Instance.diverse_solutions` method will use these annotations
+to find the desired set of diverse solutions. If we are solving an
+optimisation problem and want to find "almost" optimal solutions we must
+first acquire the optimal solution.  This solution is then passed to
+the :func:`diverse_solutions()` method in the :func:`reference_solution` parameter.
+We loop until we see a duplicate solution.
+
+..  code-block:: python
+
+    import asyncio
+    import minizinc
+
+    async def main():
+        # Create a MiniZinc model
+        model = minizinc.Model("AllDiffOpt.mzn")
+
+        # Transform Model into a instance
+        gecode = minizinc.Solver.lookup("gecode")
+        inst = minizinc.Instance(gecode, model)
+
+        # Solve the instance
+        result = await inst.solve_async(all_solutions=False)
+        print(result.objective)
+
+        # Solve the instance to obtain diverse solutions
+        sols = []
+        async for divsol in inst.diverse_solutions(reference_solution=result):
+            if divsol["x"] not in sols:
+                sols.append(divsol["x"])
+            else:
+                print("New diverse solution already in the pool of diverse solutions. Terminating...")
+                break
+            print(divsol["x"])
+
+    asyncio.run(main())
+
 
 Concurrent Solving
 ------------------

src/minizinc/__init__.py

@@ -50,4 +50,5 @@
     "Result",
     "Solver",
     "Status",
+    "Diversity",
 ]

src/minizinc/analyse.py

@@ -0,0 +1,119 @@
+#  This Source Code Form is subject to the terms of the Mozilla Public
+#  License, v. 2.0. If a copy of the MPL was not distributed with this
+#  file, You can obtain one at http://mozilla.org/MPL/2.0/.
+import json
+import os
+import platform
+import shutil
+import subprocess
+from enum import Enum, auto
+from pathlib import Path
+from typing import Any, Dict, List, Optional, Union
+
+from .driver import MAC_LOCATIONS, WIN_LOCATIONS
+from .error import ConfigurationError, MiniZincError
+
+
+class InlineOption(Enum):
+    DISABLED = auto()
+    NON_LIBRARY = auto()
+    ALL = auto()
+
+
+class MznAnalyse:
+    """Python interface to the mzn-analyse executable
+
+    This tool is used to retrieve information about or transform a MiniZinc
+    instance. This is used, for example, to  diverse solutions to the given
+    MiniZinc instance using the given solver configuration.
+    """
+
+    _executable: Path
+
+    def __init__(self, executable: Path):
+        self._executable = executable
+        if not self._executable.exists():
+            raise ConfigurationError(
+                f"No MiniZinc data annotator executable was found at '{self._executable}'."
+            )
+
+    @classmethod
+    def find(
+        cls, path: Optional[List[str]] = None, name: str = "mzn-analyse"
+    ) -> Optional["MznAnalyse"]:
+        """Finds the mzn-analyse executable on default or specified path.
+
+        The find method will look for the mzn-analyse executable to create an
+        interface for MiniZinc Python. If no path is specified, then the paths
+        given by the environment variables appended by default locations will be
+        tried.
+
+        Args:
+            path: List of locations to search. name: Name of the executable.
+
+        Returns:
+            Optional[MznAnalyse]: Returns a MznAnalyse object when found or None.
+        """
+
+        if path is None:
+            path = os.environ.get("PATH", "").split(os.pathsep)
+            # Add default MiniZinc locations to the path
+            if platform.system() == "Darwin":
+                path.extend(MAC_LOCATIONS)
+            elif platform.system() == "Windows":
+                path.extend(WIN_LOCATIONS)
+
+        # Try to locate the MiniZinc executable
+        executable = shutil.which(name, path=os.pathsep.join(path))
+        if executable is not None:
+            return cls(Path(executable))
+        return None
+
+    def run(
+        self,
+        mzn_files: List[Path],
+        inline_includes: InlineOption = InlineOption.DISABLED,
+        remove_litter: bool = False,
+        get_diversity_anns: bool = False,
+        get_solve_anns: bool = True,
+        output_all: bool = True,
+        mzn_output: Optional[Path] = None,
+        remove_anns: Optional[List[str]] = None,
+        remove_items: Optional[List[str]] = None,
+    ) -> Dict[str, Any]:
+        # Do not change the order of the arguments 'inline-includes', 'remove-items:output', 'remove-litter' and 'get-diversity-anns'
+        tool_run_cmd: List[Union[str, Path]] = [
+            str(self._executable),
+            "json_out:-",
+        ]
+
+        for f in mzn_files:
+            tool_run_cmd.append(str(f))
+
+        if inline_includes == InlineOption.ALL:
+            tool_run_cmd.append("inline-all_includes")
+        elif inline_includes == InlineOption.NON_LIBRARY:
+            tool_run_cmd.append("inline-includes")
+
+        if remove_items is not None and len(remove_items) > 0:
+            tool_run_cmd.append(f"remove-items:{','.join(remove_items)}")
+        if remove_anns is not None and len(remove_anns) > 0:
+            tool_run_cmd.append(f"remove-anns:{','.join(remove_anns)}")
+
+        if remove_litter:
+            tool_run_cmd.append("remove-litter")
+        if get_diversity_anns:
+            tool_run_cmd.append("get-diversity-anns")
+
+        if mzn_output is not None:
+            tool_run_cmd.append(f"out:{str(mzn_output)}")
+        else:
+            tool_run_cmd.append("no_out")
+
+        # Extract the diversity annotations.
+        proc = subprocess.run(
+            tool_run_cmd, stderr=subprocess.PIPE, stdout=subprocess.PIPE
+        )
+        if proc.returncode != 0:
+            raise MiniZincError(message=str(proc.stderr))
+        return json.loads(proc.stdout)

src/minizinc/driver.py

@@ -26,7 +26,13 @@
 #: Default locations on MacOS where the MiniZinc packaged release would be installed
 MAC_LOCATIONS = [
     str(Path("/Applications/MiniZincIDE.app/Contents/Resources")),
+    str(Path("/Applications/MiniZincIDE.app/Contents/Resources/bin")),
     str(Path("~/Applications/MiniZincIDE.app/Contents/Resources").expanduser()),
+    str(
+        Path(
+            "~/Applications/MiniZincIDE.app/Contents/Resources/bin"
+        ).expanduser()
+    ),
 ]
 #: Default locations on Windows where the MiniZinc packaged release would be installed
 WIN_LOCATIONS = [

src/minizinc/helpers.py

@@ -1,7 +1,7 @@
 import sys
 from dataclasses import asdict, is_dataclass
 from datetime import timedelta
-from typing import Any, Dict, Optional, Sequence, Union
+from typing import Any, Dict, Iterable, List, Optional, Sequence, Union
 
 import minizinc
 
@@ -102,7 +102,7 @@ def check_solution(
 
     assert isinstance(solution, dict)
     for k, v in solution.items():
-        if k not in ("objective", "__output_item"):
+        if k not in ("objective", "_output_item", "_checker"):
             instance[k] = v
     check = instance.solve(time_limit=time_limit)
 
@@ -120,3 +120,101 @@ def check_solution(
         minizinc.Status.OPTIMAL_SOLUTION,
         minizinc.Status.ALL_SOLUTIONS,
     ]
+
+
+def _add_diversity_to_opt_model(
+    inst: minizinc.Instance,
+    obj_annots: Dict[str, Any],
+    vars: List[Dict[str, Any]],
+    sol_fix: Optional[Dict[str, Iterable]] = None,
+):
+    for var in vars:
+        # Current and previous variables
+        varname = var["name"]
+        varprevname = var["prev_name"]
+
+        # Add the 'previous solution variables'
+        inst[varprevname] = []
+
+        # Fix the solution to given once
+        if sol_fix is not None:
+            inst.add_string(
+                f"constraint {varname} == {list(sol_fix[varname])};\n"
+            )
+
+    # Add the optimal objective.
+    if obj_annots["sense"] != "0":
+        obj_type = obj_annots["type"]
+        inst.add_string(f"{obj_type}: div_orig_opt_objective :: output;\n")
+        inst.add_string(
+            f"constraint div_orig_opt_objective == {obj_annots['name']};\n"
+        )
+        if obj_annots["sense"] == "-1":
+            inst.add_string(f"solve minimize {obj_annots['name']};\n")
+        else:
+            inst.add_string(f"solve maximize {obj_annots['name']};\n")
+    else:
+        inst.add_string("solve satisfy;\n")
+
+    return inst
+
+
+def _add_diversity_to_div_model(
+    inst: minizinc.Instance,
+    vars: List[Dict[str, Any]],
+    obj_sense: str,
+    gap: Union[int, float],
+    sols: Dict[str, Any],
+):
+    # Add the 'previous solution variables'
+    for var in vars:
+        # Current and previous variables
+        varname = var["name"]
+        varprevname = var["prev_name"]
+        varprevisfloat = "float" in var["prev_type"]
+
+        distfun = var["distance_function"]
+        prevsols = sols[varprevname] + [sols[varname]]
+        prevsol = (
+            __round_elements(prevsols, 6) if varprevisfloat else prevsols
+        )  # float values are rounded to six decimal places to avoid infeasibility due to decimal errors.
+
+        # Add the previous solutions to the model code.
+        inst[varprevname] = prevsol
+
+        # Add the diversity distance measurement to the model code.
+        dim = __num_dim(prevsols)
+        dotdots = ", ".join([".." for _ in range(dim - 1)])
+        varprevtype = "float" if "float" in var["prev_type"] else "int"
+        inst.add_string(
+            f"array [1..{len(prevsol)}] of var {varprevtype}: dist_{varname} :: output = [{distfun}({varname}, {varprevname}[sol,{dotdots}]) | sol in 1..{len(prevsol)}];\n"
+        )
+
+    # Add the bound on the objective.
+    if obj_sense == "-1":
+        inst.add_string(f"constraint div_orig_objective <= {gap};\n")
+    elif obj_sense == "1":
+        inst.add_string(f"constraint div_orig_objective >= {gap};\n")
+
+    # Add new objective: maximize diversity.
+    dist_sum = "+".join([f'sum(dist_{var["name"]})' for var in vars])
+    inst.add_string(f"solve maximize {dist_sum};\n")
+
+    return inst
+
+
+def __num_dim(x: List) -> int:
+    i = 1
+    while isinstance(x[0], list):
+        i += 1
+        x = x[0]
+    return i
+
+
+def __round_elements(x: List, p: int) -> List:
+    for i in range(len(x)):
+        if isinstance(x[i], list):
+            x[i] = __round_elements(x[i], p)
+        elif isinstance(x[i], float):
+            x[i] = round(x[i], p)
+    return x