|
1 | | -# python-minizinc-maker |
| 1 | +# pymzm |
2 | 2 |
|
3 | | -Create pure Minizinc .mzn files from Python using [python-minizinc-maker](https://github.com/Arthod/python-minizinc-maker/). |
| 3 | +Model and solve [MiniZinc](https://www.minizinc.org/) constraint problems in Python - no `.mzn` files required. |
4 | 4 |
|
5 | | -## Compatibility and Migration |
| 5 | +```python |
| 6 | +import pymzm |
| 7 | +import minizinc |
| 8 | + |
| 9 | +model = pymzm.Model() |
| 10 | +x = model.add_variable("x", val_min=1, val_max=100) |
| 11 | +y = model.add_variable("y", val_min=1, val_max=100) |
| 12 | + |
| 13 | +model.add_constraint(x * y == 7829 * 6907) |
| 14 | +model.add_constraint(x > y) |
| 15 | + |
| 16 | +model.set_solve_criteria(pymzm.SOLVE_SATISFY) |
6 | 17 |
|
7 | | -- Compatibility policy: [docs/compatibility_policy.md](docs/compatibility_policy.md) |
8 | | -- Migration notes: [docs/migration_notes.md](docs/migration_notes.md) |
9 | | -- Test matrix: [docs/test_matrix.md](docs/test_matrix.md) |
| 18 | +gecode = minizinc.Solver.lookup("gecode") |
| 19 | +result = model.solve(solver=gecode) |
| 20 | +print(result.x, result.y) # 7829 6907 |
| 21 | +``` |
10 | 22 |
|
11 | 23 | ## Install |
12 | | -Installed with pip from [pypi](https://pypi.org/project/pymzm/0.0.1/) |
| 24 | + |
13 | 25 | ``` |
14 | | -pip3 install pymzm |
| 26 | +pip install pymzm |
15 | 27 | ``` |
16 | 28 |
|
17 | | -## Model |
18 | | -Model: `model = pymzm.Model()` \ |
19 | | -Variable: `x = model.add_variable(name, vtype, val_min, val_max)` \ |
20 | | -Variables: `xs = model.add_variables(name, indicies, vtype, val_min, val_max)` \ |
21 | | -Constraint: `model.add_constraint(expr)`\ |
22 | | -Solve: `model.set_solve_criteria(solve_criteria, expr)` |
| 29 | +Requires [MiniZinc](https://www.minizinc.org/software.html) to be installed and on `PATH`. |
23 | 30 |
|
24 | | -### Global constraints |
25 | | -alldifferent, among, all_equal, count, increasing, decreasing, ..(more to be added later).. |
| 31 | +## Quickstart |
26 | 32 |
|
27 | | -### Solve |
28 | | -* model.set_solve_criteria(pymzm.SOLVE_MAXIMIZE, pymzm.Expression.sum(xs)) |
29 | | -* model.set_solve_criteria(pymzm.SOLVE_SATISFY) |
| 33 | +### 1. Build a model |
30 | 34 |
|
31 | | -## Examples |
32 | | -### intfact.py - Integer Factorization example |
33 | | -intfact.py |
34 | 35 | ```python |
35 | | -import pymzm |
36 | 36 | model = pymzm.Model() |
| 37 | +``` |
| 38 | + |
| 39 | +**Add a single variable:** |
| 40 | +```python |
| 41 | +x = model.add_variable("x", val_min=0, val_max=10) |
| 42 | +# float variable |
| 43 | +f = model.add_variable("f", vtype=pymzm.Variable.VTYPE_FLOAT, val_min=0.0, val_max=1.0) |
| 44 | +# bool variable |
| 45 | +b = model.add_variable("b", vtype=pymzm.Variable.VTYPE_BOOL) |
| 46 | +``` |
37 | 47 |
|
38 | | -x = model.add_variable("x", val_min=1, val_max=99999999) |
39 | | -y = model.add_variable("y", val_min=1, val_max=99999999) |
| 48 | +**Add indexed variables (returns a `ValueDict`):** |
| 49 | +```python |
| 50 | +xs = model.add_variables("x", indices=range(5), val_min=0, val_max=10) |
| 51 | +grid = model.add_variables("cell", indices=[(i, j) for i in range(3) for j in range(3)], val_min=1, val_max=9) |
40 | 52 |
|
41 | | -model.add_constraint(x * y == 7829 * 6907) |
42 | | -model.add_constraint(y > 1) |
| 53 | +xs[0] # Variable "x_0" |
| 54 | +grid[1, 2] # Variable "cell_1_2" |
| 55 | +``` |
| 56 | + |
| 57 | +### 2. Add constraints |
| 58 | + |
| 59 | +```python |
| 60 | +model.add_constraint(x + y == 10) |
43 | 61 | model.add_constraint(x > y) |
| 62 | +model.add_constraint(pymzm.Constraint.alldifferent(xs)) |
| 63 | +``` |
| 64 | + |
| 65 | +**Multiple constraints at once:** |
| 66 | +```python |
| 67 | +model.add_constraints([ |
| 68 | + xs[i] + xs[i + 1] <= 5 |
| 69 | + for i in range(len(xs) - 1) |
| 70 | +]) |
| 71 | +``` |
44 | 72 |
|
| 73 | +### 3. Set solve criteria |
| 74 | + |
| 75 | +```python |
45 | 76 | model.set_solve_criteria(pymzm.SOLVE_SATISFY) |
| 77 | +model.set_solve_criteria(pymzm.SOLVE_MAXIMIZE, expr=pymzm.Expression.sum(xs)) |
| 78 | +model.set_solve_criteria(pymzm.SOLVE_MINIMIZE, expr=x) |
| 79 | +``` |
| 80 | + |
| 81 | +### 4. Solve |
| 82 | + |
| 83 | +```python |
46 | 84 | gecode = minizinc.Solver.lookup("gecode") |
| 85 | + |
| 86 | +result = model.solve(solver=gecode) |
47 | 87 | result = model.solve(solver=gecode, all_solutions=True) |
48 | | -print(f"x = {result[0].x}") # x = 7829 |
49 | | -print(f"y = {result[0].y}") # y = 6907 |
| 88 | +result = model.solve(solver=gecode, timeout=datetime.timedelta(seconds=10)) |
| 89 | +result = model.solve(solver=gecode, threads=4, free_search=True) |
50 | 90 | ``` |
51 | 91 |
|
52 | | -Optional debug/export workflow: |
| 92 | +**Shortcuts:** |
53 | 93 | ```python |
54 | | -model.generate(debug=True) |
55 | | -model.write("model.mzn") |
| 94 | +result = model.optimize(solver=gecode) # requires maximize/minimize criteria |
| 95 | +is_sat = model.check_satisfiable(solver=gecode) # returns bool |
56 | 96 | ``` |
57 | 97 |
|
58 | | -### bibd.py - Balanced Incomplete Block Design |
59 | | -https://www.csplib.org/Problems/prob028/ |
| 98 | +### 5. Read results |
| 99 | + |
60 | 100 | ```python |
61 | | -v = 7; b = 7; r = 3; k = 3; l = 1 |
| 101 | +# Single solution |
| 102 | +result.x # by variable name (attribute style) |
| 103 | +result["x"] # dict style |
| 104 | +result["x_0"] # indexed variable |
| 105 | + |
| 106 | +# Multiple solutions (all_solutions=True) |
| 107 | +result[0].x |
| 108 | +result[0, "x_0"] # index + variable name |
| 109 | +len(result) |
| 110 | +``` |
62 | 111 |
|
63 | | -model = pymzm.Model() |
| 112 | +**Status:** |
| 113 | +```python |
| 114 | +result.status # minizinc.Status |
| 115 | +result.statistics # solver statistics dict |
| 116 | +``` |
64 | 117 |
|
65 | | -indicies = [(i, j) for i in range(v) for j in range(b)] |
66 | | -# bool if object v is in block b |
67 | | -xs = model.add_variables("x", indices=indicies, vtype=pymzm.Variable.VTYPE_BOOL) |
| 118 | +## Global constraints |
68 | 119 |
|
69 | | -for i in range(b): |
70 | | - model.add_constraint(pymzm.Expression.sum(xs[i, j] for j in range(v)) == r) |
71 | | -for i in range(v): |
72 | | - model.add_constraint(pymzm.Expression.sum(xs[j, i] for j in range(b)) == k) |
| 120 | +```python |
| 121 | +pymzm.Constraint.alldifferent(vars) |
| 122 | +pymzm.Constraint.among(vars, value, count) |
| 123 | +pymzm.Constraint.all_equal(vars) |
| 124 | +pymzm.Constraint.count(vars, value, count) |
| 125 | +pymzm.Constraint.increasing(vars) |
| 126 | +pymzm.Constraint.decreasing(vars) |
| 127 | +``` |
73 | 128 |
|
74 | | -for i in range(b): |
75 | | - for j in range(i): |
76 | | - model.add_constraint(pymzm.Expression.sum(xs[i, k] * xs[j, k] for k in range(v)) == l) |
| 129 | +## Expressions |
77 | 130 |
|
78 | | -model.set_solve_criteria(pymzm.SOLVE_SATISFY) |
| 131 | +```python |
| 132 | +pymzm.Expression.sum(xs) |
| 133 | +pymzm.Expression.AND([e1, e2, e3]) |
| 134 | +pymzm.Expression.OR([e1, e2, e3]) |
| 135 | +pymzm.Expression.forall(xs, lambda x: x > 0) |
| 136 | +pymzm.Expression.exists(xs, lambda x: x == 5) |
| 137 | +``` |
79 | 138 |
|
80 | | -gecode = minizinc.Solver.lookup("gecode") |
81 | | -result = model.solve(solver=gecode, all_solutions=False) |
| 139 | +## Constants and parameters |
82 | 140 |
|
83 | | -for i in range(v): |
84 | | - print(" ".join([str(int(result[f"x_{i}_{j}"])) for j in range(b)])) |
| 141 | +```python |
| 142 | +model.add_constant("N", 9) |
| 143 | +p = model.add_parameter("capacity", value=100) |
85 | 144 | ``` |
86 | | -outputs |
| 145 | + |
| 146 | +## Enum domains |
| 147 | + |
| 148 | +```python |
| 149 | +color = model.add_enum("Color", ["red", "green", "blue"]) |
| 150 | +x = model.add_variable("x", domain=color) |
87 | 151 | ``` |
88 | | -0 0 1 0 0 1 1 |
89 | | -0 1 0 0 1 1 0 |
90 | | -1 0 0 1 0 1 0 |
91 | | -0 0 1 1 1 0 0 |
92 | | -0 1 0 1 0 0 1 |
93 | | -1 1 1 0 0 0 0 |
94 | | -1 0 0 0 1 0 1 |
| 152 | + |
| 153 | +## Export to .mzn (optional) |
| 154 | + |
| 155 | +```python |
| 156 | +model.generate() # renders the model internally |
| 157 | +model.write("model.mzn") # writes to file for inspection or external use |
95 | 158 | ``` |
96 | 159 |
|
97 | | -### sat.py - Satisfiability |
| 160 | +Generate with debug output: |
98 | 161 | ```python |
99 | | -model = pymzm.Model() |
| 162 | +model.generate(debug=True) |
| 163 | +``` |
100 | 164 |
|
101 | | -xs = model.add_variables("x", indices=range(4), vtype=pymzm.Variable.VTYPE_BOOL) |
102 | | -model.add_constraint(pymzm.Expression.AND([ |
103 | | - xs[0] | xs[1] | ~xs[2], |
104 | | - xs[1] | xs[2] | ~xs[3], |
105 | | - xs[0] | ~xs[1] | xs[3], |
106 | | -])) |
107 | | -model.set_solve_criteria(pymzm.SOLVE_SATISFY) |
| 165 | +## Examples |
108 | 166 |
|
109 | | -gecode = minizinc.Solver.lookup("gecode") |
110 | | -result = model.solve(solver=gecode, all_solutions=False) |
| 167 | +| File | Problem | |
| 168 | +|------|---------| |
| 169 | +| [examples/intfact.py](examples/intfact.py) | Integer factorization | |
| 170 | +| [examples/nqueens.py](examples/nqueens.py) | N-Queens | |
| 171 | +| [examples/sudoku.py](examples/sudoku.py) | Sudoku | |
| 172 | +| [examples/magicsquare.py](examples/magicsquare.py) | Magic square | |
| 173 | +| [examples/bibd.py](examples/bibd.py) | Balanced Incomplete Block Design | |
| 174 | +| [examples/sat.py](examples/sat.py) | Boolean satisfiability | |
| 175 | + |
| 176 | +## Compatibility and migration |
| 177 | + |
| 178 | +- [Compatibility policy](docs/compatibility_policy.md) |
| 179 | +- [Migration notes](docs/migration_notes.md) |
| 180 | +- [Test matrix](docs/test_matrix.md) |
111 | 181 |
|
112 | | -for i in range(4): |
113 | | - print(f"x_{i} = {result[f'x_{i}']}") |
114 | | -``` |
|
0 commit comments