1
Fork 0
mirror of https://git.cs.ou.nl/joshua.moerman/mealy-decompose.git synced 2025-04-29 17:57:44 +02:00

optimal decomposition of sets (boring)

This commit is contained in:
Joshua Moerman 2024-04-03 16:47:24 +02:00
parent 6b17f27fb3
commit a8bbe84173
3 changed files with 421 additions and 11 deletions

View file

@ -7,8 +7,9 @@ from pysat.formula import CNF
# Stap 1: pip3 install python-sat
# Stap 2: python3 decomp-sat.py
# TODO: Een L* tabel introduceren, en het aantal representanten van de rijen
# minimaliseren, ipv representanten an sich.
# Een verzameling X ontbinden in factoren X1 ... Xc, zodat X ⊆ X1 × ... × Xc.
# Hierbij is c een parameter (het aantal componenten), en ook het aantal
# elementen van X1 t/m Xc moet vooraf bepaald zijn, dat is 'total_size'.
# Voorbeeld data
# snel voorbeeld: n = 27, c = 3 en total_size = 9
@ -20,16 +21,16 @@ total_size = 15 # als deze te laag is => UNSAT => duurt lang
os = [i for i in range(n)] # outputs
rids = [i for i in range(c)] # components
# Optimale decompositie met slechts verzamelingen. Zie ook A000792 in de OEIS
# (voor de omkering size -> n), dit groeit met de derdemacht. Dus size is
# ongeveerde de derdemachts-wortel van n. Ik weet niet hoeveel c moet zijn.
# Ook relevant: A007600, Katona's problem en Edmonds' problem.
# n = 1 2 3 4 5 6 7-9 10-12 13-18 19-27 28-36 37-54 55-81 82-108 109-162
# ------------------------------------------------------------------------
# c =* 1 1 1 1 1 2 2 2 3 3 3 4 4 4 5
# size = 1 2 3 4 5 5 6 7 8 9 10 11 12 13 14
# Optimale decompositie met slechts verzamelingen. Zie ook A007600 (omkering
# A000792) in de OEIS, dit groeit met ongeveer O(log(n)). Ik weet niet hoeveel
# c moet(/mag) zijn. Ook relevant: Katona's problem en Edmonds' problem.
#
# *) de c is voor de grootste in het interval
# Tabel: bij elke n de optimale totale grootte (en de minimale c daarbij)
# n = 1 2 3 4 5 6 ≤9 ≤12 ≤16 ≤18 ≤29 ≤27 ≤36 ≤48 ≤54 ≤64 ≤81 ≤108 ≤144 ≤111
# -------------------------------------------------------------------------
# size = 1 2 3 4 5 5 6 7 8 8 9 9 10 11 11 12 12 13 14 15
# c = 1 1 1 1 1 2 2 2 2 3 2 3 3 3 4 3 4 4 4 5
print('Start encoding')

View file

