Skip to content

Commit 1550377

Browse files
niklasdewallyniklasdewally
committed
Convert weighted sums to Minion
Add FlatWeightedSumGeq and FlatWeightedSumLeq Minion constraints, and introduce_weightedsumleq_sumgeq rule to convert weighted sums to Minion via these constraints. DETAILS This rule is a bit unusual compared to other introduction rules in that it does its own flattening. For example, introduce_sumleq only accepts sums of atoms and relies on the generic flattening rules (flatten_binop / flatten_vecop) to run before it flattens the sum. ``` a + (b*c) + (d*e) <= 10 ~~> flatten_vecop a + __0 + __1 <= 10 with new top level constraints __0 =aux b*c __1 =aux d*e --- a + __0 + __1 <= 10 ~~> introduce_sumleq flat_sumleq([a,__0,__1],10) ... ``` However, weighted sums are expressed as sums of products, which are not flat. Flattening a weighted sum generically makes it indistinguishable from a sum: ``` 1*a + 2*b + 3*c + d <= 10 ~~> flatten_vecop __0 + __1 + __2 + d <= 10 with new top level constraints __0 =aux 1*a __1 =aux 2*b __2 =aux 3*c ``` Therefore, introduce_weightedsumleq_sumgeq does its own flattening, and has a higher priority than flatten_vecop to prevent weighted sums being generically flattened. Having custom flattening semantics means that we can make more things weighted sums. For example, consider `a + 2*b + 3*c*d + (e / f) + 5*(g/h) <= 18`. This rule turns this into a single `flat_weightedsumleq` constraint: ``` a + 2*b + 3*c*d + (e/f) + 5*(g/h) <= 30 ~> introduce_weightedsumleq_sumgeq flat_weightedsumleq([1,2,3,1,5],[a,b,__0,__1,__2],30) with new top level constraints __0 = c*d __1 = e/f __2 = g/h ``` The rules to turn terms into coefficient variable pairs are the following: 1. Non-weighted atom: `a ~> (1,a)` 2. Other non-weighted term: `e ~> (1,__0), with new constraint __0 =aux e` 3. Weighted atom: `c*a ~> (c,a)` 4. Weighted non-atom: `c*e ~> (c,__0) with new constraint __0 =aux e` 5. Weighted product: `c*e*f ~> (c,__0) with new constraint __0 =aux (e*f)`
1 parent 0725be8 commit 1550377

40 files changed

+18685
-476
lines changed

‎conjure_oxide/tests/integration/basic/weighted-sum/01-simple/config.toml ‎conjure_oxide/tests/integration/basic/weighted-sum/01-simple-lt/config.toml

File renamed without changes.

‎conjure_oxide/tests/integration/basic/weighted-sum/01-simple-lt/input-expected-rule-trace-human.txt

+24
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
Sum([Sum([Product([2, x]), Product([3, y])]), z]),
2+
~~> normalise_associative_commutative ([("Base", 8900)])
3+
Sum([Product([2, x]), Product([3, y]), z])
4+
5+
--
6+
7+
(Sum([Product([2, x]), Product([3, y]), z]) < 14),
8+
~~> lt_to_leq ([("Minion", 8400)])
9+
(Sum([Product([2, x]), Product([3, y]), z]) <= Sum([14, -1]))
10+
11+
--
12+
13+
Sum([14, -1]),
14+
~~> apply_eval_constant ([("Constant", 9001)])
15+
13
16+
17+
--
18+
19+
(Sum([Product([2, x]), Product([3, y]), z]) <= 13),
20+
~~> introduce_weighted_sumleq_sumgeq ([("Minion", 4500)])
21+
FlatWeightedSumLeq([2, 3, 1],[x, y, z],13)
22+
23+
--
24+

‎conjure_oxide/tests/integration/basic/weighted-sum/01-simple/input.eprime ‎conjure_oxide/tests/integration/basic/weighted-sum/01-simple-lt/input.eprime

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
11
find x,y,z: int(2..4)
22
such that
33

4-
(2*x) + (3*y) < 12
4+
(2*x) + (3*y) + z < 14

‎conjure_oxide/tests/integration/basic/weighted-sum/01-simple-lt/input.expected-minion.solutions.json

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
[
2+
{
3+
"x": 2,
4+
"y": 2,
5+
"z": 2
6+
},
7+
{
8+
"x": 2,
9+
"y": 2,
10+
"z": 3
11+
}
12+
]

‎conjure_oxide/tests/integration/basic/weighted-sum/01-simple-lt/input.expected-parse.serialised.json

