diff --git a/docs/advanced_usage.rst b/docs/advanced_usage.rst index c63745d..25f6444 100644 --- a/docs/advanced_usage.rst +++ b/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 ------------------ diff --git a/src/minizinc/__init__.py b/src/minizinc/__init__.py index a4b7f42..3d7cb33 100644 --- a/src/minizinc/__init__.py +++ b/src/minizinc/__init__.py @@ -50,4 +50,5 @@ "Result", "Solver", "Status", + "Diversity", ] diff --git a/src/minizinc/analyse.py b/src/minizinc/analyse.py new file mode 100644 index 0000000..1d19296 --- /dev/null +++ b/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) diff --git a/src/minizinc/driver.py b/src/minizinc/driver.py index 67f5053..153500d 100644 --- a/src/minizinc/driver.py +++ b/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 = [ diff --git a/src/minizinc/helpers.py b/src/minizinc/helpers.py index 651713d..159ba2c 100644 --- a/src/minizinc/helpers.py +++ b/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 diff --git a/src/minizinc/instance.py b/src/minizinc/instance.py index 1032e5e..54f1572 100644 --- a/src/minizinc/instance.py +++ b/src/minizinc/instance.py @@ -4,12 +4,13 @@ import asyncio import contextlib import json +import logging import os import re import sys import tempfile import warnings -from dataclasses import field, make_dataclass +from dataclasses import asdict, field, is_dataclass, make_dataclass from datetime import timedelta from enum import EnumMeta from keyword import iskeyword @@ -30,8 +31,9 @@ import minizinc +from .analyse import InlineOption, MznAnalyse from .driver import Driver -from .error import MiniZincError, parse_error +from .error import ConfigurationError, MiniZincError, parse_error from .json import ( MZNJSONDecoder, MZNJSONEncoder, @@ -259,6 +261,191 @@ async def solve_async( solution = result.solution return Result(status, solution, statistics) + async def diverse_solutions( + self, + num_diverse_solutions: Optional[int] = None, + reference_solution: Optional[Union[Result, Dict]] = None, + mzn_analyse: Optional[MznAnalyse] = None, + optimise_diverse_sol: Optional[bool] = True, + solver: Optional[Solver] = None, + ) -> AsyncIterator[Result]: + """Solves the Instance to find diverse solutions using its given solver configuration. + + Finds diverse solutions to the given MiniZinc instance using the given solver + configuration. Every diverse solution is yielded one at a + time. If a reference solution is provided the diverse solutions are generated + around it. For more information regarding this methods and its + arguments, see the documentation of :func:`~MiniZinc.Instance.diverse_solutions`. + + Yields: + Result: (TODO) + A Result object containing the current solving status, values + assigned, and statistical information. + + """ + from .helpers import ( + _add_diversity_to_div_model, + _add_diversity_to_opt_model, + ) + + # Loads diverse solution generator if MiniZinc Data Annotator is present + if mzn_analyse is None: + mzn_analyse = MznAnalyse.find() + if mzn_analyse is None: + raise ConfigurationError( + "mzn-analyse executable could not be located" + ) + + try: + # Create a temporary file in which the diversity model (generated by mzn-analyse) is placed + div_file = tempfile.NamedTemporaryFile( + prefix="mzn_div", suffix=".mzn", delete=False + ) + + # Extract the diversity annotations. + with self.files() as files: + div_anns = mzn_analyse.run( + files, + get_diversity_anns=True, + inline_includes=InlineOption.NON_LIBRARY, + remove_items=["output"], + remove_anns=["mzn_expression_name"], + remove_litter=True, + mzn_output=Path(div_file.name), + )["get-diversity-annotations"] + + # Objective annotations. + obj_anns = div_anns["objective"] + variables = div_anns["vars"] + + if len(variables) <= 0: + raise MiniZincError(message="No distance measure is specified") + + if solver is None: + solver = self._solver + inst = Instance(solver, Model(Path(div_file.name)), self._driver) + + max_gap = None # Place holder for max gap. + prev_solutions = None # Place holder for prev solutions + + # Number of total diverse solutions - If not provided use the count provided in the MiniZinc model + div_num = ( + int(div_anns["k"]) + if num_diverse_solutions is None + else num_diverse_solutions + ) + # Increase the solution count by one if a reference solution is provided + if reference_solution: + div_num += 1 + + # Initial (re-)optimisation run + with inst.branch() as child: + # Add constraints to the model that sets the decision variables to the reference solution, if provided + if reference_solution: + if isinstance(reference_solution, Result) and is_dataclass( + reference_solution.solution + ) and not isinstance(reference_solution.solution, type): + solution_obj = asdict(reference_solution.solution) + else: + assert isinstance(reference_solution, dict) + solution_obj = reference_solution + for k, v in solution_obj.items(): + if k not in ("objective", "_output_item", "_checker"): + child[k] = v + + # We will extend the annotated model with the objective and vars. + child = _add_diversity_to_opt_model(child, obj_anns, variables) + + # Solve original model to optimality. + if minizinc.logger.isEnabledFor(logging.INFO): + model_type = "opt" if obj_anns["sense"] != "0" else "sat" + minizinc.logger.info( + f"[Sol 1] Solving the original ({model_type}) model to get a solution" + ) + res: Result = await child.solve_async() + # No (additional) solutions can be found, return from function + if res.solution is None: + return + + if reference_solution is None: + yield res + + # Calculate max gap. + max_gap = ( + (1 - int(obj_anns["sense"]) * float(div_anns["gap"])) + * float(res["div_orig_opt_objective"]) + if obj_anns["sense"] != "0" + else 0 + ) + + # Store current solution as previous solution + prev_solutions = asdict(res.solution) + + for i in range(2, div_num + 1): + with inst.branch() as child: + minizinc.logger.info( + f"[Sol {i}] Generating diverse solution {i}" + + (" (optimal)" if optimise_diverse_sol else "") + ) + + # We will extend the annotated model with the objective and vars. + child = _add_diversity_to_div_model( + child, + variables, + obj_anns["sense"], + max_gap, + prev_solutions, + ) + + # Solve div model to get a diverse solution. + res = await child.solve_async() + + # No (additional) solutions can be found, return from function + if res.solution is None: + return + + # Solve diverse solution to optimality after fixing the diversity vars to the obtained solution + if optimise_diverse_sol: + # Solution as dictionary + sol_div = asdict(res.solution) + + # COMMENDTED OUT FOR NOW: Merge the solution values. + # sol_dist = dict() + # for var in variables: + # distvarname = "dist_"+var["name"] + # sol_dist[distvarname] = (sol_div[distvarname]) + + # Solve opt model after fixing the diversity vars to the obtained solution + with inst.branch() as child: + child = _add_diversity_to_opt_model( + child, obj_anns, variables, sol_div + ) + + # Solve the model + res = await child.solve_async() + + # No (additional) solutions can be found, return from function + if res.solution is None: + return + + # COMMENDTED OUT FOR NOW: Add distance to previous solutions + # sol_opt = asdict(res.solution) + # sol_opt["distance_to_prev_vars"] = sol_dist + yield res + + # Store current solution as previous solution + curr_solution = asdict(res.solution) + # Add the current solution to prev solution container + assert prev_solutions is not None + for var in variables: + prev_solutions[var["prev_name"]].append( + curr_solution[var["name"]] + ) + finally: + # Remove temporary file created for the diversity model + div_file.close() + os.remove(div_file.name) + async def solutions( self, time_limit: Optional[timedelta] = None,