diff --git a/cpmpy/expressions/core.py b/cpmpy/expressions/core.py index b2a01ba62..47d03be41 100644 --- a/cpmpy/expressions/core.py +++ b/cpmpy/expressions/core.py @@ -11,7 +11,7 @@ Here is a list of standard python operators and what object (with what expr.name) it creates: - Comparisons: + **Comparisons**: - x == y Comparison("==", x, y) - x != y Comparison("!=", x, y) @@ -20,9 +20,9 @@ - x > y Comparison(">", x, y) - x >= y Comparison(">=", x, y) - Mathematical operators: + **Mathematical operators**: - - -x Operator("-", [x]) + - −x Operator("-", [x]) - x + y Operator("sum", [x,y]) - sum([x,y,z]) Operator("sum", [x,y,z]) - sum([c0*x, c1*y, c2*z]) Operator("wsum", [[c0,c1,c2],[x,y,z]]) @@ -32,7 +32,7 @@ - x % y Operator("mod", [x,y]) - x ** y Operator("pow", [x,y]) - Logical operators: + **Logical operators**: - x & y Operator("and", [x,y]) - x | y Operator("or", [x,y]) @@ -47,14 +47,16 @@ Apart from operator overloading, expressions implement two important functions: - - `is_bool()` which returns whether the __return type__ of the expression is Boolean. - If it does, the expression can be used as top-level constraint - or in logical operators. + - `is_bool()` + which returns whether the return type of the expression is Boolean. + If it does, the expression can be used as top-level constraint + or in logical operators. - - `value()` computes the value of this expression, by calling .value() on its - subexpressions and doing the appropriate computation - this is used to conveniently print variable values, objective values - and any other expression value (e.g. during debugging). + - `value()` + computes the value of this expression, by calling .value() on its + subexpressions and doing the appropriate computation + this is used to conveniently print variable values, objective values + and any other expression value (e.g. during debugging). =============== List of classes diff --git a/cpmpy/expressions/globalfunctions.py b/cpmpy/expressions/globalfunctions.py index ed43c2589..8110a261d 100644 --- a/cpmpy/expressions/globalfunctions.py +++ b/cpmpy/expressions/globalfunctions.py @@ -1,9 +1,10 @@ #!/usr/bin/env python -# -*- coding:utf-8 -*- +#-*- coding:utf-8 -*- ## ## globalfunctions.py ## """ + Global functions conveniently express numerical global constraints. Using global functions ------------------------ diff --git a/cpmpy/expressions/utils.py b/cpmpy/expressions/utils.py index 06bf92fc3..ecd865fe2 100644 --- a/cpmpy/expressions/utils.py +++ b/cpmpy/expressions/utils.py @@ -12,14 +12,21 @@ .. autosummary:: :nosignatures: + is_bool is_int is_num + is_false_cst + is_true_cst + is_boolexpr is_pure_list is_any_list + is_transition flatlist all_pairs argval + argvals eval_comparison + get_bounds """ import numpy as np diff --git a/cpmpy/expressions/variables.py b/cpmpy/expressions/variables.py index e05fc64f2..6c70e3eb0 100644 --- a/cpmpy/expressions/variables.py +++ b/cpmpy/expressions/variables.py @@ -24,9 +24,18 @@ Boolean and Integer decision variables are the key elements of a CP model. - All variables in CPMpy are n-dimensional array objects and have defined dimensions. Following the numpy library, the dimension sizes of an n-dimenionsal array is called its __shape__. In CPMpy all variables are considered an array with a given shape. For 'single' variables the shape is '1'. For an array of length `n` the shape is 'n'. An `n*m` matrix has shape (n,m), and tensors with more than 2 dimensions are all supported too. For the implementation of this, CPMpy builts on numpy's n-dimensional ndarray and inherits many of its benefits (vectorized operators and advanced indexing). + All variables in CPMpy are n-dimensional array objects and have defined dimensions. + Following the numpy library, the dimension sizes of an n-dimenionsal array is called its __shape__. + In CPMpy all variables are considered an array with a given shape. For 'single' variables the shape + is '1'. For an array of length `n` the shape is 'n'. An `n*m` matrix has shape (n,m), and tensors + with more than 2 dimensions are all supported too. For the implementation of this, + CPMpy builts on numpy's n-dimensional ndarray and inherits many of its benefits + (vectorized operators and advanced indexing). - This module contains the cornerstone `boolvar()` and `intvar()` functions, which create (numpy arrays of) variables. There is also a helper function `cpm_array` for wrapping standard numpy arrays so they can be indexed by a variable. Apart from these 3 functions, none of the classes in this module should be directly created; they are created by these 3 helper functions. + This module contains the cornerstone `boolvar()` and `intvar()` functions, which create (numpy arrays of) + variables. There is also a helper function `cpm_array()` for wrapping standard numpy arrays so they can be + indexed by a variable. Apart from these 3 functions, none of the classes in this module should be directly + instantiated; they are created by these 3 helper functions. =============== @@ -135,7 +144,7 @@ def IntVar(lb, ub, shape=1, name=None): def intvar(lb, ub, shape=1, name=None): """ - Integer decision variables are constructed by specifying the lowest (lb) + Integer decision variables are constructed by specifying the lowest (lb) value the decision variable can take, as well as the highest value (ub). Arguments: diff --git a/cpmpy/model.py b/cpmpy/model.py index d696213e3..86d30909c 100644 --- a/cpmpy/model.py +++ b/cpmpy/model.py @@ -15,9 +15,9 @@ See the examples for basic usage, which involves: - - creation, e.g. m = Model(cons, minimize=obj) - - solving, e.g. m.solve() - - optionally, checking status/runtime, e.g. m.status() + - creation, e.g. `m = Model(cons, minimize=obj)` + - solving, e.g. `m.solve()` + - optionally, checking status/runtime, e.g. `m.status()` =============== List of classes diff --git a/cpmpy/solvers/__init__.py b/cpmpy/solvers/__init__.py index 1b1459f80..6ac970d20 100644 --- a/cpmpy/solvers/__init__.py +++ b/cpmpy/solvers/__init__.py @@ -2,8 +2,8 @@ CPMpy interfaces to (the Python API interface of) solvers Solvers typically use some of the generic transformations in - `transformations` as well as specific reformulations to map the - CPMpy expression to the solver's Python API + :mod:`cpmpy.transformations` as well as specific reformulations to map the + CPMpy expression to the solver's Python API. ================== List of submodules diff --git a/cpmpy/solvers/choco.py b/cpmpy/solvers/choco.py index 1cf4574c2..882677399 100644 --- a/cpmpy/solvers/choco.py +++ b/cpmpy/solvers/choco.py @@ -1,10 +1,15 @@ #!/usr/bin/env python +#-*- coding:utf-8 -*- +## ## choco.py ## """ Interface to Choco solver's Python API - ... + Requires that the 'pychoco' python package is installed: + + $ pip install pychoco + Documentation of the solver's own Python API: https://pypi.org/project/pychoco/ @@ -18,6 +23,10 @@ :nosignatures: CPM_choco + + ============== + Module details + ============== """ import time diff --git a/cpmpy/solvers/exact.py b/cpmpy/solvers/exact.py index 05549ca3e..e3136f15a 100644 --- a/cpmpy/solvers/exact.py +++ b/cpmpy/solvers/exact.py @@ -6,8 +6,11 @@ """ Interface to Exact - Exact solves decision and optimization problems formulated as integer linear programs. Under the hood, it converts integer variables to binary (0-1) variables and applies highly efficient propagation routines and strong cutting-planes / pseudo-Boolean conflict analysis. + Exact solves decision and optimization problems formulated as integer linear programs. + Under the hood, it converts integer variables to binary (0-1) variables and applies highly efficient + propagation routines and strong cutting-planes / pseudo-Boolean conflict analysis. + The solver's git repository: https://gitlab.com/JoD/exact =============== @@ -18,6 +21,10 @@ :nosignatures: CPM_exact + + ============== + Module details + ============== """ import sys # for stdout checking import time @@ -84,7 +91,7 @@ def __init__(self, cpm_model=None, subsolver=None): Arguments: - cpm_model: Model(), a CPMpy Model() (optional) - - subsolver: None + - subsolver: None, not used """ if not self.supported(): raise Exception("Install 'exact' as a Python package to use this solver interface") diff --git a/cpmpy/solvers/gurobi.py b/cpmpy/solvers/gurobi.py index c43761dd1..d58e93a8c 100644 --- a/cpmpy/solvers/gurobi.py +++ b/cpmpy/solvers/gurobi.py @@ -1,4 +1,8 @@ #!/usr/bin/env python +#-*- coding:utf-8 -*- +## +## gurobi.py +## """ Interface to the python 'gurobi' package @@ -6,12 +10,13 @@ $ pip install gurobipy - as well as the Gurobi bundled binary packages, downloadable from: - https://www.gurobi.com/ In contrast to other solvers in this package, Gurobi is not free to use and requires an active licence You can read more about available licences at https://www.gurobi.com/downloads/ + Documentation of the solver's own Python API: + https://www.gurobi.com/documentation/current/refman/py_python_api_details.html + =============== List of classes =============== @@ -83,6 +88,7 @@ def __init__(self, cpm_model=None, subsolver=None): Arguments: - cpm_model: a CPMpy Model() + - subsolver: None, not used """ if not self.supported(): raise Exception( diff --git a/cpmpy/solvers/minizinc.py b/cpmpy/solvers/minizinc.py index b01420a1c..3248d550e 100644 --- a/cpmpy/solvers/minizinc.py +++ b/cpmpy/solvers/minizinc.py @@ -1,8 +1,18 @@ #!/usr/bin/env python +#-*- coding:utf-8 -*- +## +## minizinc.py +## """ Interface to MiniZinc's Python API - CPMpy can translate CPMpy models to the (text-based) MiniZinc language. + Requires that the 'minizinc' python package is installed: + + $ pip install minizinc + + as well as the Minizinc bundled binary packages, downloadable from: + https://github.com/MiniZinc/MiniZincIDE/releases + MiniZinc is a free and open-source constraint modeling language. MiniZinc is used to model constraint satisfaction and optimization problems in @@ -14,6 +24,8 @@ Documentation of the solver's own Python API: https://minizinc-python.readthedocs.io/ + CPMpy can translate CPMpy models to the (text-based) MiniZinc language. + =============== List of classes =============== @@ -22,6 +34,10 @@ :nosignatures: CPM_minizinc + + ============== + Module details + ============== """ import re import warnings @@ -674,7 +690,7 @@ def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from - time_limit: stop after this many seconds (default: None) - solution_limit: stop after this many solutions (default: None) - call_from_model: whether the method is called from a CPMpy Model instance or not - - any other keyword argument + - kwargs: any keyword argument, sets parameters of solver object, overwrites construction-time kwargs Returns: number of solutions found """ diff --git a/cpmpy/solvers/ortools.py b/cpmpy/solvers/ortools.py index b5b55627d..3805bae3c 100644 --- a/cpmpy/solvers/ortools.py +++ b/cpmpy/solvers/ortools.py @@ -4,7 +4,12 @@ ## ortools.py ## """ - Interface to ortools' CP-SAT Python API + Interface to OR-Tools' CP-SAT Python API. + + The 'ortools' python package is bundled by default with CPMpy. + It can be installed through `pip`: + + $ pip install ortools Google OR-Tools is open source software for combinatorial optimization, which seeks to find the best solution to a problem out of a very large set of possible solutions. @@ -22,6 +27,10 @@ :nosignatures: CPM_ortools + + ============== + Module details + ============== """ import sys # for stdout checking import numpy as np @@ -42,7 +51,7 @@ class CPM_ortools(SolverInterface): """ - Interface to the python 'ortools' CP-SAT API + Interface to the Python 'ortools' CP-SAT API Requires that the 'ortools' python package is installed: $ pip install ortools @@ -79,7 +88,7 @@ def __init__(self, cpm_model=None, subsolver=None): Arguments: - cpm_model: Model(), a CPMpy Model() (optional) - - subsolver: None + - subsolver: None, not used """ if not self.supported(): raise Exception("Install the python 'ortools' package to use this solver interface") diff --git a/cpmpy/solvers/pysat.py b/cpmpy/solvers/pysat.py index 8ca520fa8..2f6371978 100644 --- a/cpmpy/solvers/pysat.py +++ b/cpmpy/solvers/pysat.py @@ -6,6 +6,10 @@ """ Interface to PySAT's API + Requires that the 'python-sat' python package is installed: + + $ pip install python-sat[aiger,approxmc,cryptosat,pblib] + PySAT is a Python (2.7, 3.4+) toolkit, which aims at providing a simple and unified interface to a number of state-of-art Boolean satisfiability (SAT) solvers as well as to a variety of cardinality and pseudo-Boolean encodings. @@ -28,6 +32,10 @@ :nosignatures: CPM_pysat + + ============== + Module details + ============== """ from .solver_interface import SolverInterface, SolverStatus, ExitStatus from ..exceptions import NotSupportedError diff --git a/cpmpy/solvers/pysdd.py b/cpmpy/solvers/pysdd.py index a00800121..c30bf373b 100644 --- a/cpmpy/solvers/pysdd.py +++ b/cpmpy/solvers/pysdd.py @@ -1,6 +1,15 @@ +#!/usr/bin/env python +#-*- coding:utf-8 -*- +## +## pysdd.py +## """ Interface to PySDD's API + Requires that the 'PySDD' python package is installed: + + $ pip install PySDD + PySDD is a knowledge compilation package for Sentential Decision Diagrams (SDD) https://pysdd.readthedocs.io/en/latest/ @@ -19,6 +28,10 @@ :nosignatures: CPM_pysdd + + ============== + Module details + ============== """ from functools import reduce from .solver_interface import SolverInterface, SolverStatus, ExitStatus diff --git a/cpmpy/solvers/utils.py b/cpmpy/solvers/utils.py index 770b036c9..41a180581 100644 --- a/cpmpy/solvers/utils.py +++ b/cpmpy/solvers/utils.py @@ -6,9 +6,6 @@ """ Utilities for handling solvers - Contains a static variable `builtin_solvers` that lists - CPMpy solvers (first one is the default solver by default) - ================= List of functions ================= @@ -36,9 +33,10 @@ def param_combinations(all_params, remaining_keys=None, cur_params=None): Recursively yield all combinations of param values For example usage, see `examples/advanced/hyperparameter_search.py` + https://github.com/CPMpy/cpmpy/blob/master/examples/advanced/hyperparameter_search.py - all_params is a dict of {key: list} items, e.g.: - {'val': [1,2], 'opt': [True,False]} + {'val': [1,2], 'opt': [True,False]} - output is an generator over all {key:value} combinations of the keys and values. For the example above: diff --git a/cpmpy/solvers/z3.py b/cpmpy/solvers/z3.py index d02f1c3e3..5576e4eea 100644 --- a/cpmpy/solvers/z3.py +++ b/cpmpy/solvers/z3.py @@ -1,7 +1,15 @@ #!/usr/bin/env python +#-*- coding:utf-8 -*- +## +## z3.py +## """ Interface to z3's API + Requires that the 'z3-solver' python package is installed: + + $ pip install z3-solver + Z3 is a highly versatile and effective theorem prover from Microsoft. Underneath, it is an SMT solver with a wide scala of theory solvers. We will interface to the finite-domain integer related parts of the API @@ -19,6 +27,10 @@ :nosignatures: CPM_z3 + + ============== + Module details + ============== """ from .solver_interface import SolverInterface, SolverStatus, ExitStatus from ..exceptions import NotSupportedError diff --git a/cpmpy/tools/__init__.py b/cpmpy/tools/__init__.py index bba0efc1e..15fc0fdf0 100644 --- a/cpmpy/tools/__init__.py +++ b/cpmpy/tools/__init__.py @@ -1,5 +1,17 @@ """ Set of independent tools that users might appreciate. + + ============= + List of tools + ============= + + .. autosummary:: + :nosignatures: + + explain + dimacs + maximal_propagate + tune_solver """ from .tune_solver import ParameterTuner, GridSearchTuner diff --git a/cpmpy/tools/dimacs.py b/cpmpy/tools/dimacs.py index b3c138e2f..0c7e11a57 100644 --- a/cpmpy/tools/dimacs.py +++ b/cpmpy/tools/dimacs.py @@ -1,3 +1,18 @@ +#!/usr/bin/env python +#-*- coding:utf-8 -*- +## +## dimacs.py +## +""" + This file implements helper functions for exporting CPMpy models from and to DIMACS format. + DIMACS is a textual format to represent CNF problems. + The header of the file should be formatted as `p cnf ` + If the number of variables and constraints are not given, it is inferred by the parser. + + Each remaining line of the file is formatted as a list of integers. + An integer represents a Boolean variable and a negative Boolean variable is represented using a `-` sign. +""" + import cpmpy as cp from cpmpy.expressions.variables import _BoolVarImpl, NegBoolView @@ -9,16 +24,6 @@ import re -""" -This file implements helper functions for exporting CPMpy models from and to DIMACS format. -DIMACS is a textual format to represent CNF problems. -The header of the file should be formatted as `p cnf -If the number of variables and constraints are not given, it is inferred by the parser. - -Each remaining line of the file is formatted as a list of integers. -An integer represents a Boolean variable and a negative Boolean variable is represented using a `-` sign. -""" - def write_dimacs(model, fname=None): """ diff --git a/cpmpy/tools/explain/__init__.py b/cpmpy/tools/explain/__init__.py index b17289035..bc0e2b10f 100644 --- a/cpmpy/tools/explain/__init__.py +++ b/cpmpy/tools/explain/__init__.py @@ -1,3 +1,24 @@ +#!/usr/bin/env python +#-*- coding:utf-8 -*- +## +## __init__.py +## +""" + Collection of tools for explanation techniques. + + ============= + List of tools + ============= + + .. autosummary:: + :nosignatures: + + mus + mss + mcs + utils +""" + from .mus import * from .mss import * from .mcs import * \ No newline at end of file diff --git a/cpmpy/tools/explain/mcs.py b/cpmpy/tools/explain/mcs.py index cde1323b2..28ffa0db9 100644 --- a/cpmpy/tools/explain/mcs.py +++ b/cpmpy/tools/explain/mcs.py @@ -5,7 +5,7 @@ def mcs(soft, hard=[], solver="ortools"): """ Compute Minimal Correction Subset of unsatisfiable model. - Remvoving these contraints will result in a satisfiable model. + Removing these contraints will result in a satisfiable model. Computes a subset of constraints which minimizes the total number of constraints to be removed """ return mcs_opt(soft, hard, 1, solver) diff --git a/cpmpy/tools/explain/utils.py b/cpmpy/tools/explain/utils.py index 5afe2fc3c..8db2fd691 100644 --- a/cpmpy/tools/explain/utils.py +++ b/cpmpy/tools/explain/utils.py @@ -1,3 +1,21 @@ +#!/usr/bin/env python +#-*- coding:utf-8 -*- +## +## utils.py +## +""" + Utilities for explanation techniques + + ================= + List of functions + ================= + + .. autosummary:: + :nosignatures: + + make_assump_model +""" + import cpmpy as cp from cpmpy.transformations.normalize import toplevel_list diff --git a/cpmpy/tools/tune_solver.py b/cpmpy/tools/tune_solver.py index e6e37b8e3..c56e1099a 100644 --- a/cpmpy/tools/tune_solver.py +++ b/cpmpy/tools/tune_solver.py @@ -6,9 +6,9 @@ Programming, Artificial Intelligence, and Operations Research. CPAIOR 2022. Lecture Notes in Computer Science, vol 13292. Springer, Cham. https://doi.org/10.1007/978-3-031-08011-1_6 - DOI: https://doi.org/10.1007/978-3-031-08011-1_6 - Link to paper: https://rdcu.be/cQyWR - Link to original code of paper: https://github.com/ML-KULeuven/DeCaprio + - DOI: https://doi.org/10.1007/978-3-031-08011-1_6 + - Link to paper: https://rdcu.be/cQyWR + - Link to original code of paper: https://github.com/ML-KULeuven/DeCaprio This code currently only implements the author's 'Hamming' surrogate function. The parameter tuner iteratively finds better hyperparameters close to the current best configuration during the search. @@ -23,13 +23,15 @@ from ..solvers.solver_interface import ExitStatus class ParameterTuner: + """ + Parameter tuner based on DeCaprio method [ref_to_decaprio] + """ def __init__(self, solvername, model, all_params=None, defaults=None): - """ - Parameter tuner based on DeCaprio method [ref_to_decaprio] - :param: solvername: Name of solver to tune - :param: model: CPMpy model to tune parameters on - :param: all_params: optional, dictionary with parameter names and values to tune. If None, use predefined parameter set. + """ + :param solvername: Name of solver to tune + :param model: CPMpy model to tune parameters on + :param all_params: optional, dictionary with parameter names and values to tune. If None, use predefined parameter set. """ self.solvername = solvername self.model = model @@ -44,9 +46,9 @@ def __init__(self, solvername, model, all_params=None, defaults=None): def tune(self, time_limit=None, max_tries=None, fix_params={}): """ - :param: time_limit: Time budget to run tuner in seconds. Solver will be interrupted when time budget is exceeded - :param: max_tries: Maximum number of configurations to test - :param: fix_params: Non-default parameters to run solvers with. + :param time_limit: Time budget to run tuner in seconds. Solver will be interrupted when time budget is exceeded + :param max_tries: Maximum number of configurations to test + :param fix_params: Non-default parameters to run solvers with. """ if time_limit is not None: start_time = time.time() diff --git a/cpmpy/transformations/__init__.py b/cpmpy/transformations/__init__.py index 516b75c65..7acb14e12 100644 --- a/cpmpy/transformations/__init__.py +++ b/cpmpy/transformations/__init__.py @@ -1,5 +1,5 @@ """ - Methods to transform CPMpy expressions in other CPMpy expressions + Methods to transform CPMpy expressions into other CPMpy expressions Input and output are always CPMpy expressions, so transformations can be chained and called multiple times, as needed. @@ -15,6 +15,13 @@ .. autosummary:: :nosignatures: + comparison + decompose_global flatten_model get_variables + linearize + negation + normalize + reification + to_cnf """ diff --git a/cpmpy/transformations/comparison.py b/cpmpy/transformations/comparison.py index f9bce788c..eee30461c 100644 --- a/cpmpy/transformations/comparison.py +++ b/cpmpy/transformations/comparison.py @@ -1,10 +1,3 @@ -import copy - -from .flatten_model import get_or_make_var -from ..expressions.core import Comparison, Operator -from ..expressions.utils import is_boolexpr -from ..expressions.variables import _NumVarImpl, _BoolVarImpl - """ Transformations regarding Comparison constraints (originally). Now, it is regarding numeric expressions in general, including nested ones. @@ -22,6 +15,12 @@ - only_numexpr_equality(): transforms `NumExpr IV` (also reified) to `(NumExpr == A) & (A IV)` if not supported """ +import copy +from .flatten_model import get_or_make_var +from ..expressions.core import Comparison, Operator +from ..expressions.utils import is_boolexpr +from ..expressions.variables import _NumVarImpl, _BoolVarImpl + def only_numexpr_equality(constraints, supported=frozenset()): """ transforms `NumExpr IV` to `(NumExpr == A) & (A IV)` if not supported diff --git a/cpmpy/transformations/decompose_global.py b/cpmpy/transformations/decompose_global.py index 79228d0a9..61607a02d 100644 --- a/cpmpy/transformations/decompose_global.py +++ b/cpmpy/transformations/decompose_global.py @@ -1,3 +1,7 @@ +""" + Decompose any global constraint not supported by the solver. +""" + import copy import warnings # for deprecation warning diff --git a/cpmpy/transformations/negation.py b/cpmpy/transformations/negation.py index 607d97581..507d94116 100644 --- a/cpmpy/transformations/negation.py +++ b/cpmpy/transformations/negation.py @@ -1,3 +1,6 @@ +""" + Transformations dealing with negations. +""" import copy import warnings # for deprecation warning import numpy as np diff --git a/cpmpy/transformations/normalize.py b/cpmpy/transformations/normalize.py index b5cf35d17..f7dc900c0 100644 --- a/cpmpy/transformations/normalize.py +++ b/cpmpy/transformations/normalize.py @@ -1,3 +1,7 @@ +""" + Normalizing the constraints given to a CPMpy model. +""" + import copy import numpy as np diff --git a/cpmpy/transformations/reification.py b/cpmpy/transformations/reification.py index 3861398c1..21b41b769 100644 --- a/cpmpy/transformations/reification.py +++ b/cpmpy/transformations/reification.py @@ -1,13 +1,3 @@ -import copy -from ..expressions.core import Operator, Comparison, Expression -from ..expressions.globalconstraints import GlobalConstraint -from ..expressions.globalfunctions import Element -from ..expressions.variables import _BoolVarImpl, _NumVarImpl -from ..expressions.python_builtins import all -from ..expressions.utils import is_any_list -from .flatten_model import flatten_constraint, get_or_make_var -from .negation import recurse_negation - """ Transformations regarding reification constraints. @@ -23,6 +13,15 @@ - only_implies(): transforms all reifications to BV -> BE form - reify_rewrite(): rewrites reifications not supported by a solver to ones that are """ +import copy +from ..expressions.core import Operator, Comparison, Expression +from ..expressions.globalconstraints import GlobalConstraint +from ..expressions.globalfunctions import Element +from ..expressions.variables import _BoolVarImpl, _NumVarImpl +from ..expressions.python_builtins import all +from ..expressions.utils import is_any_list +from .flatten_model import flatten_constraint, get_or_make_var +from .negation import recurse_negation def only_bv_reifies(constraints): newcons = [] diff --git a/cpmpy/transformations/to_cnf.py b/cpmpy/transformations/to_cnf.py index 918d9cc4e..c982b5276 100644 --- a/cpmpy/transformations/to_cnf.py +++ b/cpmpy/transformations/to_cnf.py @@ -1,7 +1,3 @@ -from ..expressions.core import Operator, Comparison -from ..expressions.variables import _BoolVarImpl, NegBoolView -from .reification import only_implies -from .flatten_model import flatten_constraint """ Converts the logical constraints into disjuctions using the tseitin transform, including flattening global constraints that are is_bool() and not in `supported`. @@ -22,6 +18,10 @@ - BE -> BV - BV -> BE """ +from ..expressions.core import Operator, Comparison +from ..expressions.variables import _BoolVarImpl, NegBoolView +from .reification import only_implies +from .flatten_model import flatten_constraint def to_cnf(constraints): """ diff --git a/docs/adding_solver.md b/docs/adding_solver.md index f579f3bea..0fe6f9d9e 100644 --- a/docs/adding_solver.md +++ b/docs/adding_solver.md @@ -12,7 +12,7 @@ Implementing the template consists of the following parts: * `solve()` where you call the solver, get the status and runtime, and reverse-map the variable values after solving * `objective()` if your solver supports optimisation * `transform()` where you call the necessary transformations in `cpmpy.transformations` to transform CPMpy expressions to those that the solver supports - * `__add__()` where you call transform and map the resulting CPMpy expressions that the solver supports, to API function calls on the underlying solver + * `__add__()` where you call transform and map the resulting CPMpy expressions, that the solver supports, to API function calls on the underlying solver * `solveAll()` optionally, if the solver natively supports solution enumeration ## Transformations and posting constraints @@ -29,13 +29,13 @@ So for any solver you wish to add, chances are that most of the transformations ## Stateless transformation functions -Because CPMpy solver interfaces transform and post constraints *eagerly*, they can be used *incremental*, meaning that you can add some constraints, call `solve()` add some more constraints and solve again. If the underlying solver is also incremental, it will reuse knowledge of the previous solve call to speed up this solve call. +Because CPMpy's solver-interfaces transform and post constraints *eagerly*, they can be used *incremental*, meaning that you can add some constraints, call `solve()` add some more constraints and solve again. If the underlying solver is also incremental, it will reuse knowledge of the previous solve call to speed up this solve call. The way that CPMpy succeeds to be an incremental modeling language, is by making all transformation functions *stateless*. Every transformation function is a python *function* that maps a (list of) CPMpy expressions to (a list of) equivalent CPMpy expressions. Transformations are not classes, they do not store state, they do not know (or care) what model a constraint belongs to. They take expressions as input and compute expressions as output. That means they can be called over and over again, and chained in any combination or order. That also makes them modular, and any solver can use any combination of transformations that it needs. We continue to add and improve the transformations, and we are happy to discuss transformations you are missing, or variants of existing transformations that can be refined. -Most transformations do not need any state, they just do a bit of rewriting. Some transformations do, for example in the case of common subexpression elimination. In that case, the solver interface (you who are reading this), should store a dictionary in your solver interface class, and pass that as (optional) argument to the transformation function. The transformation function will read and write to that dictionary as it needs, while still remaining stateless on its own. Each transformation function documents when it supports an optional state dictionary, see all available transformations in `cpmpy/transformations/`. +Most transformations do not need any state, they just do a bit of rewriting. Some transformations do, for example in the case of [Common Subexpression Elimination (CSE)](https://en.wikipedia.org/wiki/Common_subexpression_elimination). In that case, the solver interface (you who are reading this), should store a dictionary in your solver interface class, and pass that as (optional) argument to the transformation function. The transformation function will read and write to that dictionary as it needs, while still remaining stateless on its own. Each transformation function documents when it supports an optional state dictionary, see all available transformations in `cpmpy/transformations/`. ## What is a good Python interface for a solver? @@ -87,7 +87,7 @@ class SolverX { } ``` -If you have such a C++ API, then there exist automatic python packages that can make Python bindings, such as [CPPYY](https://cppyy.readthedocs.io/en/latest/). +If you have such a C++ API, then there exist automatic python packages that can make Python bindings, such as [CPPYY](https://cppyy.readthedocs.io/en/latest/) or [pybind11](https://pybind11.readthedocs.io/en/stable/). We have not done this ourselves yet, so get in touch to share your experience and advice! @@ -101,6 +101,7 @@ As not every solver should support all possible constraints, you can exclude som After posting the constraint, the answer of your solver is checked so you will both be able to monitor when your interface crashes or when a translation to the solver is incorrect. ## Tunable hyperparameters -CPMpy offers a tool for searching the best hyperparameter configuration for a given model on a solver (see [corresponding documentation](solver_parameters.md)). -Solver wanting to support this tool should add the following attributes to their solver interface: `tunable_params` and `default_params` (see [ortools](https://github.com/CPMpy/cpmpy/blob/11ae35b22357ad9b8d6f47317df2c236c3ef5997/cpmpy/solvers/ortools.py#L473) for an example). +CPMpy offers a tool for searching the best hyperparameter configuration for a given model on a solver (see [corresponding documentation](./solver_parameters.md)). +Solvers wanting to support this tool should add the following attributes to their interface: `tunable_params` and `default_params` (see [OR-Tools](https://github.com/CPMpy/cpmpy/blob/11ae35b22357ad9b8d6f47317df2c236c3ef5997/cpmpy/solvers/ortools.py#L473) for an example). + diff --git a/docs/api/expressions/globalfunctions.rst b/docs/api/expressions/globalfunctions.rst new file mode 100644 index 000000000..8240d85b0 --- /dev/null +++ b/docs/api/expressions/globalfunctions.rst @@ -0,0 +1,7 @@ +Global Functions (:mod:`cpmpy.expressions.globalfunctions`) +=================================================== + +.. automodule:: cpmpy.expressions.globalfunctions + :members: + :undoc-members: + :inherited-members: diff --git a/docs/api/solvers/choco.rst b/docs/api/solvers/choco.rst new file mode 100644 index 000000000..66f739ed8 --- /dev/null +++ b/docs/api/solvers/choco.rst @@ -0,0 +1,7 @@ +CPMpy exact interface (:mod:`cpmpy.solvers.choco`) +===================================================== + +.. automodule:: cpmpy.solvers.choco + :members: + :undoc-members: + :inherited-members: \ No newline at end of file diff --git a/docs/api/tools.rst b/docs/api/tools.rst new file mode 100644 index 000000000..022761aa1 --- /dev/null +++ b/docs/api/tools.rst @@ -0,0 +1,6 @@ +Tools (:mod:`cpmpy.tools`) +======================================== + +.. automodule:: cpmpy.tools + :members: + :inherited-members: \ No newline at end of file diff --git a/docs/api/tools/dimacs.rst b/docs/api/tools/dimacs.rst new file mode 100644 index 000000000..8b785778c --- /dev/null +++ b/docs/api/tools/dimacs.rst @@ -0,0 +1,7 @@ +DIMACS (:mod:`cpmpy.tools.dimacs`) +===================================================== + +.. automodule:: cpmpy.tools.dimacs + :members: + :undoc-members: + :inherited-members: \ No newline at end of file diff --git a/docs/api/tools/explain.rst b/docs/api/tools/explain.rst new file mode 100644 index 000000000..22f15dd12 --- /dev/null +++ b/docs/api/tools/explain.rst @@ -0,0 +1,33 @@ +Explanation tools (:mod:`cpmpy.tools.explain`) +===================================================== + +.. automodule:: cpmpy.tools.explain + :members: + :undoc-members: + :inherited-members: + +.. include:: ./explain/mus.rst +.. include:: ./explain/mss.rst +.. include:: ./explain/mcs.rst +.. include:: ./explain/utils.rst + +.. .. automodule:: cpmpy.tools.explain.mcs +.. :title: +.. :members: +.. :undoc-members: +.. :inherited-members: + +.. .. automodule:: cpmpy.tools.explain.mss +.. :members: +.. :undoc-members: +.. :inherited-members: + +.. .. automodule:: cpmpy.tools.explain.mus +.. :members: +.. :undoc-members: +.. :inherited-members: + +.. .. automodule:: cpmpy.tools.explain.utils +.. :members: +.. :undoc-members: +.. :inherited-members: \ No newline at end of file diff --git a/docs/api/tools/explain/mcs.rst b/docs/api/tools/explain/mcs.rst new file mode 100644 index 000000000..f098d0dc1 --- /dev/null +++ b/docs/api/tools/explain/mcs.rst @@ -0,0 +1,7 @@ +MCS (:mod:`cpmpy.tools.explain.mcs`) +===================================================== + +.. automodule:: cpmpy.tools.explain.mcs + :members: + :undoc-members: + :inherited-members: \ No newline at end of file diff --git a/docs/api/tools/explain/mss.rst b/docs/api/tools/explain/mss.rst new file mode 100644 index 000000000..cc77290e2 --- /dev/null +++ b/docs/api/tools/explain/mss.rst @@ -0,0 +1,7 @@ +MSS (:mod:`cpmpy.tools.explain.mss`) +===================================================== + +.. automodule:: cpmpy.tools.explain.mss + :members: + :undoc-members: + :inherited-members: \ No newline at end of file diff --git a/docs/api/tools/explain/mus.rst b/docs/api/tools/explain/mus.rst new file mode 100644 index 000000000..8fdcd532c --- /dev/null +++ b/docs/api/tools/explain/mus.rst @@ -0,0 +1,7 @@ +MUS (:mod:`cpmpy.tools.explain.mus`) +===================================================== + +.. automodule:: cpmpy.tools.explain.mus + :members: + :undoc-members: + :inherited-members: \ No newline at end of file diff --git a/docs/api/tools/explain/utils.rst b/docs/api/tools/explain/utils.rst new file mode 100644 index 000000000..a4a44657f --- /dev/null +++ b/docs/api/tools/explain/utils.rst @@ -0,0 +1,7 @@ +Utils (:mod:`cpmpy.tools.explain.utils`) +===================================================== + +.. automodule:: cpmpy.tools.explain.utils + :members: + :undoc-members: + :inherited-members: \ No newline at end of file diff --git a/docs/api/tools/maximal_propagate.rst b/docs/api/tools/maximal_propagate.rst new file mode 100644 index 000000000..9fe5dad3a --- /dev/null +++ b/docs/api/tools/maximal_propagate.rst @@ -0,0 +1,7 @@ +Maximal Propagate (:mod:`cpmpy.tools.maximal_propagate`) +===================================================== + +.. automodule:: cpmpy.tools.maximal_propagate + :members: + :undoc-members: + :inherited-members: \ No newline at end of file diff --git a/docs/api/tools/tune_solver.rst b/docs/api/tools/tune_solver.rst new file mode 100644 index 000000000..503b3eb36 --- /dev/null +++ b/docs/api/tools/tune_solver.rst @@ -0,0 +1,7 @@ +Solver Parameter Tuning (:mod:`cpmpy.tools.tune_solver`) +===================================================== + +.. automodule:: cpmpy.tools.tune_solver + :members: + :undoc-members: + :inherited-members: \ No newline at end of file diff --git a/docs/api/transformations.rst b/docs/api/transformations.rst index 29174f126..266ea5802 100644 --- a/docs/api/transformations.rst +++ b/docs/api/transformations.rst @@ -3,4 +3,15 @@ Expression transformations (:mod:`cpmpy.transformations`) .. automodule:: cpmpy.transformations :members: + :undoc-members: :inherited-members: + +.. .. include:: ./transformations/comparison.rst +.. .. include:: ./transformations/decompose_global.rst +.. .. include:: ./transformations/flatten_model.rst +.. .. include:: ./transformations/get_variables.rst +.. .. include:: ./transformations/linearize.rst +.. .. include:: ./transformations/negation.rst +.. .. include:: ./transformations/normalize.rst +.. .. include:: ./transformations/reification.rst +.. .. include:: ./transformations/to_cnf.rst \ No newline at end of file diff --git a/docs/api/transformations/comparison.rst b/docs/api/transformations/comparison.rst new file mode 100644 index 000000000..a534380e7 --- /dev/null +++ b/docs/api/transformations/comparison.rst @@ -0,0 +1,9 @@ +.. orphan:: + +Comparison (:mod:`cpmpy.transformations.comparison`) +======================================================================== + +.. automodule:: cpmpy.transformations.comparison + :members: + :undoc-members: + :inherited-members: \ No newline at end of file diff --git a/docs/api/transformations/decompose_global.rst b/docs/api/transformations/decompose_global.rst new file mode 100644 index 000000000..e8f6f9973 --- /dev/null +++ b/docs/api/transformations/decompose_global.rst @@ -0,0 +1,7 @@ +Decompose Global (:mod:`cpmpy.transformations.decompose_global`) +======================================================================== + +.. automodule:: cpmpy.transformations.decompose_global + :members: + :undoc-members: + :inherited-members: \ No newline at end of file diff --git a/docs/api/transformations/negation.rst b/docs/api/transformations/negation.rst new file mode 100644 index 000000000..9496ad5ef --- /dev/null +++ b/docs/api/transformations/negation.rst @@ -0,0 +1,7 @@ +Negation (:mod:`cpmpy.transformations.negation`) +======================================================================== + +.. automodule:: cpmpy.transformations.negation + :members: + :undoc-members: + :inherited-members: \ No newline at end of file diff --git a/docs/api/transformations/normalize.rst b/docs/api/transformations/normalize.rst new file mode 100644 index 000000000..1c5f0dfc1 --- /dev/null +++ b/docs/api/transformations/normalize.rst @@ -0,0 +1,7 @@ +Normalize (:mod:`cpmpy.transformations.normalize`) +======================================================================== + +.. automodule:: cpmpy.transformations.normalize + :members: + :undoc-members: + :inherited-members: \ No newline at end of file diff --git a/docs/conf.py b/docs/conf.py index 7f5b1daa6..99ea742ec 100644 --- a/docs/conf.py +++ b/docs/conf.py @@ -42,12 +42,28 @@ 'sphinx.ext.autosummary', 'sphinx.ext.mathjax', 'sphinx.ext.viewcode', - 'm2r2', + 'myst_parser', 'sphinx_rtd_theme', 'sphinx_automodapi.automodapi', 'sphinx_automodapi.smart_resolver' ] +myst_enable_extensions = [ + "amsmath", + "attrs_inline", + "colon_fence", + "deflist", + "dollarmath", + "fieldlist", + "html_admonition", + "html_image", + "replacements", + "smartquotes", + "strikethrough", + "substitution", + "tasklist", +] + numpydoc_show_class_members = False numpydoc_show_inherited_class_members = False diff --git a/docs/developers.md b/docs/developers.md index f8d4db9af..c3ee62e25 100644 --- a/docs/developers.md +++ b/docs/developers.md @@ -34,27 +34,28 @@ python -m pytest tests/test_solvers.py ## Code structure - * _tests/_ contains the tests - * _docs/_ contains the docs. Any change there is automatically updated, with some delay, on [https://cpmpy.readthedocs.io/](https://cpmpy.readthedocs.io/) - * _examples/_ our examples, always happy to include more - * _cpmpy/_ the python module that you install when doing `pip install cpmpy` + * _tests/_ : contains the tests + * _docs/_ : contains the docs. Any change there is automatically updated, with some delay, on [https://cpmpy.readthedocs.io/](https://cpmpy.readthedocs.io/) + * _examples/_ : our examples, always happy to include more + * _cpmpy/_ : the python module that you install when doing `pip install cpmpy` The module is structured as such: - * _model.py_ contains the omnipresent `Model()` container - * _expressions/_ Classes and functions that represent and create expressions (constraints and objectives) - * _solvers/_ CPMpy interfaces to (the Python API interface of) solvers - * _transformations/_ Methods to transform CPMpy expressions in other CPMpy expressions - * _tools/_ Set of independent tools that users might appreciate. + * _model.py_ : contains the omnipresent `Model()` container + * _exceptions.py_ : contains a collection of CPMpy specific exceptions + * _expressions/_ : Classes and functions that represent and create expressions (constraints and objectives) + * _solvers/_ : CPMpy interfaces to (the Python API interface of) solvers + * _transformations/_ : Methods to transform CPMpy expressions into other CPMpy expressions + * _tools/_ : Set of independent tools that users might appreciate. -The typical flow in which these submodules are used when using CPMpy is: the user creates _expressions_ which they put into a _model_ object. This is then given to a _solver_ object to solve, which will first _transform_ the expressions into expressions that it supports, which it then posts to the Python API interface of that particular solver. +The typical flow in which these submodules are used when programming with CPMpy is: the user creates _expressions_ which they put into a _model_ object. This is then given to a _solver_ object to solve, which will first _transform_ the original expressions into expressions that it supports, which it then posts to the Python API interface of that particular solver. Tools are not part of the core of CPMpy. They are additional tools that _use_ CPMpy, e.g. for debugging, parameter tuning etc. -## Github practices +## GitHub practices -When filing a bug, please add a small case that allows us to reproduce it. If the testcase is confidential, mail Tias directly. +When filing a bug, please add a small case that allows us to reproduce it. If the testcase is confidential, mail [Tias](mailto:tias.guns@kuleuven.be) directly. Only documentation changes can be directly applied on the master branch. All other changes should be submitted as a pull request. diff --git a/docs/docs_todo.md b/docs/docs_todo.md new file mode 100644 index 000000000..0fcba6b5f --- /dev/null +++ b/docs/docs_todo.md @@ -0,0 +1,37 @@ +# TODO + +A list of things in CPMpy's docs which need fixed / which are optional improvements. + +A lot of proof-reading is still needed to catch all formatting mistakes (especially in the API section, as taken for the code's docstrings) + + +- [ ] Outdated copyright + - whilst updated on the repo, ReadTheDocs still gives 2021 as copyright year + +- [ ] Mention Exact + - In many places where solvers get listed, Exact is not inluded (especially for things that make Exact stand out; e.g. unsat core extraction) + +- [ ] Solver overview table + - available solvers and their supported features + e.g. incrementality, core exctraction, proof logging, parallelisation, ... + +- [ ] Overview of available CPMpy tools +- [ ] "frietkot" link in ocus is down +- [ ] docs already refer to cse in "how to add a solver" + - CSE has not been added to master yet + +- [ ] Decision variables shape + - decision variable docs say that all variables are arrays and thus have the shape attribute + -> only NDVarArrays + +- [ ] Sphinx's python autodoc annotations: + - see Exact's interface + - [The Python Domain — Sphinx documentation (sphinx-doc.org)](https://www.sphinx-doc.org/en/master/usage/domains/python.html#directive-py-method) + +- [ ] Gurobi GRB_ENV subsolver + document this + +- [ ] Jupyter notebooks + +- [ ] Use of "warning" boxes & others + diff --git a/docs/how_to_debug.md b/docs/how_to_debug.md index 5c9f5d253..40ed0d418 100644 --- a/docs/how_to_debug.md +++ b/docs/how_to_debug.md @@ -7,7 +7,7 @@ The bug can be situated in one of three layers: - the CPMpy library - the solver -coincidentally, they are ordered from most likely to least likely. So let's start at the bottom. +Coincidentally, they are ordered from most likely to least likely. So let's start at the bottom. If you don't have a bug yet, but are curious, here is some general advise from expert modeller [Håkan Kjellerstrand](http://www.hakank.org/): - Test the model early and often. This makes it easier to detect problems in the model. @@ -21,22 +21,23 @@ If you get an error and have difficulty understanding it, try searching on the i If you don't find it, or if the solver runs fine and without error, but you don't get the answer you expect; then try swapping out the solver for another solver and see what gives... -Replace `model.solve()` by `model.solve(solver='minizinc')` for example. You do need to install MiniZinc and minizinc-python first though. +Replace `model.solve()` by `model.solve(solver='minizinc')` for example. You do need to install MiniZinc and minizinc-python first though. Take a look at [the solver API interface](./api/solvers.rst) for the install instructions. Either you have the same output, and it is not the solver's fault, or you have a different output and you actually found one of these rare solver bugs. Report on the bugtracker of the solver, or on the CPMpy github page where we will help you file a bug 'upstream' (or maybe even work around it in CPMpy). ## Debugging a modeling error -You get an error when you create an expression? Then you are probably writing it wrongly. Check the documentation and the running examples for similar examples of what you wish to express. +You get an error when you create an expression? Then you are probably writing it wrongly. Check the documentation and the running examples for similar instances of what you wish to express. Here are a few quirks in Python/CPMpy: - when using `&` and `|`, make sure to always put the subexpressions in brackets. E.g. `(x == 1) & (y == 0)` instead of `x == 1 & y == 0`. The latter wont work, because Python will unfortunately think you meant `x == (1 & (y == 0))`. - you can write `vars[other_var]` but you can't write `non_var_list[a_var]`. That is because the `vars` list knows CPMpy, and the `non_var_list` does not. Wrap it: `non_var_list = cpm_array(non_var_list)` first, or write `Element(non_var_list, a_var)` instead. - only write `sum(v)` on lists, don't write it if `v` is a matrix or tensor, as you will get a list in response. Instead, use NumPy's `v.sum()` instead. + - when providing names for decision variables, make shure that they are unique. Many solvers depend on this uniqueness and you will encounter strange (and hard to debug) behaviour if you don't enforce this. Try printing the expression `print(e)` or subexpressions, and check that the output matches what you wish to express. Decompose the expression and try printing the individual components and their piecewice composition to see what works and when it starts to break. -If you don't find it, report it on the CPMpy github Issues page and we'll help you (and maybe even extend the above list of quirks). +If you don't find it, report it on the CPMpy GitHub Issues page and we'll help you (and maybe even extend the above list of quirks). ## Debugging a `solve()` error @@ -52,9 +53,9 @@ for c in model.constraints: Model(c).solve() ``` -The last constraint printed before the exception is the curlpit... Please report on Github. We want to catch corner cases in CPMpy, even if it is a solver limitation, so please report on the CPMpy github Issues page. +The last constraint printed before the exception is the curlpit... Please report on GitHub. We want to catch corner cases in CPMpy, even if it is a solver limitation, so please report on the CPMpy GitHub Issues page. -Or maybe, you got one of CPMpy's NotImplementedErrors. Share your use case with us on Github and we will implement it. Or implemented it yourself first, that is also very welcome ; ) +Or maybe, you got one of CPMpy's NotImplementedErrors. Share your use case with us on GitHub and we will implement it. Or implemented it yourself first, that is also very welcome ; ) ## Debugging an UNSATisfiable model @@ -62,7 +63,7 @@ First, print the model: ```print(model)``` -and check that the output matches what you want to express. Do you see anything unusual? Start there, see why the expression is not what you intended to express, as described in 'Debugging a modeling error'. +and check that the output matches what you want to express. Do you see anything unusual? Start there, see why the expression is not what you intended to express, as described in [Debugging a modeling error](#debugging-a-modeling-error). If that does not help, try printing the 'transformed' **constraints**, the way that the solver actually sees them, including decompositions and rewrites: @@ -95,7 +96,7 @@ print(f"Optimizing {obj_var} subject to", s.transform(obj_expr)) ### Automatically minimising the UNSAT program If the above is unwieldy because your constraint problem is too large, then consider automatically reducing it to a 'Minimal Unsatisfiable Subset' (MUS). -This is now part of our standard tools, that you can use as follows: +This is now part of our [standard tools](./api/tools.rst), that you can use as follows: ```python from cpmpy.tools import mus @@ -113,7 +114,7 @@ unsat_cons = mus(model.constraints) With this smaller set of constraints, repeat the visual inspection steps above. -(Note that for an UNSAT problem there can be many MUSes, the `examples/advanced/` folder has the MARCO algorithm that can enumerate all MSS/MUSes.) +(Note that for an UNSAT problem there can be many MUSes, the `examples/advanced/` [folder](https://github.com/CPMpy/cpmpy/tree/master/examples/advanced) has the [MARCO algorithm](https://github.com/CPMpy/cpmpy/blob/master/examples/advanced/marco_musmss_enumeration.py) that can enumerate all MSS/MUSes.) ### Correcting an UNSAT program @@ -142,6 +143,8 @@ sat_cons = mss(model.constraints) # x[0] or x[1], x[2] -> x[1], ~x[0] cons_to_remove = (mcs(model.constraints)) # x[0] ``` +More information about these tools can be found in [their API documentation](./api/tools/explain.rst). + ## Debugging a satisfiable model, that does not contain an expected solution We will ignore the (possible) objective function here and focus on the feasibility part. @@ -158,5 +161,5 @@ This one is most annoying... Double check the printing of the model for oddities Try generating an explanation sequence for the solution... this requires a satisfaction problem, so remove the objective function or add a constraint that constraints the objective function to the value attained by the impossible solution. -As to generating the explanation sequence, check out our advanced example on [stepwise OCUS explanations](https://github.com/CPMpy/cpmpy/blob/master/examples/advanced/ocus_explanations.py) +As to generating the explanation sequence, check out our advanced example on [stepwise OCUS explanations](https://github.com/CPMpy/cpmpy/blob/master/examples/advanced/ocus_explanations.py). diff --git a/docs/index.rst b/docs/index.rst index 3d17e5df1..b26280641 100644 --- a/docs/index.rst +++ b/docs/index.rst @@ -71,4 +71,5 @@ Are you a solver developer? We are keen to integrate solvers that have a python api/expressions api/model api/solvers - api/transformations \ No newline at end of file + api/transformations + api/tools \ No newline at end of file diff --git a/docs/modeling.md b/docs/modeling.md index 3fb1fe16a..0bdf70ed6 100644 --- a/docs/modeling.md +++ b/docs/modeling.md @@ -4,26 +4,28 @@ This page explains and demonstrates how to use CPMpy to model and solve combinat ## Installation -Installation is available through the `pip` python package manager. This will also install and use `ortools` as default solver: +Installation is available through the `pip` Python package manager. This will also install and use `ortools` as default solver (see how to use alternative solvers [here](#selecting-a-solver)): ```commandline pip install cpmpy ``` -See [installation instructions](installation_instructions.html) for more details. +See [installation instructions](./installation_instructions.rst) for more details. ## Using the library -To conveniently use CPMpy in your python project, include it as follows: +To conveniently use CPMpy in your Python project, include it as follows: ```python from cpmpy import * ``` -This will overload the built-in `any()`, `all()`, `min()`, `max()`, `sum()` functions, such that they create CPMpy expressions when used on decision variables (see below). This convenience comes at the cost of some overhead for all uses of these functions in your code. +This will overload the built-in `any()`, `all()`, `min()`, `max()`, `sum()` functions, such that they create CPMpy expressions when used on decision variables (see below). This convenience comes at the cost of some overhead for all uses of these functions in your code (even when no CPMpy decision variables are involved). -You can also import it as a package, which does not overload the python built-ins: +You can also import it as a package, which does not overload the Python built-ins: ```python import cpmpy as cp ``` +The build-in operators can now be accessed through the package (for example `cp.any()`) without overloading Python's defaults. + We will use the latter in this document. ## Decision variables @@ -35,19 +37,19 @@ CPMpy supports discrete decision variables, namely Boolean and integer decision ```python import cpmpy as cp -b = cp.boolvar(name="b") -x = cp.intvar(1,10, name="x") +b = cp.boolvar(name="b") # a Boolean decision variable +x = cp.intvar(1,10, name="x") # an Integer decision variable ``` -Decision variables have a **domain**, a set of allowed values. For Boolean variables this is implicitly the values 'False' and 'True'. For Integer decision variables, you have to specify the lower-bound and upper-bound (`1` and `10` respectively above). +Decision variables have a **domain**, a set of allowed values. For Boolean variables this is implicitly the values 'False' and 'True'. For Integer decision variables, you have to specify the lower-bound and upper-bound (`1` and `10` respectively in the above example). If you want a **sparse domain**, containing only a few values, you can either define a suitable lower/upper bound and then forbid specific values, e.g. `x != 3, x != 5, x != 7`; or you can use the shorthand *InDomain* global constraint: `InDomain(x, [1,2,4,6,8,9])`. -Decision variables have a **unique name**. You can set it yourself, otherwise a unique name will automatically be assigned to it. If you print `print(b, x)` decision variables, it will print the name. Did we already say the name must be unique? Many solvers use the name as unique identifier, and it is near-impossible to debug with non-uniquely named variables. +Decision variables have a **unique name**. You can set it yourself, otherwise a unique name will automatically be assigned. If you print decision variables (`print(b)` or `print(x)`), it will display the name. Did we already say the name must be unique? Many solvers use the name as unique identifier, and it is near-impossible to debug with non-uniquely named decision variables. -A solver will set the **value** of the decision variables for which it solved, if it can find a solution. You can retrieve it with `v.value()`. Variables are not tied to a solver, so you can use the same variable in multiple models and solvers. When a solve call finishes, it will overwrite the value of all its decision variables. +A solver will set the **value** of the decision variables for which it solved, if it can find a solution. You can retrieve it with `v.value()`. Variables are not tied to a solver, so you can use the same variable across multiple models and solvers. When a solve call finishes, it will overwrite the value of all its decision variables. Before solving, this value will be `None`. After solving it has either taken a boolean or integer value, or it is still None. For example when the solver didn't find any solution or when the decision variable was never used in the model, i.e. never appeared in a constraint or the objective function (a stale decision variable). -Finally, by providing a **shape** you automatically create a **numpy n-dimensional array** of decision variables. They automatically get their index appended to their name to ensure it is unique: +Finally, by providing a **shape** you automatically create a **numpy n-dimensional array** of decision variables. These variables automatically get their index appended to their name (the name is provided on the array-level) as to ensure its uniqueness: ```python import cpmpy as cp @@ -59,17 +61,19 @@ x = cp.intvar(1,10, shape=(2,2), name="x") print(x) # [[x[0,0] x[0,1]] # [x[1,0] x[1,1]]] ``` -You can also call `v.value()` on these n-dimensional arrays, which will return an n-dimensional **numpy** array of values. And you can do vectorized operations and comparisons, like in regular numpy. As we will see below, this is very convenient and avoids having to write out many loops. It also makes it compatible with many existing scientific python tools, including machine learning and visualisation libraries, so a lot less glue code to write. +Similar to individual decision variables, you can call `v.value()` on these n-dimensional arrays. This will return an n-dimensional **numpy** array of values, one value for each of the included decision variables. + +Since the arrays of decision variables are based on numpy, you can do **vectorized operations** and **comparisons** on them. As we will see below, this is very convenient and avoids having to write out many loops. It also makes it compatible with many existing scientific Python tools, including machine learning and visualisation libraries. A lot less glue code will need to be written! -See [the API documentation on variables](api/expressions/variables.html) for more detailed information. +See [the API documentation on variables](./api/expressions/variables.rst) for more detailed information. Note that decision variables are not tied to a model. You can use the same variable in different models; its value() will be the one of the last succesful solve call. ## Creating a model -A **model** is a collection of constraints over decision variables, optionally with an objective function. It represents a problem for which a solution must be found, e.g. by a solver. A solution is an assignment to the decision variables, such that each of the constraints is satisfied. +A **model** is a collection of constraints over decision variables, optionally with an objective function. It represents a problem for which a solution must be found, e.g. through the use of a solver. A solution is an assignment of values to the decision variables, such that the values lie within their respective variables' domain and such that each of the constraints is satisfied. -In CPMpy, the `Model()` object is a simple container that stores a list of CPMpy expressions representing constraints. It can also store a CPMpy expression representing an objective function that must be minimized or maximized. Constraints are added in the constructor, or using the built-in `+=` addition operator that corresponds to calling the `__add__()` function. +In CPMpy, the `Model()` object is a simple container that stores a list of CPMpy expressions representing constraints. In the case of an optimisation problem, it can also store a CPMpy expression representing an objective function that must be minimized or maximized. Constraints are added in the constructor, or using the built-in `+=` addition operator that corresponds to calling the `__add__()` function. Here is an example, where we explain how to express constraints in the next section: @@ -96,6 +100,8 @@ print(m) # pretty printing of the model, very useful for debugging ``` The `Model()` object has a number of other helpful functions, such as `to_file()` to store the model and `copy()` for creating a copy. +See [the API documentation on models](./api/model.rst) for more detailed information. + ## Expressing constraints A constraint is a relation between decision variables that restricts what values these variables can take. @@ -162,10 +168,10 @@ import cpmpy as cp a,b,c = cp.boolvar(shape=3) m = cp.Model( - a.implies(b), - b.implies(a), - a.implies(~c), - (~c).implies(a) + a.implies(b), # a -> b + b.implies(a), # b -> a + a.implies(~c), # a -> (~c) + (~c).implies(a) # (~c) -> a ) ``` For reverse implication, you switch the arguments yourself; it is difficult to read reverse implications out loud anyway. And as before, always use brackets around subexpressions to avoid surprises! @@ -174,7 +180,7 @@ For reverse implication, you switch the arguments yourself; it is difficult to r ### Simple comparison constraints -We overload Pythons comparison operators: `==, !=, <, <=, >, >=`. Comparisons are allowed between any CPMpy expressions as well as Boolean and integer constants. +We overload Python's comparison operators: `==, !=, <, <=, >, >=`. Comparisons are allowed between any CPMpy expressions as well as Boolean and integer constants. On a technical note, we treat Booleans as a subclass of integer expressions. This means that a Boolean (output) expression can be used anywhere a numeric expression can be used, where `True` is treated as `1` and `False` as `0`. But the inverse is not true: integers can NOT be used with Boolean operators, even when you intialise their domain to (0,1) they are still not Boolean: @@ -226,9 +232,9 @@ m = cp.Model( ### Arithmetic constraints -We overload Python's built-in arithmetic operators `+,-,*,//,%`. These can be used to built arbitrarily nested numeric expressions, which can then be turned into a constraint by adding a comparison to it. +We overload Python's built-in arithmetic operators `+,-,*,//,%`. These can be used to build arbitrarily nested numeric expressions, which can then be turned into a constraint by adding a comparison to it. -We also overwrite the built-in functions `abs(),sum(),min(),max()` which can be used to created numeric expressions. Some examples: +We also overwrite the built-in functions `abs(),sum(),min(),max()` which can be used for creating numeric expressions. Some examples: ```python import cpmpy as cp @@ -258,7 +264,7 @@ m = cp.Model( ) ``` -Note that because of our overloading of `+,-,*,//` some numpy functions like `np.sum(some_array)` will also create a CPMpy expression when used on CPMpy decision variables. However, this is not guaranteed, and other functions like `np.max(some_array)` will not. To **avoid surprises**, you should hence always take care to call the CPMpy functions `cp.sum(), `cp.max()` etc. We did overload `some_cpm_array.sum()` and `.min()/.max()` (including the axis= argument), so these are safe to use. +Note that because of our overloading of `+,-,*,//` some numpy functions like `np.sum(some_array)` will also create a CPMpy expression when used on CPMpy decision variables. However, this is not guaranteed, and other functions like `np.max(some_array)` will not. To **avoid surprises**, you should hence always take care to call the CPMpy functions `cp.sum()`, `cp.max()` etc. We did overload `some_cpm_array.sum()` and `.min()`/`.max()` (including the axis= argument), so these are safe to use. ### Global constraints @@ -269,15 +275,17 @@ In constraint solving, a global constraint is a function that expresses a relati A good example is the `AllDifferent()` global constraint that ensures all its arguments have distinct values. `AllDifferent(x,y,z)` can be decomposed into `[x!=y, x!=z, y!=z]`. For AllDifferent, the decomposition consists of _n*(n-1)_ pairwise inequalities, which are simpler constraints that most solvers support. -However, a solver that has specialised datastructures for this constraint specifically does not need to create the decomposition. Furthermore, for AllDifferent solvers can implement specialised algorithms that can propagate strictly stronger than the decomposed constraints can. +However, a solver that has specialised datastructures for this constraint specifically does not need to create the decomposition. Furthermore, solvers can implement specialised algorithms that can propagate strictly stronger than the decomposed constraints can. #### Global constraints -A non-exhaustive list of global constraints that are available in CPMpy is: `Xor(), AllDifferent(), AllDifferentExcept0(), Table(), Circuit(), Cumulative(), GlobalCardinalityCount()`. +Many global constraints are available in CPMpy. Some include `Xor(), AllDifferent(), AllDifferentExcept0(), Table(), Circuit(), Cumulative(), GlobalCardinalityCount()`. + +For a complete list of global constraints, their meaning and more information on how to define your own, see [the API documentation on global constraints](./api/expressions/globalconstraints.rst). -For their meaning and more information on how to define your own global constraints, see [the API documentation on global constraints](api/expressions/globalconstraints.html). Global constraints can also be reified (e.g. used in an implication or equality constraint). +Global constraints can also be reified (e.g. used in an implication or equality constraint). CPMpy will automatically decompose them if needed. If you want to see the decomposition yourself, you can call the `decompose()` function on them. @@ -287,24 +295,24 @@ x = cp.intvar(1,4, shape=4, name="x") b = cp.boolvar() cp.Model( cp.AllDifferent(x), - cp.AllDifferent(x).decompose(), # equivalent: [(x[0]) != (x[1]), (x[0]) != (x[2]), ... + cp.AllDifferent(x).decompose()[0], # equivalent: [(x[0]) != (x[1]), (x[0]) != (x[2]), ... b.implies(cp.AllDifferent(x)), cp.Xor(b, cp.AllDifferent(x)), # etc... ) ``` -`decompose()` returns two arguments, one that represents the constraints and an optional one that defines any new variables needed. This is technical, but important to make negation work, if you want to know more check the [the API documentation on global constraints](api/expressions/globalconstraints.html). +`decompose()` returns two arguments, one that represents the constraints and another that defines any newly created decision variables during the decomposition process. This is technical, but important to make negation work, if you want to know more check the [the API documentation on global constraints](./api/expressions/globalconstraints.rst). -#### Numeric global constraints +#### Global functions Coming back to the Python-builtin functions `min(),max(),abs()`, these are a bit special because they have a numeric return type. In fact, constraint solvers typically implement a global constraint `MinimumEq(args, var)` that represents `min(args) == var`, so it combines a numeric function with a comparison, where it will ensure that the bounds of the expressions on both sides satisfy the comparison relation. However, CPMpy also wishes to support the expressions `min(xs) > v` as well as `v + min(xs) != 4` and other nested expressions. -In CPMpy we do this by instantiating min/max/abs as **numeric global constraints**. E.g. `min([x,y,z])` becomes `Minimum([x,y,z])` which inherits from `GlobalFunction` because it has a numeric return type. Our library will transform the constraint model, including arbitrarly nested expressions, such that the numeric global constraint is used in a comparison with a variable. Then, the solver will either support it, or we will call `decompose_comparison()` on the numeric global constraint, which will decompose e.g. `min(xs) == v`. +In CPMpy we do this by instantiating min/max/abs as **global functions**. E.g. `min([x,y,z])` becomes `Minimum([x,y,z])` which inherits from `GlobalFunction` because it has a numeric return type. Our library will transform the constraint model, including arbitrarly nested expressions, such that the global function is used within a comparison with a variable. Then, the solver will either support it, or we will call `decompose_comparison()` ([link](./api/expressions/globalfunctions.rst#cpmpy.expressions.globalfunctions.Abs.decompose_comparison)) on the global function. A non-exhaustive list of **numeric global constraints** that are available in CPMpy is: `Minimum(), Maximum(), Count(), Element()`. -For their meaning and more information on how to define your own global constraints, see [the API documentation on global functions](api/expressions/globalfunctions.html). +For their meaning and more information on how to define your own global functions, see [the API documentation on global functions](./api/expressions/globalfunctions.rst). ```python import cpmpy as cp @@ -322,7 +330,7 @@ print(s.transform(cp.min(x) + cp.max(x) - 5 > 2*cp.Count(x, 2))) ``` -#### The Element numeric global constraint +#### The Element global function The `Element(Arr,Idx)` global function enforces that the result equals `Arr[Idx]` with `Arr` an array of constants or variables (the first argument) and `Idx` an integer decision variable, representing the index into the array. @@ -341,7 +349,7 @@ print(f"arr: {arr.value()}, idx: {idx.value()}, val: {arr[idx].value()}") # example output -- arr: [2 1 3 4], idx: 0, val: 2 ``` -The `arr[idx]` works because `arr` is a CPMpy `NDVarArray()` and we overloaded the `__getitem__()` python function. It even supports multi-dimensional access, e.g. `arr[idx1,idx2]`. +The `arr[idx]` works because `arr` is a CPMpy `NDVarArray()` and we overloaded the `__getitem__()` Python function. It even supports multi-dimensional access, e.g. `arr[idx1,idx2]`. This does not work on NumPy arrays though, as they don't know CPMpy. So you have to **wrap the array** in our `cpm_array()` or call `Element()` directly: @@ -371,7 +379,7 @@ print(f"arr: {arr.value()}, idx: {idx.value()}, val: {arr[idx].value()}") ## Objective functions -If a model has no objective function specified, then it is a satisfaction problem: the goal is to find out whether a solution, any solution, exists. When an objective function is added, this function needs to be minimized or maximized. +If a model has no objective function specified, then it represents a satisfaction problem: the goal is to find out whether a solution, any solution, exists. When an objective function is added, this function needs to be minimized or maximized. Any CPMpy expression can be added as objective function. Solvers are especially good in optimizing linear functions or the minimum/maximum of a set of expressions. Other (non-linear) expressions are supported too, just give it a try. @@ -433,21 +441,29 @@ n = m.solveAll() print("Nr of solutions:", n) # Nr of solutions: 6 ``` -When using `solveAll()`, a solver will use an optimized native implementation behind the scenes when that exists. +When using `solveAll()`, a solver will use an optimized native implementation behind the scenes when that exists. Otherwise it will be emulated with an iterative approach, resulting in a performance impact. -It has a `display=...` argument that can be used to display expressions or as a callback, as well as the `solution_limit=...` argument to set a solution limit. It also accepts any named argument, like `time_limit=...`, that the underlying solver accepts. +It has a `display=...` argument that can be used to display expressions (provide a list of expressions to be evaluated) or as a more generic callback (provide a function), both to be evaluated for each found solution. +It has a `solution_limit=...` argument to set a limit on the number of solutions to solve for. +It also accepts any named argument, like `time_limit=...`, that the underlying solver accepts. For more information about the available arguments, look at [the solver API documentation](./api/solvers.rst) for the solver in question. ```python +# Using list of expressions n = m.solveAll(display=[x,cp.sum(x)], solution_limit=3) # [array([1, 0]), 1] # [array([2, 0]), 2] # [array([3, 0]), 3] + +# Using callback function +n = m.solveAll(display=lambda: print([x.value(), cp.sum(x).value()]), solution_limit=3) +# ... ``` +(Note that the Exact solver, unlike other solvers, takes most of its arguments at construction time.) -There is much more to say on enumerating solutions and the use of callbacks or blocking clauses. See the [the detailed documentation on finding multiple solutions](multiple_solutions.html). +There is much more to say on enumerating solutions and the use of callbacks or blocking clauses. See the [the detailed documentation on finding multiple solutions](./multiple_solutions.md). ## Debugging a model -If the solver is complaining about your model, then a good place to start debugging is to **print** the model you have created, or the individual constraints. If they look fine (e.g. no integers, or shorter or longer expressions then what you intended) and you don't know which constraint specifically is causing the error, then you can feed the constraints incrementally to the solver you are using: +If the solver is complaining about your model, then a good place to start debugging is to **print** the model (or individual constraints) that you have created. If they look fine (e.g. no integers, or shorter or longer expressions then what you intended) and you don't know which constraint specifically is causing the error, then you can feed the constraints incrementally to the solver you are using: ```python import cpmpy as cp @@ -460,18 +476,19 @@ m = cp.Model(cons) # any model created # e.g. if you wrote `all(x)` instead of `cp.all(x)` it will contain 'True' instead of the conjunction print(m) -s = cp.SolverLookup.get("ortools") +s = cp.SolverLookup.get("ortools") # will be explained later # feed the constraints one-by-one for c in m.constraints: s += c # add the constraints incrementally until you hit the error ``` -If that is not sufficient or you want to debug an unexpected (non)solution, have a look at our detailed [Debugging guide](how_to_debug.md). +If that is not sufficient or you want to debug an unexpected (non)solution, have a look at our detailed [Debugging guide](./how_to_debug.md). ## Selecting a solver -The default solver is OR-Tools CP-SAT, an award winning constraint solver. But CPMpy supports multiple other solvers: a MIP solver (gurobi), SAT solvers (those in PySAT), the Z3 SMT solver, even a knowledge compiler (PySDD) and any CP solver supported by the text-based MiniZinc language. +The default solver is [OR-Tools CP-SAT](https://developers.google.com/optimization), an award winning constraint solver. But CPMpy supports multiple other solvers: a MIP solver (gurobi), SAT solvers (those in PySAT), the Z3 SMT solver, even a knowledge compiler (PySDD) and any CP solver supported by the text-based MiniZinc language. +The list of supported solver interfaces can be found in [the API documentation](./api/solvers.rst). See the full list of solvers known by CPMpy with: ```python @@ -479,7 +496,7 @@ import cpmpy as cp cp.SolverLookup.solvernames() ``` -On my system, with pysat and minizinc installed, this gives `['ortools', 'minizinc', 'minizinc:chuffed', 'minizinc:coin-bc', ..., 'pysat:minicard', 'pysat:minisat22', 'pysat:minisat-gh'] +On a system with pysat and minizinc installed, this for example gives `['ortools', 'minizinc', 'minizinc:chuffed', 'minizinc:coin-bc', ..., 'pysat:minicard', 'pysat:minisat22', 'pysat:minisat-gh']` You can specify a solvername when calling `solve()` on a model: @@ -491,11 +508,11 @@ m = cp.Model(cp.sum(x) <= 5) m.solve(solver="minizinc:chuffed") ``` -Note that for solvers other than "ortools", you will need to **install additional package(s)**. You can check if a solver, e.g. "minizinc", is supported by calling `cp.SolverLookup.get("gurobi")` and it will raise a helpful error if it is not yet installed on your system. See [the API documentation](api/solvers.html) of the solver for detailed installation instructions. +Note that for solvers other than "ortools", you will need to **install additional package(s)**. You can check if a solver, e.g. "gurobi", is supported by calling `cp.SolverLookup.get("gurobi")` and it will raise a helpful error if it is not yet installed on your system. See [the API documentation](./api/solvers.rst) of the solver for detailed installation instructions. ## Model versus solver interface -A `Model()` is a **lazy container**. It simply stores the constraints. Only when `solve()` is called will it instantiate a solver, and send the entire model to it at once. So `m.solve("ortools")` is equivalent to: +A `Model()` is a **lazy container**. It simply stores the constraints. Only when `solve()` is called will it instantiate a solver instance, and send the entire model to it at once. So `m.solve("ortools")` is equivalent to: ```python s = SolverLookup.get("ortools", m) s.solve() @@ -521,7 +538,7 @@ On a technical note, remark that a solver object does not modify the Model objec ## Setting solver parameters Now lets use our solver-specific powers. -For example, with `m` a CPMpy Model(), you can do the following to make or-tools use 8 parallel cores and print search progress: +For example, with `m` a CPMpy Model(), you can do the following to make OR-Tools use 8 parallel cores and print search progress: ```python import cpmpy as cp @@ -530,7 +547,7 @@ s = cp.SolverLookup.get("ortools", m) s.solve(num_search_workers=8, log_search_progress=True) ``` -Modern CP-solvers support a variety of hyperparameters. (See the full list of [OR-tools parameters](https://github.com/google/or-tools/blob/stable/ortools/sat/sat_parameters.proto) for example). +Modern CP-solvers support a variety of hyperparameters. (See the full list of [OR-Tools parameters](https://github.com/google/or-tools/blob/stable/ortools/sat/sat_parameters.proto) for example). Using the solver interface, any parameter that the solver supports can be passed using the `.solve()` call. These parameters will be posted to the native solver before solving the model. @@ -540,12 +557,12 @@ s.solve(cp_model_probing_level = 2, symmetry_level = 1) ``` -See [the API documentation of the solvers](api/solvers.html) for information and links on the parameters supported. See our documentation page on [solver parameters](solver_parameters.html) if you want to tune your hyperparameters automatically. +See [the API documentation of the solvers](./api/solvers.rst) for information and links on the parameters supported. See our documentation page on [solver parameters](./solver_parameters.md) if you want to tune your hyperparameters automatically. ## Accessing the underlying solver object After solving, we can access the underlying solver object to retrieve some information about the solve. -For example in ortools we can find the number of search branches like this, expanding our previous example. +For example in OR-Tools we can find the number of search branches like this (expanding on our previous example): ```python import cpmpy as cp x = cp.intvar(0,10, shape=3) @@ -556,8 +573,8 @@ s.solve() print(s.ort_solver.NumBranches()) ``` -Other solvers, like Minizinc might have other native objects stored. -You can see which solver native objects are initialized for each solver in [the API documentation](api/solvers.html) of the solver. +Other solvers, like Minizinc, might have other native objects stored. +You can see which solver native objects are initialized for each solver in [the API documentation](./api/solvers.rst) of the solver. We can access the solver statistics from the mzn_result object like this: ```python @@ -568,7 +585,7 @@ s = cp.SolverLookup.get("minizinc") s += (cp.sum(x) <= 5) s.solve() print(s.mzn_result.statistics) -print(s.mzn_result.statistics['nodes']) #if we are only interested in the nb of search nodes +print(s.mzn_result.statistics['nodes']) # if we are only interested in the nb of search nodes ``` ## Incremental solving @@ -577,18 +594,18 @@ It is important to realize that a CPMpy solver interface is _eager_. That means This has two potential benefits for incremental solving, whereby you add more constraints and variables inbetween solve calls: 1) CPMpy only translates and posts each constraint once, even if the model is solved multiple times; and - 2) if the solver itself is incremental then it can reuse any information from call to call, as the state of the native solver object is kept between solver calls and can therefore rely on information derived during a previous `solve` call. + 2) if the solver itself is incremental then it can reuse any information from call to call, as the state of the native solver object is kept between solver calls and can therefore rely on information derived during a previous `.solve()` call. ```python -gs = SolverLookup.get("gurobi") +s = SolverLookup.get("gurobi") -gs += sum(ivar) <= 5 -gs.solve() +s += sum(ivar) <= 5 +s.solve() -gs += sum(ivar) == 3 +s += sum(ivar) == 3 # the underlying gurobi instance is reused, only the new constraint is added to it. # gurobi is an incremental solver and will look for solutions starting from the previous one. -gs.solve() +s.solve() ``` _Technical note_: OR-Tools its model representation is incremental but its solving itself is not (yet?). Gurobi and the PySAT solvers are fully incremental, as is Z3. The text-based MiniZinc language is not incremental. @@ -597,7 +614,7 @@ _Technical note_: OR-Tools its model representation is incremental but its solvi SAT and CP-SAT solvers oftentimes support solving under assumptions, which is also supported by their CPMpy interface. Assumption variables are usefull for incremental solving when you want to activate/deactivate different subsets of constraints without copying (parts of) the model or removing constraints and re-solving. By relying on the solver interface directly as in the previous section, the state of the solver is kept in between solve-calls. -Many explanation-generation algorithms (see `cpmpy.tools.explain`) make use of this feature to speed up the solving. +Many explanation-generation algorithms ([see](./api/tools/explain.rst) `cpmpy.tools.explain`) make use of this feature to speed up the solving. ```python import cpmpy as cp @@ -612,7 +629,7 @@ cp.Model([c1,c2,c3]).solve() # Will be UNSAT s = cp.SolverLookup.get("exact") # OR-tools, PySAT and Exact support solving under assumptions assump = cp.boolvar(shape=3, name="assump") -s += assump.implies([c1,c2,c3]) +s += assump.implies([c1,c2,c3]) # assump[0] -> c1, assump[1] -> c2, assump[2] -> c3 # Underlying solver state will be kept inbetween solve-calls s.solve(assumptions=assump[0,1]) # Will be SAT @@ -624,23 +641,23 @@ s.solve(assumptions=assump[1,2]) # Will be SAT ## Using solver-specific CPMpy features -We sometimes add solver-specific functions to the CPMpy interface, for convenient access. Two examples of this are `solution_hint()` and `get_core()` which is supported by the OR-Tools and PySAT solvers and interfaces. Other solvers may work differently and not have these concepts. +We sometimes add solver-specific functions to the CPMpy interface, for convenient access. Two examples of this are `solution_hint()` and `get_core()` which is supported by the OR-Tools, PySAT and Exact solvers and interfaces. Other solvers may work differently and not have these concepts. -`solution_hint()` tells the solver that it could use these variable-values first during search, e.g. typically from a previous solution: +`solution_hint()` tells the solver that it could start from these value-to-variable assignments during search, e.g. start from a previous solution: ```python import cpmpy as cp x = cp.intvar(0,10, shape=3) s = cp.SolverLookup.get("ortools") s += cp.sum(x) <= 5 -# we are operating on a ortools' interface here +# we are operating on an ortools' interface here s.solution_hint(x, [1,2,3]) s.solve() print(x.value()) ``` -`get_core()` asks the solver for an unsatisfiable core, in case a solution did not exist and assumption variables were used. See the documentation on [Unsat core extraction](unsat_core_extraction.html). +`get_core()` asks the solver for an unsatisfiable core, in case a solution did not exist and assumption variables were used. See the documentation on [Unsat core extraction](./unsat_core_extraction.md). -See [the API documentation of the solvers](api/solvers.html) to learn about their special functions. +See [the API documentation of the solvers](./api/solvers.rst) to learn about their special functions. ## Direct solver access @@ -683,7 +700,10 @@ s += cp.DirectConstraint("AddAutomaton", (trans_vars, 0, [2], trans_tabl), A minimal example of the DirectConstraint for every supported solver is [in the test suite](https://github.com/CPMpy/cpmpy/tree/master/tests/test_direct.py). -The `DirectConstraint` is a very powerful primitive to get the most out of specific solvers. See the following examples: [nonogram_ortools.ipynb](https://github.com/CPMpy/cpmpy/tree/master/examples/nonogram_ortools.ipynb) which uses a helper function that generates automatons with DirectConstraints; [vrp_ortools.py](https://github.com/CPMpy/cpmpy/tree/master/examples/vrp_ortools.ipynb) demonstrating ortools' newly introduced multi-circuit global constraint through DirectConstraint; and [pctsp_ortools.py](https://github.com/CPMpy/cpmpy/tree/master/examples/pctsp_ortools.ipynb) that uses a DirectConstraint to use OR-Tools circuit to post a sub-circuit constraint as needed for this price-collecting TSP variant. +The `DirectConstraint` is a very powerful primitive to get the most out of specific solvers. See the following examples: +- [nonogram_ortools.ipynb](https://github.com/CPMpy/cpmpy/tree/master/examples/nonogram_ortools.ipynb) which uses a helper function that generates automatons with DirectConstraints; +- [vrp_ortools.py](https://github.com/CPMpy/cpmpy/blob/master/examples/vrp_ortools.py) demonstrating OR-Tools' newly introduced multi-circuit global constraint through DirectConstraint; and +- [pctsp_ortools.py](https://github.com/CPMpy/cpmpy/blob/master/examples/pctsp_ortools.py) that uses a DirectConstraint to use OR-Tools circuit to post a sub-circuit constraint as needed for this price-collecting TSP variant. ### Directly accessing the underlying solver @@ -700,7 +720,7 @@ s += AllDifferent(iv) # the traditional way, equivalent to: s.native_model.AddAllDifferent(s.solver_vars(iv)) # directly calling the API (OR-Tools' python library), has to be with native variables ``` -Observe how we first map the CPMpy variables to native variables by calling `s.solver_vars()`, and then give these to the native solver API directly (in the case of OR-Tools, the `native_model` property returns a `CpModel` instance). This is in fact what happens behind the scenes when posting a DirectConstraint, or any CPMpy constraint. Consult [the solver API documentation](api/solvers.html) for more information on the available solver specific objects which can be accessed directly. +Observe how we first map the CPMpy variables to native variables by calling `s.solver_vars()`, and then give these to the native solver API directly (in the case of OR-Tools, the `native_model` property returns a `CpModel` instance). This is in fact what happens behind the scenes when posting a DirectConstraint, or any CPMpy constraint. Consult [the solver API documentation](./api/solvers.rst) for more information on the available solver specific objects which can be accessed directly. While directly calling the solver offers a lot of freedom, it is a bit more cumbersome as you have to map the variables manually each time. Also, you no longer have a declarative model that you can pass along, print or inspect. In contrast, a `DirectConstraint` is a CPMpy expression so it can be part of a model like any other CPMpy constraint. Note that it can only be used as top-level (non-nested, non-reified) constraint. @@ -709,7 +729,7 @@ Because CPMpy offers programmatic access to the solver API, hyperparameter searc ### Built-in tuners -The tools directory contains a utility to efficiently search through the hyperparameter space defined by the solvers `tunable_params`. +The tools directory contains a [utility](https://github.com/CPMpy/cpmpy/blob/master/cpmpy/tools/tune_solver.py) to efficiently search through the hyperparameter space defined by the solvers' `tunable_params`. Solver interfaces not providing the set of tunable parameters can still be tuned by using this utility and providing the parameter (values) yourself. diff --git a/docs/multiple_solutions.md b/docs/multiple_solutions.md index 06d8b2b09..221dfb55d 100644 --- a/docs/multiple_solutions.md +++ b/docs/multiple_solutions.md @@ -6,8 +6,8 @@ When using `solveAll()`, a solver will use an optimized native implementation be It has two special named optional arguments: - * `display=...`: accepts a CPMpy expression, a list of CPMpy expressions or a callback function that will be called on every solution found (default: None) - * `solution_limit=...`: stop after this many solutions (default: None) + - `display=...` : accepts a CPMpy expression, a list of CPMpy expressions or a callback function that will be called on every solution found (default: None) + - `solution_limit=...` : stop after this many solutions (default: None) It also accepts named argument `time_limit=...` and any other keyword argument is passed on to the solver just like `solve()` does. @@ -93,7 +93,7 @@ while s.solve(): s += ~all(x == x.value()) ``` -In case of multiple variables you should put them in one long python-native list, as such: +In case of multiple variables you should put them in one long Python-native list, as such: ```python x = intvar(0,3, shape=2) b = boolvar() @@ -111,7 +111,7 @@ while s.solve(): ## Diverse solution search A better, more complex example of repeated solving is when searching for diverse solutions. -The goal is to iteratively find solutions that are as diverse as possible with the previous solutions. Many definitions of diversity between solutions exist. We can for example measure the difference between two solutions with the Hamming distance (comparing the number of different values) or the Euclidian distance (compare the absolute difference in value for the variables). +The goal is to iteratively find solutions that are as diverse as possible with the previous solutions. Many definitions of diversity between solutions exist. We can for example measure the difference between two solutions with the [Hamming distance](https://en.wikipedia.org/wiki/Hamming_distance#:~:text=In%20information%20theory%2C%20the%20Hamming,the%20corresponding%20symbols%20are%20different.) (comparing the number of different values) or the [Euclidian distance](https://en.wikipedia.org/wiki/Euclidean_distance) (compare the absolute difference in value for the variables). Here is the example code for enumerating K diverse solutions with Hamming distance, which overwrites the objective function in each iteration: @@ -130,7 +130,7 @@ while len(store) < 3 and s.solve(): s.maximize(sum([sum(x != sol) for sol in store])) ``` -As a fun fact, observe how `x != sol` works, even though one is a vector of Boolean variables and sol is Numpy array. However, both have the same length, so this is automatically translated into a pairwise comparison constraint by CPMpy. These numpy-style vectorized operations mean we have to write much less loops while modelling. +As a fun fact, observe how `x != sol` works, even though one is a vector of Boolean variables and sol is Numpy array. However, both have the same length, so this is automatically translated into a pairwise comparison constraint by CPMpy. These numpy-style vectorized operations mean we have to write much less loops while modeling. To use the Euclidian distance, only the last line needs to be changed. We again use vectorized operations and obtain succinct models. The creation of intermediate variables (with appropriate domains) is done by CPMpy behind the scenes. @@ -157,3 +157,4 @@ cb = OrtSolutionPrinter() s.solve(enumerate_all_solutions=True, solution_callback=cb) print("Nr of solutions:",cb.solution_count()) ``` +Have a look at `OrtSolutionPrinter`'s [implementation](https://github.com/CPMpy/cpmpy/blob/master/cpmpy/solvers/ortools.py#L650). diff --git a/docs/requirements.txt b/docs/requirements.txt index bfbbd40c7..41f88aadb 100644 --- a/docs/requirements.txt +++ b/docs/requirements.txt @@ -1,7 +1,6 @@ numpy>=1.17.0 -m2r2>=0.2.7 +myst-parser sphinx-automodapi -sphinx_rtd_theme -sphinx==5.3.0 -sphinx_rtd_theme==1.1.1 -readthedocs-sphinx-search==0.1.1 \ No newline at end of file +sphinx>=5.3.0 # cannot be updated due to m2r2 no longer being maintained -> switch to MyST? +sphinx_rtd_theme>=2.0.0 +readthedocs-sphinx-search>=0.3.2 \ No newline at end of file diff --git a/docs/solvers.md b/docs/solvers.md index 11ecd309a..76035b576 100644 --- a/docs/solvers.md +++ b/docs/solvers.md @@ -2,7 +2,7 @@ CPMpy can be used as a declarative modeling language: you create a `Model()`, add constraints and call `solve()` on it. -The default solver is ortools CP-SAT, an award winning constraint solver. But CPMpy supports multiple other solvers: a MIP solver (gurobi), SAT solvers (those in PySAT), the Z3 SMT solver, a conflict-driven cutting-planes solver (Exact), even a knowledge compiler (PySDD) and any CP solver supported by the text-based MiniZinc language. +The default solver is OR-Tools CP-SAT, an award winning constraint solver. But CPMpy supports multiple other solvers: a MIP solver (gurobi), SAT solvers (those in PySAT), the Z3 SMT solver, a conflict-driven cutting-planes solver (Exact), even a knowledge compiler (PySDD) and any CP solver supported by the text-based MiniZinc language. See the list of solvers known by CPMpy with: diff --git a/docs/unsat_core_extraction.md b/docs/unsat_core_extraction.md index fd8228097..862f1ebfc 100644 --- a/docs/unsat_core_extraction.md +++ b/docs/unsat_core_extraction.md @@ -4,9 +4,9 @@ When a model is unsatisfiable, it can be desirable to get a better idea of which In the SATisfiability literature, the Boolean variables of interests are called _assumption_ variables and the solver will assume they are true. The subset of these variables that, when true, make the model unsatisfiable is called an unsatisfiable _core_. -Lazy Clause Generation solvers, like or-tools, are built on SAT solvers and hence can inherit the ability to define assumption variables and extract an unsatisfiable core. +Lazy Clause Generation solvers, like OR-Tools, are built on SAT solvers and hence can inherit the ability to define assumption variables and extract an unsatisfiable core. -Since version 8.2, or-tools supports declaring assumption variables, and extracting an unsat core. We also implement this functionality in CPMpy, using PySAT-like `s.solve(assumptions=[...])` and `s.get_core()`: +Since version 8.2, OR-Tools supports declaring assumption variables, and extracting an unsat core. We also implement this functionality in CPMpy, using PySAT-like `s.solve(assumptions=[...])` and `s.get_core()`: ```python from cpmpy import * @@ -39,8 +39,10 @@ from cpmpy.tools import mus print(mus(m.constraints)) ``` -We welcome any additional examples that use CPMpy in this way!! Here is one example: the [MARCO algorithm for enumerating all MUS/MSSes](http://github.com/tias/cppy/tree/master/examples/advanced/marco_musmss_enumeration.py). Here is another: a [stepwise explanation algorithm](https://github.com/CPMpy/cpmpy/blob/master/examples/advanced/ocus_explanations.py) for SAT problems (implicit hitting-set based) +We welcome any additional examples that use CPMpy in this way!! Here is one example: the [MARCO algorithm for enumerating all MUS/MSSes](http://github.com/tias/cppy/tree/master/examples/advanced/marco_musmss_enumeration.py). Here is another: a [stepwise explanation algorithm](https://github.com/CPMpy/cpmpy/blob/master/examples/advanced/ocus_explanations.py) for SAT problems (implicit hitting-set based). -One OR-TOOLS specific caveat is that this particular (default) solver its Python interface is by design _stateless_. That means that, unlike in PySAT, calling `s.solve(assumptions=bv)` twice for a different `bv` array does NOT REUSE anything from the previous run: no warm-starting, no learnt clauses that are kept, no incrementality, so there will be some pre-processing overhead. If you know of another CP solver with a (Python) assumption interface that is incremental, let us know!! +More information on how to use these tools can be found in [the tools API documentation](./api/tools.rst) -A final-final note is that you can manually warm-start or-tools with a previously found solution with s.solution\_hint(); see also the MARCO code linked above. +One OR-Tools specific caveat is that this particular (default) solver its Python interface is by design _stateless_. That means that, unlike in PySAT, calling `s.solve(assumptions=bv)` twice for a different `bv` array does NOT REUSE anything from the previous run: no warm-starting, no learnt clauses that are kept, no incrementality, so there will be some pre-processing overhead. If you know of another CP solver with a (Python) assumption interface that is incremental, let us know!! + +A final-final note is that you can manually warm-start OR-Tools with a previously found solution through `s.solution_hint()`; see also the MARCO code linked above.