bugfix in decompose_mealy.py and it actually works now

other/decompose_mealy.py

@@ -5,11 +5,16 @@ from pysat.formula import CNF
 
 ### Gebruik:
 # Stap 1: pip3 install python-sat
-# Stap 2: python3 decomp-sat.py
+# Stap 2: python3 decompose_mealy.py
 
+
+###################################
+# Wat dingetjes over Mealy machines
+
+# Voorbeeld: 2n states, input-alfabet 'a' en 'b', outputs [0...n-1]
 def rick_koenders_machine(N):
-  transition_fun = {((n, False), 'a') : ((n+1) % 3, False) for n in range(N)}
+  transition_fun = {((n, False), 'a') : ((n+1) % N, False) for n in range(N)}
-  transition_fun |= {(((n+1) % 3, True), 'a') : (n % 3, True) for n in range(N)}
+  transition_fun |= {(((n+1) % N, True), 'a') : (n % N, True) for n in range(N)}
   transition_fun |= {((n, b), 'b') : (n, not b) for b in [False, True] for n in range(N)}
   output_fun = {((n, b), 'a') : n for b in [False, True] for n in range(N)}
   output_fun |= {((n, b), 'b') : 0 for b in [False, True] for n in range(N)}
@@ -29,23 +34,45 @@ def mealy_sem_q(machine, word, state):
 def mealy_sem(machine, word):
   return mealy_sem_q(machine, word, machine['initial_state'])
 
+def print_table(cell, rs, cs):
+  first_col_size = max([len(str(r)) for r in rs])
+  col_size = 1 + max([len(str(c)) for c in cs])
 
+  print(''.rjust(first_col_size), end='')
+  for c in cs:
+    print(str(c).rjust(col_size), end='')
+  print('')
+
+  for r in rs:
+    print(str(r).rjust(first_col_size), end='')
+    for c in cs:
+      print(cell(r, c).rjust(col_size), end='')
+    print('')
+
+
+################
 # Voorbeeld data
-machine = rick_koenders_machine(3)
+machine = rick_koenders_machine(4) # 8 states
 
-# L* table
+# L* table: Niet noodzakelijk volledig, werkt ook met minder data, maar ik
-rows = ['', 'a', 'aa', 'b', 'ab', 'aab', 'abaa', 'aabab']
+# weet niet wat voor garanties we dan kunnen geven. Het is sowieso maar de
-cols = ['a', 'aa', 'aaa', 'b', 'ab', 'ba']
+# vraag of de kolommen voldoende zijn als we projecteren.
+rows = ['', 'a', 'aa', 'aaa', 'aaaa', 'b', 'ab', 'aab', 'aaab']
+cols = ['a', 'aa', 'aaa', 'aaaa', 'b', 'ab', 'ba', 'abab']
 
-# We zoeken 2 componenten, grootte 5 (is minder dan 6)
+print_table(lambda r, c: str(mealy_sem(machine, r+c)), rows, cols)
+
+# We zoeken 2 componenten met gezamelijke grootte 6 (minder dan 8)
+# als de de total_size te laag is => UNSAT => duurt lang
 c = 2
-total_size = 5 # als deze te laag is => UNSAT => duurt lang
+total_size = 6
-
-os = machine['outputs'] # outputs
-rids = [i for i in range(c)] # components
 
 
+########################
+# Encodering naar logica
 print('Start encoding')
+os = machine['outputs']      # outputs
+rids = [i for i in range(c)] # components
 vpool = IDPool()
 cnf = CNF()
 
@@ -97,7 +124,7 @@ for rid in rids:
     for ry in rows:
       for rz in rows:
         # als rx R ry en ry R rz dan rx R rz
-        cnf.append([-var_rel(rid, rx, ry), -var_rel(rid, ry, rz), var_rel(rid, rx, rz)])
+        cnf.append([-var_row_rel(rid, rx, ry), -var_row_rel(rid, ry, rz), var_row_rel(rid, rx, rz)])
 
 # Constraint zodat de relaties samen alle elementen kunnen onderscheiden.
 # (Aka: the bijbehorende quotienten zijn joint-injective.)
