dekker.one
Flat White Vitriol - An incremental solver protocol for combinatorial solving using shared objects
1# Flat White Vitriol (FZnSO) - An incremental solver protocol for combinatorial solving using shared objects
2
3## Introduction
4
5## Common Functionality
6
7Although solvers are able to define their own functionality using the FZnSO protocol, we advocate for the following common functionality to be implemented by different solvers.
8This will allow for a more consistent user experience when interacting with different solvers.
9Even if a solver does not implement all of these functions, we recommend that the solvers do not use the same name for different functionality.
10
11### Common Options
12
13A solver will expose its available options through `fznso_option_list`.
14We recommend that solvers eagerly implement the following options:
15
16- `all_optimal` (`bool`, default: `false`): If set to `true`, the solver will after finding an optimal solution, continue to search for other solutions with the same objective value.
17- `fixed_search` (`bool`, default: `false`): If set to `true`, the solver will strictly follow the search order defined by the user.
18- `intermediate` (`bool`, default: `false`): If set to `true` for a problem with an objective strategy set, the solver will trigger its `on_solution` callback when it finds an intermediate solution.
19 Afterward, the solver will continue the search until it finds the next solution, or it proves that no better solutions exist (returning the `FznsoComplete` status).
20- `threads` (`int`, default: `1`): For multithreaded solvers, this option will set the number of threads to use.
21- `time_limit` (`int`, default: `-1`): If set to a positive integer, the solver will abandon the search after the specified number of milliseconds.
22- `random_seed` (`opt int`, default: `<>`): If set to a positive integer, the solver will use the given value as the seed for its random number generator.
23 Solvers are encouraged to use a variable seed for the default value.
24- `verbose` (`bool`, default: `false`): If set to `true`, the solver will print additional information about its process to `stderr`.
25
26### Common Constraints
27
28A solver will expose the constraints that can be used in a `FznsoModel` through `fznso_constraint_list`.
29We encourage solvers to support the constraints using the names and definitions from the [FlatZinc Builtins](https://docs.minizinc.dev/en/stable/lib-flatzinc.html).
30Other MiniZinc (global) constraints are also encouraged to be implemented, using the `fzn_` prefix.
31
32### Common Objective Strategies
33
34A solver will expose the objective strategies that can be used in a `FznsoModel` through `fznso_objective_list`.
35We encourage solvers to support the following objective strategies if possible:
36
37- `lex_maximize_int` (`list of var int`) | `lex_maximize_float` (`list of var float`): The solver will maximize the list of decision variables in lexicographical order, i.e., the first variable is maximized first, then the second variable, etc.
38- `lex_minimize_int` (`list of var int`) | `lex_minimize_float` (`list of var float`): The solver will minimize the list of decision variables in lexicographical order, i.e., the first variable is minimized first, then the second variable, etc.
39- `maximize_int` (`var int`) | `maximize_float` (`var float`): The solver will maximize the given decision variable.
40- `minimize_int` (`var int`) | `minimize_float` (`var float`): The solver will minimize the given decision variable.
41- `pareto_maximize_int` (`list of var int`) | `pareto_maximize_float` (`list of
42var float`): The solver will output solutions where at least one decision variable is assigned a higher value than it was assigned in all previous solutions.
43
44Note that if no objective is set, then the solver is expected to find any valid assignment of the decision variables that satisfies the constraints added to the solver.