+184
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,184 @@
1+
{
2+
"constraints": [
3+
{
4+
"Lt": [
5+
{
6+
"clean": false,
7+
"etype": null
8+
},
9+
{
10+
"Sum": [
11+
{
12+
"clean": false,
13+
"etype": null
14+
},
15+
[
16+
{
17+
"Sum": [
18+
{
19+
"clean": false,
20+
"etype": null
21+
},
22+
[
23+
{
24+
"Product": [
25+
{
26+
"clean": false,
27+
"etype": null
28+
},
29+
[
30+
{
31+
"Atomic": [
32+
{
33+
"clean": false,
34+
"etype": null
35+
},
36+
{
37+
"Literal": {
38+
"Int": 2
39+
}
40+
}
41+
]
42+
},
43+
{
44+
"Atomic": [
45+
{
46+
"clean": false,
47+
"etype": null
48+
},
49+
{
50+
"Reference": {
51+
"UserName": "x"
52+
}
53+
}
54+
]
55+
}
56+
]
57+
]
58+
},
59+
{
60+
"Product": [
61+
{
62+
"clean": false,
63+
"etype": null
64+
},
65+
[
66+
{
67+
"Atomic": [
68+
{
69+
"clean": false,
70+
"etype": null
71+
},
72+
{
73+
"Literal": {
74+
"Int": 3
75+
}
76+
}
77+
]
78+
},
79+
{
80+
"Atomic": [
81+
{
82+
"clean": false,
83+
"etype": null
84+
},
85+
{
86+
"Reference": {
87+
"UserName": "y"
88+
}
89+
}
90+
]
91+
}
92+
]
93+
]
94+
}
95+
]
96+
]
97+
},
98+
{
99+
"Atomic": [
100+
{
101+
"clean": false,
102+
"etype": null
103+
},
104+
{
105+
"Reference": {
106+
"UserName": "z"
107+
}
108+
}
109+
]
110+
}
111+
]
112+
]
113+
},
114+
{
115+
"Atomic": [
116+
{
117+
"clean": false,
118+
"etype": null
119+
},
120+
{
121+
"Literal": {
122+
"Int": 14
123+
}
124+
}
125+
]
126+
}
127+
]
128+
}
129+
],
130+
"next_var": 0,
131+
"variables": [
132+
[
133+
{
134+
"UserName": "x"
135+
},
136+
{
137+
"domain": {
138+
"IntDomain": [
139+
{
140+
"Bounded": [
141+
2,
142+
4
143+
]
144+
}
145+
]
146+
}
147+
}
148+
],
149+
[
150+
{
151+
"UserName": "y"
152+
},
153+
{
154+
"domain": {
155+
"IntDomain": [
156+
{
157+
"Bounded": [
158+
2,
159+
4
160+
]
161+
}
162+
]
163+
}
164+
}
165+
],
166+
[
167+
{
168+
"UserName": "z"
169+
},
170+
{
171+
"domain": {
172+
"IntDomain": [
173+
{
174+
"Bounded": [
175+
2,
176+
4
177+
]
178+
}
179+
]
180+
}
181+
}
182+
]
183+
]
184+
}

‎conjure_oxide/tests/integration/basic/weighted-sum/01-simple-lt/input.expected-rewrite.serialised.json

+99
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,99 @@
1+
{
2+
"constraints": [
3+
{
4+
"FlatWeightedSumLeq": [
5+
{
6+
"clean": false,
7+
"etype": null
8+
},
9+
[
10+
{
11+
"Int": 2
12+
},
13+
{
14+
"Int": 3
15+
},
16+
{
17+
"Int": 1
18+
}
19+
],
20+
[
21+
{
22+
"Reference": {
23+
"UserName": "x"
24+
}
25+
},
26+
{
27+
"Reference": {
28+
"UserName": "y"
29+
}
30+
},
31+
{
32+
"Reference": {
33+
"UserName": "z"
34+
}
35+
}
36+
],
37+
{
38+
"Literal": {
39+
"Int": 13
40+
}
41+
}
42+
]
43+
}
44+
],
45+
"next_var": 0,
46+
"variables": [
47+
[
48+
{
49+
"UserName": "x"
50+
},
51+
{
52+
"domain": {
53+
"IntDomain": [
54+
{
55+
"Bounded": [
56+
2,
57+
4
58+
]
59+
}
60+
]
61+
}
62+
}
63+
],
64+
[
65+
{
66+
"UserName": "y"
67+
},
68+
{
69+
"domain": {
70+
"IntDomain": [
71+
{
72+
"Bounded": [
73+
2,
74+
4
75+
]
76+
}
77+
]
78+
}
79+
}
80+
],
81+
[
82+
{
83+
"UserName": "z"
84+
},
85+
{
86+
"domain": {
87+
"IntDomain": [
88+
{
89+
"Bounded": [
90+
2,
91+
4
92+
]
93+
}
94+
]
95+
}
96+
}
97+
]
98+
]
99+
}

0 commit comments

Comments
 (0)