@@ -107,6 +134,22 @@ for xi, xo in enumerate(os):
     # Tenminste een rid moet een verschil maken
     cnf.append([-var_rel(rid, xo, yo) for rid in rids])
 
+# Als outputs equivalent zijn, dan ook sommige rijen, en andersom.
+print('rel <=> row_rel')
+for rid in rids:
+  for rx in rows:
+    for ry in rows:
+      osx = [mealy_sem(machine, rx + c) for c in cols]
+      osy = [mealy_sem(machine, ry + c) for c in cols]
+      oss = list(zip(osx, osy))
+
+      # (ox1 ~ oy1 and ox2 ~ oy2 and ...) => rx ~ ry
+      cnf.append([-var_rel(rid, ox, oy) for (ox, oy) in oss] + [var_row_rel(rid, rx, ry)])
+
+      # rx ~ ry => oxi ~ oyi
+      for (ox, oy) in oss:
+        cnf.append([-var_row_rel(rid, rx, ry), var_rel(rid, ox, oy)])
+
 # De constraints die zorgen dat representanten ook echt representanten zijn.
 print('- representatives (r)')
 for rid in rids:
@@ -126,26 +169,12 @@ print('- representatives at most k')
 cnf_optim = CardEnc.atmost([var_row_rep(rid, rx) for rid in rids for rx in rows], total_size, vpool=vpool)
 cnf.extend(cnf_optim)
 
-# Als outputs equivalent zijn, dan ook sommige rijen, en andersom.
+def print_eqrel(rel, xs):
-print('rel <=> row_rel')
+  print_table(lambda r, c: 'Y' if rel(r, c) else '·', xs, xs)
-for rid in rids:
-  for rx in rows:
-    for ry in rows:
-      if ry <= rx:
-        continue
-      osx = [mealy_sem(machine, rx + c) for c in cols]
-      osy = [mealy_sem(machine, ry + c) for c in cols]
-      oss = zip(osx, osy)
-
-      # (ox1 ~ oy1 and ox2 ~ oy2 and ...) => rx ~ ry
-      cnf.append([-var_rel(rid, ox, oy) for (ox, oy) in oss] + [var_row_rel(rid, rx, ry)])
-
-      # rx ~ ry => oxi ~ oyi
-      for (ox, oy) in oss:
-        cnf.append([-var_row_rel(rid, rx, ry), var_rel(rid, ox, oy)])
 
 
-# Probleem oplossen met solver :-).
+##################################
+# Probleem oplossen met solver :-)
 print('Start solving')
 print('- copying formula')
 with Solver(bootstrap_with=cnf) as solver:
@@ -166,6 +195,14 @@ with Solver(bootstrap_with=cnf) as solver:
     if l < 0: model[-l] = False
     else: model[l] = True
 
+  for rid in rids:
+    print(f'Relation {rid}:')
+    print_eqrel(lambda x, y: model[var_rel(rid, x, y)], os)
+
+  for rid in rids:
+    print(f'Row relation {rid}:')
+    print_eqrel(lambda x, y: model[var_row_rel(rid, x, y)], rows)
+
   # print equivalence classes
   count = 0
   for rid in rids:

other/decompose_set.py

@@ -5,12 +5,13 @@ from pysat.formula import CNF
 
 ### Gebruik:
 # Stap 1: pip3 install python-sat
-# Stap 2: python3 decomp-sat.py
+# Stap 2: python3 decompose_set.py
 
 # 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
 # langzaam vb.:   n = 151, c = 4 en total_size = 15
@@ -32,7 +33,6 @@ rids = [i for i in range(c)] # components
 # c    =  1 1 1 1 1 2  2   2   2   3   2   3   3   3   4   3   4    4   4     5
 
 
-
 print('Start encoding')
 vpool = IDPool()
 cnf = CNF()
@@ -97,6 +97,7 @@ print('- representatives at most k')
 cnf_optim = CardEnc.atmost([var_rep(rid, xo) for rid in rids for xo in os], total_size, vpool=vpool)
 cnf.extend(cnf_optim)
 
+
 # Probleem oplossen met solver :-).
 print('Start solving')
 print('- copying formula')