@ -0,0 +1,314 @@
| number of components |
N | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 | best
-------------------------------------------------------------
1 | 1 | (1, 1)
2 | 2 | (2, 1)
3 | 3 | (3, 1)
4 | 4 4 | (4, 1)
5 | 5 5 | (5, 1)
6 | 6 5 | (5, 2)
7 | 7 6 6 | (6, 2)
8 | 8 6 6 | (6, 2)
9 | 9 6 | (6, 2)
10 | 10 7 7 | (7, 2)
11 | 11 7 7 | (7, 2)
12 | 12 7 7 | (7, 2)
13 | 13 8 8 8 | (8, 2)
14 | 14 8 8 8 | (8, 2)
15 | 15 8 8 8 | (8, 2)
16 | 16 8 8 8 | (8, 2)
17 | 17 9 8 | (8, 3)
18 | 18 9 8 | (8, 3)
19 | 19 9 9 9 | (9, 2)
20 | 20 9 9 9 | (9, 2)
21 | 21 10 9 9 | (9, 3)
22 | 22 10 9 9 | (9, 3)
23 | 23 10 9 9 | (9, 3)
24 | 24 10 9 9 | (9, 3)
25 | 25 10 9 | (9, 3)
26 | 26 11 9 | (9, 3)
27 | 27 11 9 | (9, 3)
28 | 28 11 10 10 10 | (10, 3)
29 | 29 11 10 10 10 | (10, 3)
30 | 30 11 10 10 10 | (10, 3)
31 | 31 12 10 10 10 | (10, 3)
32 | 32 12 10 10 10 | (10, 3)
33 | 33 12 10 10 | (10, 3)
34 | 34 12 10 10 | (10, 3)
35 | 35 12 10 10 | (10, 3)
36 | 36 12 10 10 | (10, 3)
37 | 37 13 11 11 11 | (11, 3)
38 | 38 13 11 11 11 | (11, 3)
39 | 39 13 11 11 11 | (11, 3)
40 | 40 13 11 11 11 | (11, 3)
41 | 41 13 11 11 11 | (11, 3)
42 | 42 13 11 11 11 | (11, 3)
43 | 43 14 11 11 11 | (11, 3)
44 | 44 14 11 11 11 | (11, 3)
45 | 45 14 11 11 11 | (11, 3)
46 | 46 14 11 11 11 | (11, 3)
47 | 47 14 11 11 11 | (11, 3)
48 | 48 14 11 11 11 | (11, 3)
49 | 49 14 12 11 | (11, 4)
50 | 50 15 12 11 | (11, 4)
51 | 51 15 12 11 | (11, 4)
52 | 52 15 12 11 | (11, 4)
53 | 53 15 12 11 | (11, 4)
54 | 54 15 12 11 | (11, 4)
55 | 55 15 12 12 12 12 | (12, 3)
56 | 56 15 12 12 12 12 | (12, 3)
57 | 57 16 12 12 12 12 | (12, 3)
58 | 58 16 12 12 12 12 | (12, 3)
59 | 59 16 12 12 12 12 | (12, 3)
60 | 60 16 12 12 12 12 | (12, 3)
61 | 61 16 12 12 12 12 | (12, 3)
62 | 62 16 12 12 12 12 | (12, 3)
63 | 63 16 12 12 12 12 | (12, 3)
64 | 64 16 12 12 12 12 | (12, 3)
65 | 65 17 13 12 12 | (12, 4)
66 | 66 17 13 12 12 | (12, 4)
67 | 17 13 12 12 | (12, 4)
73 | 18 13 12 | (12, 4)
81 | 18 14 12 | (12, 4)
82 | 19 14 13 13 13 | (13, 4)
91 | 20 14 13 13 13 | (13, 4)
97 | 20 14 13 13 | (13, 4)
101 | 21 15 13 13 | (13, 4)
109 | 21 15 14 14 14 14 | (14, 4)
111 | 22 15 14 14 14 14 | (14, 4)
122 | 23 15 14 14 14 14 | (14, 4)
126 | 23 16 14 14 14 14 | (14, 4)
129 | 23 16 14 14 14 | (14, 4)
133 | 24 16 14 14 14 | (14, 4)
145 | 25 16 15 14 | (14, 5)
151 | 25 17 15 14 | (14, 5)
157 | 26 17 15 14 | (14, 5)
163 | 26 17 15 15 15 15 | (15, 4)
170 | 27 17 15 15 15 15 | (15, 4)
181 | 27 18 15 15 15 15 | (15, 4)
183 | 28 18 15 15 15 15 | (15, 4)
193 | 28 18 16 15 15 | (15, 5)
197 | 29 18 16 15 15 | (15, 5)
211 | 30 18 16 15 15 | (15, 5)
217 | 30 19 16 15 | (15, 5)
226 | 31 19 16 15 | (15, 5)
241 | 32 19 16 15 | (15, 5)
244 | 32 19 16 16 16 16 16 | (16, 4)
253 | 32 20 16 16 16 16 16 | (16, 4)
257 | 33 20 17 16 16 16 | (16, 5)
273 | 34 20 17 16 16 16 | (16, 5)
289 | 34 20 17 16 16 | (16, 5)
290 | 35 20 17 16 16 | (16, 5)
295 | 35 21 17 16 16 | (16, 5)
307 | 36 21 17 16 16 | (16, 5)
321 | 36 21 18 16 16 | (16, 5)
325 | 37 21 18 17 17 17 17 | (17, 5)
343 | 38 21 18 17 17 17 17 | (17, 5)
344 | 38 22 18 17 17 17 17 | (17, 5)
362 | 39 22 18 17 17 17 17 | (17, 5)
381 | 40 22 18 17 17 17 17 | (17, 5)
385 | 40 22 18 17 17 17 | (17, 5)
393 | 40 23 18 17 17 17 | (17, 5)
401 | 41 23 19 17 17 17 | (17, 5)
421 | 42 23 19 17 17 17 | (17, 5)
433 | 42 23 19 18 17 | (17, 6)
442 | 43 23 19 18 17 | (17, 6)
449 | 43 24 19 18 17 | (17, 6)
463 | 44 24 19 18 17 | (17, 6)
485 | 45 24 19 18 17 | (17, 6)
487 | 45 24 19 18 18 18 18 18 | (18, 5)
501 | 45 24 20 18 18 18 18 18 | (18, 5)
507 | 46 24 20 18 18 18 18 18 | (18, 5)
513 | 46 25 20 18 18 18 18 | (18, 5)
530 | 47 25 20 18 18 18 18 | (18, 5)
553 | 48 25 20 18 18 18 18 | (18, 5)
577 | 49 26 20 19 18 18 | (18, 6)
601 | 50 26 20 19 18 18 | (18, 6)
626 | 51 26 21 19 18 18 | (18, 6)
649 | 51 27 21 19 18 | (18, 6)
651 | 52 27 21 19 18 | (18, 6)
677 | 53 27 21 19 18 | (18, 6)
703 | 54 27 21 19 18 | (18, 6)
730 | 55 28 21 19 19 19 19 19 | (19, 5)
751 | 55 28 22 19 19 19 19 19 | (19, 5)
757 | 56 28 22 19 19 19 19 19 | (19, 5)
769 | 56 28 22 20 19 19 19 | (19, 6)
785 | 57 28 22 20 19 19 19 | (19, 6)
811 | 57 29 22 20 19 19 19 | (19, 6)
813 | 58 29 22 20 19 19 19 | (19, 6)
842 | 59 29 22 20 19 19 19 | (19, 6)
865 | 59 29 22 20 19 19 | (19, 6)
871 | 60 29 22 20 19 19 | (19, 6)
901 | 61 30 23 20 19 19 | (19, 6)
931 | 62 30 23 20 19 19 | (19, 6)
962 | 63 30 23 20 19 19 | (19, 6)
973 | 63 30 23 20 20 20 20 20 20 | (20, 5)
993 | 64 30 23 20 20 20 20 20 20 | (20, 5)
1001 | 64 31 23 20 20 20 20 20 20 | (20, 5)
1025 | 65 31 23 21 20 20 20 20 | (20, 6)
1057 | 66 31 23 21 20 20 20 20 | (20, 6)
1081 | 66 31 24 21 20 20 20 20 | (20, 6)
1090 | 31 24 21 20 20 20 20 | (20, 6)
1101 | 32 24 21 20 20 20 20 | (20, 6)
1153 | 32 24 21 20 20 20 | (20, 6)
1211 | 33 24 21 20 20 20 | (20, 6)
1281 | 33 24 22 20 20 20 | (20, 6)
1297 | 33 25 22 21 20 | (20, 7)
1332 | 34 25 22 21 20 | (20, 7)
1453 | 35 25 22 21 20 | (20, 7)
1459 | 35 25 22 21 21 21 21 21 | (21, 6)
1513 | 35 26 22 21 21 21 21 21 | (21, 6)
1537 | 35 26 22 21 21 21 21 | (21, 6)
1585 | 36 26 22 21 21 21 21 | (21, 6)
1601 | 36 26 23 21 21 21 21 | (21, 6)
1729 | 37 26 23 22 21 21 | (21, 7)
1765 | 37 27 23 22 21 21 | (21, 7)
1873 | 38 27 23 22 21 21 | (21, 7)
1945 | 38 27 23 22 21 | (21, 7)
2001 | 38 27 24 22 21 | (21, 7)
2029 | 39 27 24 22 21 | (21, 7)
2059 | 39 28 24 22 21 | (21, 7)
2188 | 39 28 24 22 22 22 22 22 | (22, 6)
2198 | 40 28 24 22 22 22 22 22 | (22, 6)
2305 | 40 28 24 23 22 22 22 | (22, 7)
2367 | 41 28 24 23 22 22 22 | (22, 7)
2402 | 41 29 24 23 22 22 22 | (22, 7)
2501 | 41 29 25 23 22 22 22 | (22, 7)
2549 | 42 29 25 23 22 22 22 | (22, 7)
2593 | 42 29 25 23 22 22 | (22, 7)
2745 | 43 30 25 23 22 22 | (22, 7)
2917 | 43 30 25 23 23 23 23 23 23 | (23, 6)
2941 | 44 30 25 23 23 23 23 23 23 | (23, 6)
3073 | 44 30 25 24 23 23 23 23 | (23, 7)
3126 | 44 30 26 24 23 23 23 23 | (23, 7)
3137 | 44 31 26 24 23 23 23 23 | (23, 7)
3151 | 45 31 26 24 23 23 23 23 | (23, 7)
3376 | 46 31 26 24 23 23 23 23 | (23, 7)
3457 | 46 31 26 24 23 23 23 | (23, 7)
3585 | 46 32 26 24 23 23 23 | (23, 7)
3601 | 47 32 26 24 23 23 23 | (23, 7)
3751 | 47 32 27 24 23 23 23 | (23, 7)
3841 | 48 32 27 24 23 23 23 | (23, 7)
3889 | 48 32 27 24 24 23 | (23, 8)
4097 | 49 33 27 25 24 23 | (23, 8)
4353 | 50 33 27 25 24 23 | (23, 8)
4375 | 50 33 27 25 24 24 24 24 24 | (24, 7)
4501 | 50 33 28 25 24 24 24 24 24 | (24, 7)
4609 | 50 34 28 25 24 24 24 24 | (24, 7)
4625 | 51 34 28 25 24 24 24 24 | (24, 7)
4914 | 52 34 28 25 24 24 24 24 | (24, 7)
5121 | 52 34 28 26 24 24 24 24 | (24, 7)
5185 | 52 35 28 26 25 24 24 | (24, 8)
5203 | 53 35 28 26 25 24 24 | (24, 8)
5401 | 53 35 29 26 25 24 24 | (24, 8)
5509 | 54 35 29 26 25 24 24 | (24, 8)
5833 | 55 36 29 26 25 24 | (24, 8)
6157 | 56 36 29 26 25 24 | (24, 8)
6401 | 56 36 29 27 25 24 | (24, 8)
6481 | 56 36 30 27 25 24 | (24, 8)
6499 | 57 36 30 27 25 24 | (24, 8)
6562 | 57 37 30 27 25 25 25 25 25 | (25, 7)
6860 | 58 37 30 27 25 25 25 25 25 | (25, 7)
6913 | 58 37 30 27 26 25 25 25 | (25, 8)
7221 | 59 37 30 27 26 25 25 25 | (25, 8)
7291 | 59 38 30 27 26 25 25 25 | (25, 8)
7601 | 60 38 30 27 26 25 25 25 | (25, 8)
7777 | 60 38 31 27 26 25 25 | (25, 8)
8001 | 61 38 31 28 26 25 25 | (25, 8)
8101 | 61 39 31 28 26 25 25 | (25, 8)
8401 | 62 39 31 28 26 25 25 | (25, 8)
8749 | 62 39 31 28 26 26 26 26 26 26 | (26, 7)
8821 | 63 39 31 28 26 26 26 26 26 26 | (26, 7)
9001 | 63 40 31 28 26 26 26 26 26 26 | (26, 7)
9073 | 63 40 32 28 26 26 26 26 26 26 | (26, 7)
9217 | 63 40 32 28 27 26 26 26 26 | (26, 8)
9262 | 64 40 32 28 27 26 26 26 26 | (26, 8)
9703 | 65 40 32 28 27 26 26 26 26 | (26, 8)
10001 | 65 41 32 29 27 26 26 26 26 | (26, 8)
10165 | 66 41 32 29 27 26 26 26 26 | (26, 8)
10369 | 66 41 32 29 27 26 26 26 | (26, 8)
10585 | 66 41 33 29 27 26 26 26 | (26, 8)
10649 | 41 33 29 27 26 26 26 | (26, 8)
11001 | 42 33 29 27 26 26 26 | (26, 8)
11665 | 42 33 29 27 27 26 | (26, 9)
12101 | 43 33 29 27 27 26 | (26, 9)
12289 | 43 33 29 28 27 26 | (26, 9)
12349 | 43 34 29 28 27 26 | (26, 9)
12501 | 43 34 30 28 27 26 | (26, 9)
13123 | 43 34 30 28 27 27 27 27 27 | (27, 8)
13311 | 44 34 30 28 27 27 27 27 27 | (27, 8)
13825 | 44 34 30 28 27 27 27 27 | (27, 8)
14407 | 44 35 30 28 27 27 27 27 | (27, 8)
14642 | 45 35 30 28 27 27 27 27 | (27, 8)
15553 | 45 35 30 28 28 27 27 | (27, 9)
15626 | 45 35 31 28 28 27 27 | (27, 9)
15973 | 46 35 31 28 28 27 27 | (27, 9)
16385 | 46 35 31 29 28 27 27 | (27, 9)
16808 | 46 36 31 29 28 27 27 | (27, 9)
17425 | 47 36 31 29 28 27 27 | (27, 9)
17497 | 47 36 31 29 28 27 | (27, 9)
18751 | 47 36 32 29 28 27 | (27, 9)
19009 | 48 36 32 29 28 27 | (27, 9)
19209 | 48 37 32 29 28 27 | (27, 9)
19684 | 48 37 32 29 28 28 28 28 28 | (28, 8)
20481 | 48 37 32 30 28 28 28 28 28 | (28, 8)
20737 | 49 37 32 30 29 28 28 28 | (28, 9)
21953 | 49 38 32 30 29 28 28 28 | (28, 9)
22465 | 50 38 32 30 29 28 28 28 | (28, 9)
22501 | 50 38 33 30 29 28 28 28 | (28, 9)
23329 | 50 38 33 30 29 28 28 | (28, 9)
24337 | 51 38 33 30 29 28 28 | (28, 9)
25089 | 51 39 33 30 29 28 28 | (28, 9)
25601 | 51 39 33 31 29 28 28 | (28, 9)
26245 | 51 39 33 31 29 29 29 29 29 29 | (29, 8)
26365 | 52 39 33 31 29 29 29 29 29 29 | (29, 8)
27001 | 52 39 34 31 29 29 29 29 29 29 | (29, 8)
27649 | 52 39 34 31 30 29 29 29 29 | (29, 9)
28562 | 53 39 34 31 30 29 29 29 29 | (29, 9)
28673 | 53 40 34 31 30 29 29 29 29 | (29, 9)
30759 | 54 40 34 31 30 29 29 29 29 | (29, 9)
31105 | 54 40 34 31 30 29 29 29 | (29, 9)
32001 | 54 40 34 32 30 29 29 29 | (29, 9)
32401 | 54 40 35 32 30 29 29 29 | (29, 9)
32769 | 54 41 35 32 30 29 29 29 | (29, 9)
33125 | 55 41 35 32 30 29 29 29 | (29, 9)
34993 | 55 41 35 32 30 30 29 | (29, 10)
35673 | 56 41 35 32 30 30 29 | (29, 10)
36865 | 56 42 35 32 31 30 29 | (29, 10)
38417 | 57 42 35 32 31 30 29 | (29, 10)
38881 | 57 42 36 32 31 30 29 | (29, 10)
39367 | 57 42 36 32 31 30 30 30 30 30 | (30, 9)
40001 | 57 42 36 33 31 30 30 30 30 30 | (30, 9)
41161 | 58 42 36 33 31 30 30 30 30 30 | (30, 9)
41473 | 58 43 36 33 31 30 30 30 30 | (30, 9)
44101 | 59 43 36 33 31 30 30 30 30 | (30, 9)
46657 | 59 44 37 33 31 31 30 30 | (30, 10)
47251 | 60 44 37 33 31 31 30 30 | (30, 10)
49153 | 60 44 37 33 32 31 30 30 | (30, 10)
50001 | 60 44 37 34 32 31 30 30 | (30, 10)
50626 | 61 44 37 34 32 31 30 30 | (30, 10)
52489 | 61 45 37 34 32 31 30 | (30, 10)
54001 | 62 45 37 34 32 31 30 | (30, 10)
54433 | 62 45 38 34 32 31 30 | (30, 10)
57601 | 63 45 38 34 32 31 30 | (30, 10)
59050 | 63 46 38 34 32 31 31 31 31 31 | (31, 9)
61441 | 64 46 38 34 32 31 31 31 31 31 | (31, 9)
62209 | 64 46 38 34 32 32 31 31 31 | (31, 10)
62501 | 64 46 38 35 32 32 31 31 31 | (31, 10)
63505 | 64 46 39 35 32 32 31 31 31 | (31, 10)
65537 | 65 46 39 35 33 32 31 31 31 | (31, 10)
65611 | 65 47 39 35 33 32 31 31 31 | (31, 10)
69633 | 66 47 39 35 33 32 31 31 31 | (31, 10)
69985 | 66 47 39 35 33 32 31 31 | (31, 10)
72901 | 66 48 39 35 33 32 31 31 | (31, 10)
73985 | 48 39 35 33 32 31 31 | (31, 10)
74089 | 48 40 35 33 32 31 31 | (31, 10)
78126 | 48 40 36 33 32 31 31 | (31, 10)
78733 | 48 40 36 33 32 32 32 32 32 32 | (32, 9)
81001 | 49 40 36 33 32 32 32 32 32 32 | (32, 9)
81921 | 49 40 36 34 32 32 32 32 32 32 | (32, 9)
82945 | 49 40 36 34 33 32 32 32 32 | (32, 10)
86437 | 49 41 36 34 33 32 32 32 32 | (32, 10)
90001 | 50 41 36 34 33 32 32 32 32 | (32, 10)
93313 | 50 41 36 34 33 32 32 32 | (32, 10)
93751 | 50 41 37 34 33 32 32 32 | (32, 10)

