From e2391e811c461d4761ab242242775bd02e0eea5e Mon Sep 17 00:00:00 2001 From: Thomas Sergeys Date: Mon, 15 Jul 2024 13:42:40 +0200 Subject: [PATCH 01/13] docs: straight forward improvements --- cpmpy/expressions/globalfunctions.py | 3 ++- cpmpy/expressions/variables.py | 15 ++++++++++++--- cpmpy/model.py | 6 +++--- cpmpy/solvers/__init__.py | 4 ++-- cpmpy/solvers/choco.py | 6 ++++++ cpmpy/solvers/exact.py | 9 ++++++++- cpmpy/solvers/gurobi.py | 4 ++++ cpmpy/solvers/minizinc.py | 8 ++++++++ cpmpy/solvers/ortools.py | 8 ++++++-- cpmpy/solvers/pysat.py | 4 ++++ cpmpy/solvers/pysdd.py | 9 +++++++++ cpmpy/solvers/z3.py | 8 ++++++++ docs/adding_solver.md | 2 +- docs/developers.md | 23 ++++++++++++----------- docs/how_to_debug.md | 10 +++++----- docs/modeling.md | 24 ++++++++++++------------ docs/multiple_solutions.md | 8 ++++---- docs/solvers.md | 2 +- docs/unsat_core_extraction.md | 8 ++++---- 19 files changed, 111 insertions(+), 50 deletions(-) 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/variables.py b/cpmpy/expressions/variables.py index 31c1ab33b..d39d70103 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. =============== @@ -126,7 +135,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 0b95daeab..a0249c4a7 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 e66a71d6c..06fe6dc41 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 db9b0afee..de9fca8d9 100644 --- a/cpmpy/solvers/choco.py +++ b/cpmpy/solvers/choco.py @@ -1,4 +1,6 @@ #!/usr/bin/env python +#-*- coding:utf-8 -*- +## ## choco.py ## """ @@ -18,6 +20,10 @@ :nosignatures: CPM_choco + + ============== + Module details + ============== """ import time diff --git a/cpmpy/solvers/exact.py b/cpmpy/solvers/exact.py index 5f0598cfb..72a28d100 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 diff --git a/cpmpy/solvers/gurobi.py b/cpmpy/solvers/gurobi.py index dbe3618bf..4e2c8406f 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 diff --git a/cpmpy/solvers/minizinc.py b/cpmpy/solvers/minizinc.py index 0aae6579c..c66fa2a0b 100644 --- a/cpmpy/solvers/minizinc.py +++ b/cpmpy/solvers/minizinc.py @@ -1,4 +1,8 @@ #!/usr/bin/env python +#-*- coding:utf-8 -*- +## +## minizinc.py +## """ Interface to MiniZinc's Python API @@ -22,6 +26,10 @@ :nosignatures: CPM_minizinc + + ============== + Module details + ============== """ import re import warnings diff --git a/cpmpy/solvers/ortools.py b/cpmpy/solvers/ortools.py index b15e12243..e2ab65be8 100644 --- a/cpmpy/solvers/ortools.py +++ b/cpmpy/solvers/ortools.py @@ -4,7 +4,7 @@ ## ortools.py ## """ - Interface to ortools' CP-SAT Python API + Interface to OR-Tools' CP-SAT Python API. 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 +22,10 @@ :nosignatures: CPM_ortools + + ============== + Module details + ============== """ import sys # for stdout checking import numpy as np @@ -42,7 +46,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 diff --git a/cpmpy/solvers/pysat.py b/cpmpy/solvers/pysat.py index 889e48aa8..907c35b85 100644 --- a/cpmpy/solvers/pysat.py +++ b/cpmpy/solvers/pysat.py @@ -28,6 +28,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..fa0073348 100644 --- a/cpmpy/solvers/pysdd.py +++ b/cpmpy/solvers/pysdd.py @@ -1,3 +1,8 @@ +#!/usr/bin/env python +#-*- coding:utf-8 -*- +## +## pysdd.py +## """ Interface to PySDD's API @@ -19,6 +24,10 @@ :nosignatures: CPM_pysdd + + ============== + Module details + ============== """ from functools import reduce from .solver_interface import SolverInterface, SolverStatus, ExitStatus diff --git a/cpmpy/solvers/z3.py b/cpmpy/solvers/z3.py index 52776ee1e..db93275fd 100644 --- a/cpmpy/solvers/z3.py +++ b/cpmpy/solvers/z3.py @@ -1,4 +1,8 @@ #!/usr/bin/env python +#-*- coding:utf-8 -*- +## +## z3.py +## """ Interface to z3's API @@ -19,6 +23,10 @@ :nosignatures: CPM_z3 + + ============== + Module details + ============== """ from .solver_interface import SolverInterface, SolverStatus, ExitStatus from ..exceptions import NotSupportedError diff --git a/docs/adding_solver.md b/docs/adding_solver.md index f579f3bea..7c55fc859 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 diff --git a/docs/developers.md b/docs/developers.md index f8d4db9af..fbf7c2927 100644 --- a/docs/developers.md +++ b/docs/developers.md @@ -34,25 +34,26 @@ 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. diff --git a/docs/how_to_debug.md b/docs/how_to_debug.md index 5c9f5d253..5344ef19d 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. @@ -36,7 +36,7 @@ Here are a few quirks in Python/CPMpy: 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 +52,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 @@ -158,5 +158,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/modeling.md b/docs/modeling.md index 8bf897bc8..a5496a9a9 100644 --- a/docs/modeling.md +++ b/docs/modeling.md @@ -14,13 +14,13 @@ See [installation instructions](installation_instructions.html) 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. -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 ``` @@ -174,7 +174,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,7 +226,7 @@ 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: @@ -258,7 +258,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 @@ -341,7 +341,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: @@ -521,7 +521,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 +530,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. @@ -545,7 +545,7 @@ See [the API documentation of the solvers](api/solvers.html) for information and ## 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,7 +556,7 @@ s.solve() print(s.ort_solver.NumBranches()) ``` -Other solvers, like Minizinc might have other native objects stored. +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. We can access the solver statistics from the mzn_result object like this: @@ -568,7 +568,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,7 +577,7 @@ 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") diff --git a/docs/multiple_solutions.md b/docs/multiple_solutions.md index 06d8b2b09..cd6cadeee 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() @@ -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. 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..d36cd81d6 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 * @@ -41,6 +41,6 @@ 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) -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!! +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 with s.solution\_hint(); see also the MARCO code linked above. +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. From 5843b228e239d3b62a08aab8a94bc8af58ec9bfd Mon Sep 17 00:00:00 2001 From: Thomas Sergeys Date: Mon, 15 Jul 2024 13:44:25 +0200 Subject: [PATCH 02/13] docs: improve solver install instructions --- cpmpy/solvers/choco.py | 5 ++++- cpmpy/solvers/gurobi.py | 5 +++-- cpmpy/solvers/minizinc.py | 10 +++++++++- cpmpy/solvers/ortools.py | 5 +++++ cpmpy/solvers/pysat.py | 4 ++++ cpmpy/solvers/pysdd.py | 4 ++++ cpmpy/solvers/z3.py | 4 ++++ 7 files changed, 33 insertions(+), 4 deletions(-) diff --git a/cpmpy/solvers/choco.py b/cpmpy/solvers/choco.py index de9fca8d9..1a10f878b 100644 --- a/cpmpy/solvers/choco.py +++ b/cpmpy/solvers/choco.py @@ -6,7 +6,10 @@ """ 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/ diff --git a/cpmpy/solvers/gurobi.py b/cpmpy/solvers/gurobi.py index 4e2c8406f..d532efcc9 100644 --- a/cpmpy/solvers/gurobi.py +++ b/cpmpy/solvers/gurobi.py @@ -10,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 =============== diff --git a/cpmpy/solvers/minizinc.py b/cpmpy/solvers/minizinc.py index c66fa2a0b..5013fe1c6 100644 --- a/cpmpy/solvers/minizinc.py +++ b/cpmpy/solvers/minizinc.py @@ -6,7 +6,13 @@ """ 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 @@ -18,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 =============== diff --git a/cpmpy/solvers/ortools.py b/cpmpy/solvers/ortools.py index e2ab65be8..f43b2a782 100644 --- a/cpmpy/solvers/ortools.py +++ b/cpmpy/solvers/ortools.py @@ -5,6 +5,11 @@ ## """ 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. diff --git a/cpmpy/solvers/pysat.py b/cpmpy/solvers/pysat.py index 907c35b85..dba10e431 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. diff --git a/cpmpy/solvers/pysdd.py b/cpmpy/solvers/pysdd.py index fa0073348..c30bf373b 100644 --- a/cpmpy/solvers/pysdd.py +++ b/cpmpy/solvers/pysdd.py @@ -6,6 +6,10 @@ """ 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/ diff --git a/cpmpy/solvers/z3.py b/cpmpy/solvers/z3.py index db93275fd..907eb53af 100644 --- a/cpmpy/solvers/z3.py +++ b/cpmpy/solvers/z3.py @@ -6,6 +6,10 @@ """ 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 From 933950ef5fc20a06b1ecc8538053d42f317c8cb9 Mon Sep 17 00:00:00 2001 From: Thomas Sergeys Date: Mon, 15 Jul 2024 15:41:40 +0200 Subject: [PATCH 03/13] docs: Add useful links --- docs/adding_solver.md | 4 ++-- docs/developers.md | 2 +- docs/how_to_debug.md | 10 ++++++---- docs/modeling.md | 12 ++++++++---- docs/multiple_solutions.md | 3 ++- docs/unsat_core_extraction.md | 4 +++- 6 files changed, 22 insertions(+), 13 deletions(-) diff --git a/docs/adding_solver.md b/docs/adding_solver.md index 7c55fc859..43e42b6cd 100644 --- a/docs/adding_solver.md +++ b/docs/adding_solver.md @@ -35,7 +35,7 @@ The way that CPMpy succeeds to be an incremental modeling language, is by making 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! diff --git a/docs/developers.md b/docs/developers.md index fbf7c2927..c3ee62e25 100644 --- a/docs/developers.md +++ b/docs/developers.md @@ -55,7 +55,7 @@ Tools are not part of the core of CPMpy. They are additional tools that _use_ CP ## 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/how_to_debug.md b/docs/how_to_debug.md index 5344ef19d..a8bf6a9e4 100644 --- a/docs/how_to_debug.md +++ b/docs/how_to_debug.md @@ -21,7 +21,7 @@ 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.html) 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). @@ -62,7 +62,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 +95,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.html), that you can use as follows: ```python from cpmpy.tools import mus @@ -113,7 +113,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 +142,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.html). + ## 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. diff --git a/docs/modeling.md b/docs/modeling.md index a5496a9a9..7952c9923 100644 --- a/docs/modeling.md +++ b/docs/modeling.md @@ -4,7 +4,7 @@ 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](./modeling.html#selecting-a-solver)): ```commandline pip install cpmpy @@ -96,6 +96,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.html) for more detailed information. + ## Expressing constraints A constraint is a relation between decision variables that restricts what values these variables can take. @@ -436,6 +438,7 @@ 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. 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 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.html) for the solver in question. ```python n = m.solveAll(display=[x,cp.sum(x)], solution_limit=3) # [array([1, 0]), 1] @@ -470,8 +473,9 @@ If that is not sufficient or you want to debug an unexpected (non)solution, have ## 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.html). See the full list of solvers known by CPMpy with: ```python @@ -597,7 +601,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.html) `cpmpy.tools.explain`) make use of this feature to speed up the solving. ```python import cpmpy as cp @@ -709,7 +713,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 cd6cadeee..b0234df98 100644 --- a/docs/multiple_solutions.md +++ b/docs/multiple_solutions.md @@ -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: @@ -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#L640). diff --git a/docs/unsat_core_extraction.md b/docs/unsat_core_extraction.md index d36cd81d6..aadd2b034 100644 --- a/docs/unsat_core_extraction.md +++ b/docs/unsat_core_extraction.md @@ -39,7 +39,9 @@ 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). + +More information on how to use these tools can be found in [the tools API documentation](api/tools.html) 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!! From 207c9978942c4183887386cd6b32f83ebd416041 Mon Sep 17 00:00:00 2001 From: Thomas Sergeys Date: Tue, 16 Jul 2024 13:13:06 +0200 Subject: [PATCH 04/13] docs: Add missing pages --- cpmpy/expressions/utils.py | 8 +++++ cpmpy/tools/__init__.py | 12 +++++++ cpmpy/tools/explain/__init__.py | 21 ++++++++++++ cpmpy/tools/explain/utils.py | 18 ++++++++++ cpmpy/transformations/__init__.py | 9 ++++- cpmpy/transformations/comparison.py | 13 ++++---- cpmpy/transformations/reification.py | 19 +++++------ cpmpy/transformations/to_cnf.py | 9 ++--- docs/api/expressions/globalfunctions.rst | 7 ++++ docs/api/solvers/choco.rst | 7 ++++ docs/api/tools.rst | 6 ++++ docs/api/tools/dimacs.rst | 7 ++++ docs/api/tools/explain.rst | 33 +++++++++++++++++++ docs/api/tools/explain/mcs.rst | 7 ++++ docs/api/tools/explain/mss.rst | 7 ++++ docs/api/tools/explain/mus.rst | 7 ++++ docs/api/tools/explain/utils.rst | 7 ++++ docs/api/tools/miximal_propagate.rst | 7 ++++ docs/api/tools/tune_solver.rst | 7 ++++ docs/api/transformations.rst | 11 +++++++ docs/api/transformations/comparison.rst | 9 +++++ docs/api/transformations/decompose_global.rst | 7 ++++ docs/api/transformations/negation.rst | 7 ++++ docs/api/transformations/normalize.rst | 7 ++++ docs/index.rst | 3 +- 25 files changed, 232 insertions(+), 23 deletions(-) create mode 100644 docs/api/expressions/globalfunctions.rst create mode 100644 docs/api/solvers/choco.rst create mode 100644 docs/api/tools.rst create mode 100644 docs/api/tools/dimacs.rst create mode 100644 docs/api/tools/explain.rst create mode 100644 docs/api/tools/explain/mcs.rst create mode 100644 docs/api/tools/explain/mss.rst create mode 100644 docs/api/tools/explain/mus.rst create mode 100644 docs/api/tools/explain/utils.rst create mode 100644 docs/api/tools/miximal_propagate.rst create mode 100644 docs/api/tools/tune_solver.rst create mode 100644 docs/api/transformations/comparison.rst create mode 100644 docs/api/transformations/decompose_global.rst create mode 100644 docs/api/transformations/negation.rst create mode 100644 docs/api/transformations/normalize.rst diff --git a/cpmpy/expressions/utils.py b/cpmpy/expressions/utils.py index 06bf92fc3..6bd8ae748 100644 --- a/cpmpy/expressions/utils.py +++ b/cpmpy/expressions/utils.py @@ -12,14 +12,22 @@ .. 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 + get_store """ import numpy as np 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/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/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/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..4e36161e3 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 ExprStore, is_boolexpr, get_store +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/reification.py b/cpmpy/transformations/reification.py index 3861398c1..4230bad84 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 ExprStore, get_store, 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..fbe027939 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,11 @@ - BE -> BV - BV -> BE """ +from cpmpy.expressions.utils import ExprStore, get_store +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/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/miximal_propagate.rst b/docs/api/tools/miximal_propagate.rst new file mode 100644 index 000000000..9fe5dad3a --- /dev/null +++ b/docs/api/tools/miximal_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/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 From 24c7bbfa95fa83e4864a2a0c25b222af6015064d Mon Sep 17 00:00:00 2001 From: Thomas Sergeys Date: Tue, 16 Jul 2024 13:15:01 +0200 Subject: [PATCH 05/13] docs: small improvements --- cpmpy/expressions/core.py | 24 +++++---- cpmpy/solvers/exact.py | 2 +- cpmpy/solvers/gurobi.py | 1 + cpmpy/solvers/minizinc.py | 2 +- cpmpy/solvers/ortools.py | 2 +- cpmpy/solvers/utils.py | 6 +-- cpmpy/tools/dimacs.py | 25 ++++++---- cpmpy/tools/explain/mcs.py | 2 +- cpmpy/tools/tune_solver.py | 24 +++++---- docs/adding_solver.md | 5 +- docs/how_to_debug.md | 3 +- docs/modeling.md | 100 +++++++++++++++++++++---------------- 12 files changed, 111 insertions(+), 85 deletions(-) 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/solvers/exact.py b/cpmpy/solvers/exact.py index 72a28d100..2573c9fa6 100644 --- a/cpmpy/solvers/exact.py +++ b/cpmpy/solvers/exact.py @@ -91,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 d532efcc9..de6a58499 100644 --- a/cpmpy/solvers/gurobi.py +++ b/cpmpy/solvers/gurobi.py @@ -88,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 5013fe1c6..5026c7b1f 100644 --- a/cpmpy/solvers/minizinc.py +++ b/cpmpy/solvers/minizinc.py @@ -682,7 +682,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 f43b2a782..cb58e6598 100644 --- a/cpmpy/solvers/ortools.py +++ b/cpmpy/solvers/ortools.py @@ -88,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/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/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/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/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/docs/adding_solver.md b/docs/adding_solver.md index 43e42b6cd..2b584de60 100644 --- a/docs/adding_solver.md +++ b/docs/adding_solver.md @@ -29,7 +29,7 @@ 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. @@ -102,5 +102,6 @@ After posting the constraint, the answer of your solver is checked so you will b ## 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). +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/how_to_debug.md b/docs/how_to_debug.md index a8bf6a9e4..1def89b6f 100644 --- a/docs/how_to_debug.md +++ b/docs/how_to_debug.md @@ -27,12 +27,13 @@ Either you have the same output, and it is not the solver's fault, or you have a ## 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. diff --git a/docs/modeling.md b/docs/modeling.md index 7952c9923..4014eb7d4 100644 --- a/docs/modeling.md +++ b/docs/modeling.md @@ -18,12 +18,14 @@ 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: ```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,7 +61,9 @@ 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. @@ -67,9 +71,9 @@ Note that decision variables are not tied to a model. You can use the same varia ## 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: @@ -164,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! @@ -230,7 +234,7 @@ m = cp.Model( 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 @@ -271,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.html). -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. @@ -289,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.html). -#### 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.html#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.html). ```python import cpmpy as cp @@ -324,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. @@ -373,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. @@ -435,22 +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.html) 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). ## 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 @@ -463,7 +476,7 @@ 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 @@ -483,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: @@ -495,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.html) 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() @@ -584,15 +597,15 @@ This has two potential benefits for incremental solving, whereby you add more co 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. @@ -616,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 @@ -628,15 +641,15 @@ 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()) @@ -687,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 From e15601c46420bb5c4d4a7bcbbf7ce1eda8ece1fb Mon Sep 17 00:00:00 2001 From: Thomas Sergeys Date: Tue, 16 Jul 2024 14:05:45 +0200 Subject: [PATCH 06/13] Remove leftover of CSE --- cpmpy/transformations/comparison.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cpmpy/transformations/comparison.py b/cpmpy/transformations/comparison.py index 4e36161e3..eee30461c 100644 --- a/cpmpy/transformations/comparison.py +++ b/cpmpy/transformations/comparison.py @@ -18,7 +18,7 @@ import copy from .flatten_model import get_or_make_var from ..expressions.core import Comparison, Operator -from ..expressions.utils import ExprStore, is_boolexpr, get_store +from ..expressions.utils import is_boolexpr from ..expressions.variables import _NumVarImpl, _BoolVarImpl def only_numexpr_equality(constraints, supported=frozenset()): From 2701d2732df968c62af07a3885b8c67a53f72c13 Mon Sep 17 00:00:00 2001 From: Thomas Sergeys Date: Tue, 16 Jul 2024 14:05:45 +0200 Subject: [PATCH 07/13] Remove leftover of CSE --- cpmpy/expressions/utils.py | 3 +-- cpmpy/transformations/comparison.py | 2 +- cpmpy/transformations/reification.py | 2 +- cpmpy/transformations/to_cnf.py | 1 - 4 files changed, 3 insertions(+), 5 deletions(-) diff --git a/cpmpy/expressions/utils.py b/cpmpy/expressions/utils.py index 6bd8ae748..ecd865fe2 100644 --- a/cpmpy/expressions/utils.py +++ b/cpmpy/expressions/utils.py @@ -26,8 +26,7 @@ argval argvals eval_comparison - get_bounds - get_store + get_bounds """ import numpy as np diff --git a/cpmpy/transformations/comparison.py b/cpmpy/transformations/comparison.py index 4e36161e3..eee30461c 100644 --- a/cpmpy/transformations/comparison.py +++ b/cpmpy/transformations/comparison.py @@ -18,7 +18,7 @@ import copy from .flatten_model import get_or_make_var from ..expressions.core import Comparison, Operator -from ..expressions.utils import ExprStore, is_boolexpr, get_store +from ..expressions.utils import is_boolexpr from ..expressions.variables import _NumVarImpl, _BoolVarImpl def only_numexpr_equality(constraints, supported=frozenset()): diff --git a/cpmpy/transformations/reification.py b/cpmpy/transformations/reification.py index 4230bad84..21b41b769 100644 --- a/cpmpy/transformations/reification.py +++ b/cpmpy/transformations/reification.py @@ -19,7 +19,7 @@ from ..expressions.globalfunctions import Element from ..expressions.variables import _BoolVarImpl, _NumVarImpl from ..expressions.python_builtins import all -from ..expressions.utils import ExprStore, get_store, is_any_list +from ..expressions.utils import is_any_list from .flatten_model import flatten_constraint, get_or_make_var from .negation import recurse_negation diff --git a/cpmpy/transformations/to_cnf.py b/cpmpy/transformations/to_cnf.py index fbe027939..c982b5276 100644 --- a/cpmpy/transformations/to_cnf.py +++ b/cpmpy/transformations/to_cnf.py @@ -18,7 +18,6 @@ - BE -> BV - BV -> BE """ -from cpmpy.expressions.utils import ExprStore, get_store from ..expressions.core import Operator, Comparison from ..expressions.variables import _BoolVarImpl, NegBoolView from .reification import only_implies From 99ea14ef9a68846bf58808a14cf979404af3b21d Mon Sep 17 00:00:00 2001 From: Thomas Sergeys Date: Tue, 16 Jul 2024 15:04:01 +0200 Subject: [PATCH 08/13] docs: todo list a non-complete list of things to do to improve the documentation --- docs/docs_todo.md | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 docs/docs_todo.md diff --git a/docs/docs_todo.md b/docs/docs_todo.md new file mode 100644 index 000000000..b7ab348ea --- /dev/null +++ b/docs/docs_todo.md @@ -0,0 +1,29 @@ +# 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) + +- [ ] 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 + From 00269a1c69c4e53d75a76f3d1dbd2031c0003862 Mon Sep 17 00:00:00 2001 From: Thomas Sergeys Date: Tue, 16 Jul 2024 15:04:01 +0200 Subject: [PATCH 09/13] docs: todo list a non-complete list of things to do to improve the documentation --- docs/docs_todo.md | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) create mode 100644 docs/docs_todo.md diff --git a/docs/docs_todo.md b/docs/docs_todo.md new file mode 100644 index 000000000..730dde2f6 --- /dev/null +++ b/docs/docs_todo.md @@ -0,0 +1,32 @@ +# 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 + From 4da121be1182c30ac8fa28e793abcd6dae27c9be Mon Sep 17 00:00:00 2001 From: Thomas Sergeys Date: Wed, 17 Jul 2024 09:49:35 +0200 Subject: [PATCH 10/13] Update sphinx dependencies --- docs/requirements.txt | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/docs/requirements.txt b/docs/requirements.txt index bfbbd40c7..2b3a4c6b3 100644 --- a/docs/requirements.txt +++ b/docs/requirements.txt @@ -1,7 +1,6 @@ numpy>=1.17.0 m2r2>=0.2.7 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 From eee84881e3ec0a43018cc1d77260d4530f804862 Mon Sep 17 00:00:00 2001 From: wout4 Date: Thu, 18 Jul 2024 16:25:21 +0200 Subject: [PATCH 11/13] add file headers --- cpmpy/transformations/decompose_global.py | 4 ++++ cpmpy/transformations/negation.py | 3 +++ cpmpy/transformations/normalize.py | 4 ++++ 3 files changed, 11 insertions(+) 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 From 0a93ff1ef47945fcd514012d95242fd3841c2db2 Mon Sep 17 00:00:00 2001 From: Thomas Sergeys Date: Thu, 25 Jul 2024 10:33:27 +0200 Subject: [PATCH 12/13] Change m2r2 to MyST m2r2 is not longer actively maintained, causing issues with newer versions of sphinx. As a bonus, cross-referencing is now easier, allowing to directly write links to .rst files instead of their build .html counterparts. --- docs/adding_solver.md | 2 +- docs/conf.py | 18 ++++++++++++++++- docs/docs_todo.md | 6 +++++- docs/how_to_debug.md | 6 +++--- docs/modeling.md | 38 +++++++++++++++++------------------ docs/multiple_solutions.md | 2 +- docs/requirements.txt | 2 +- docs/unsat_core_extraction.md | 2 +- 8 files changed, 48 insertions(+), 28 deletions(-) diff --git a/docs/adding_solver.md b/docs/adding_solver.md index 2b584de60..0fe6f9d9e 100644 --- a/docs/adding_solver.md +++ b/docs/adding_solver.md @@ -101,7 +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)). +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/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/docs_todo.md b/docs/docs_todo.md index dae494d6d..0fcba6b5f 100644 --- a/docs/docs_todo.md +++ b/docs/docs_todo.md @@ -7,7 +7,7 @@ A lot of proof-reading is still needed to catch all formatting mistakes (especia - [ ] 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) @@ -31,3 +31,7 @@ A lot of proof-reading is still needed to catch all formatting mistakes (especia - [ ] 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 1def89b6f..40ed0d418 100644 --- a/docs/how_to_debug.md +++ b/docs/how_to_debug.md @@ -21,7 +21,7 @@ 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. Take a look at [the solver API interface](api/solvers.html) for the install instructions. +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). @@ -96,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](api/tools.html), 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 @@ -143,7 +143,7 @@ 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.html). +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 diff --git a/docs/modeling.md b/docs/modeling.md index 8c442f570..0bdf70ed6 100644 --- a/docs/modeling.md +++ b/docs/modeling.md @@ -4,13 +4,13 @@ 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 (see how to use alternative solvers [here](./modeling.html#selecting-a-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 @@ -65,7 +65,7 @@ Similar to individual decision variables, you can call `v.value()` on these n-di 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. @@ -100,7 +100,7 @@ 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.html) for more detailed information. +See [the API documentation on models](./api/model.rst) for more detailed information. ## Expressing constraints @@ -283,7 +283,7 @@ However, a solver that has specialised datastructures for this constraint specif 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.html). +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). Global constraints can also be reified (e.g. used in an implication or equality constraint). @@ -300,7 +300,7 @@ cp.Model( cp.Xor(b, cp.AllDifferent(x)), # etc... ) ``` -`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.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). #### Global functions @@ -308,11 +308,11 @@ Coming back to the Python-builtin functions `min(),max(),abs()`, these are a bit 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 **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.html#cpmpy.expressions.globalfunctions.Abs.decompose_comparison)) on the global function. +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 functions, 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 @@ -445,7 +445,7 @@ When using `solveAll()`, a solver will use an optimized native implementation be 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.html) for the solver in question. +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) @@ -459,7 +459,7 @@ n = m.solveAll(display=lambda: print([x.value(), cp.sum(x).value()]), solution_l ``` (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 @@ -482,13 +482,13 @@ 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](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.html). +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 @@ -508,7 +508,7 @@ 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. "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.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 @@ -557,7 +557,7 @@ 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 @@ -574,7 +574,7 @@ 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. +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 @@ -614,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](api/tools/explain.html) `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 @@ -655,9 +655,9 @@ 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 @@ -720,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. diff --git a/docs/multiple_solutions.md b/docs/multiple_solutions.md index b0234df98..221dfb55d 100644 --- a/docs/multiple_solutions.md +++ b/docs/multiple_solutions.md @@ -157,4 +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#L640). +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 2b3a4c6b3..41f88aadb 100644 --- a/docs/requirements.txt +++ b/docs/requirements.txt @@ -1,5 +1,5 @@ numpy>=1.17.0 -m2r2>=0.2.7 +myst-parser sphinx-automodapi sphinx>=5.3.0 # cannot be updated due to m2r2 no longer being maintained -> switch to MyST? sphinx_rtd_theme>=2.0.0 diff --git a/docs/unsat_core_extraction.md b/docs/unsat_core_extraction.md index aadd2b034..862f1ebfc 100644 --- a/docs/unsat_core_extraction.md +++ b/docs/unsat_core_extraction.md @@ -41,7 +41,7 @@ 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). -More information on how to use these tools can be found in [the tools API documentation](api/tools.html) +More information on how to use these tools can be found in [the tools API documentation](./api/tools.rst) 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!! From 2e5fe6c13d95508cbe78bfd1969d389009634dbb Mon Sep 17 00:00:00 2001 From: Thomas Sergeys Date: Thu, 25 Jul 2024 10:42:29 +0200 Subject: [PATCH 13/13] Typo in filename --- docs/api/tools/{miximal_propagate.rst => maximal_propagate.rst} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename docs/api/tools/{miximal_propagate.rst => maximal_propagate.rst} (100%) diff --git a/docs/api/tools/miximal_propagate.rst b/docs/api/tools/maximal_propagate.rst similarity index 100% rename from docs/api/tools/miximal_propagate.rst rename to docs/api/tools/maximal_propagate.rst