95
other/partitions.py Normal file
View file

@ -0,0 +1,95 @@
from math import prod
# bounds
N = 99999
C = 16
# precondition k <= n
def all_partitions_(n, k):
if n == 0:
return [[]]
acc = []
for j in range(1, k+1):
ps = all_partitions_(n-j, min(n-j, j))
acc.extend([[j]+p for p in ps])
return acc
def all_partitions(n):
return all_partitions_(n, n)
def highest_product(n):
ps = all_partitions(n)
highest_prod = {}
for p in ps:
if len(p) > C:
continue
v = prod(p)
if len(p) not in highest_prod:
highest_prod[len(p)] = v
else:
if v > highest_prod[len(p)]:
highest_prod[len(p)] = v
return highest_prod
def tabulate(upper):
highest_n_per_c = {}
table = {}
for s in range(1, upper+1):
res = highest_product(s)
for c, n in res.items():
for n2 in range(highest_n_per_c.get(c, 0)+1, min(n, N)+1):
table[(n2, c)] = s
highest_n_per_c[c] = n
return {(n, c): s for (n, c), s in table.items() if s <= n}
def trim_tab(tab):
best_s = {}
best_c = {}
for (n, c), s in tab.items():
if n not in best_s:
best_s[n] = s
best_c[n] = c
if s < best_s[n]:
best_s[n] = s
best_c[n] = c
return {(n, c): s for (n, c), s in tab.items() if c <= best_c[n] or s <= best_s[n]}
def print_table(tab0):
tab = trim_tab(tab0)
col_width = {0: 1} | {c: len(str(c)) for (_, c) in tab.keys()}
for (n, c), s in tab.items():
col_width[0] = max(col_width[0], len(str(n)))
col_width[c] = max(col_width[c], len(str(s)))
N = max([n for (n, _) in tab.keys()])
C = max([c for (_, c) in tab.keys()])
prev_row = ''
for n in range(1, N+1):
best = None
row = ''
for c in range(1, C+1):
if (n, c) in tab:
row += ' ' + str(tab[(n, c)]).rjust(col_width[c])
if not best or tab[(n, c)] < best[0]:
best = (tab[(n, c)], c)
else:
row += ' ' + ''.rjust(col_width[c])
if row != prev_row:
print(str(n).rjust(col_width[0]) + ' |' + row + ' | ' + str(best))
prev_row = row