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

more formatting

Browse source
This commit is contained in:
Joshua Moerman 2024-06-14 14:09:18 +02:00
parent 353d191c0c
commit 8223ff9d59
6 changed files with 100 additions and 58 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
.ruff.toml Normal file
View file

@ -0,0 +1,8 @@
indent-width = 2
line-length = 320
[format]
quote-style = "single"
[lint]
ignore = ["E741"]

41
other/decompose_fsm.py
View file

@ -10,11 +10,11 @@ import argparse
# Stap 1: pip3 install python-sat # Stap 1: pip3 install python-sat
# Stap 2: python3 decompose_fsm.py -h # Stap 2: python3 decompose_fsm.py -h
parser = argparse.ArgumentParser(description="Decomposes a FSM into smaller components by remapping its outputs. Uses a SAT solver.") parser = argparse.ArgumentParser(description='Decomposes a FSM into smaller components by remapping its outputs. Uses a SAT solver.')
parser.add_argument('-c', '--components', type=int, default=2, help='number of components') parser.add_argument('-c', '--components', type=int, default=2, help='number of components')
parser.add_argument('-n', '--total-size', type=int, help='total number of states of the components') parser.add_argument('-n', '--total-size', type=int, help='total number of states of the components')
parser.add_argument('--add-state-trans', default=False, action="store_true", help='adds state transitivity constraints') parser.add_argument('--add-state-trans', default=False, action='store_true', help='adds state transitivity constraints')
parser.add_argument('-v', '--verbose', default=False, action="store_true", help='prints more info') parser.add_argument('-v', '--verbose', default=False, action='store_true', help='prints more info')
parser.add_argument('filename', help='path to .dot file') parser.add_argument('filename', help='path to .dot file')
args = parser.parse_args() args = parser.parse_args()
@ -22,7 +22,7 @@ args = parser.parse_args()
c = args.components c = args.components
total_size = args.total_size total_size = args.total_size
assert c >= 1 # c = 1 is zinloos, maar zou moeten werken assert c >= 1 # c = 1 is zinloos, maar zou moeten werken
assert total_size >= c # elk component heeft tenminste 1 state assert total_size >= c # elk component heeft tenminste 1 state
@ -46,6 +46,7 @@ class FSM:
def output(self, s, a): def output(self, s, a):
return self.output_map[(s, a)] return self.output_map[(s, a)]
def parse_dot_file(lines): def parse_dot_file(lines):
def parse_transition(line): def parse_transition(line):
(l, _, r) = line.partition('->') (l, _, r) = line.partition('->')
@ -83,6 +84,7 @@ def parse_dot_file(lines):
return FSM(initial_state, states, inputs, outputs, transition_map, output_map) return FSM(initial_state, states, inputs, outputs, transition_map, output_map)
with open(args.filename) as file: with open(args.filename) as file:
machine = parse_dot_file(file) machine = parse_dot_file(file)
if args.verbose: if args.verbose:
@ -94,6 +96,7 @@ print(f'Initial size: {len(machine.states)}')
################################### ###################################
# Utility functions # Utility functions
def print_table(cell, rs, cs): def print_table(cell, rs, cs):
first_col_size = max([len(str(r)) for r in rs]) first_col_size = max([len(str(r)) for r in rs])
col_size = 1 + max([len(str(c)) for c in cs] + [len(cell(r, c)) for c in cs for r in rs]) col_size = 1 + max([len(str(c)) for c in cs] + [len(cell(r, c)) for c in cs for r in rs])
@ -109,6 +112,7 @@ def print_table(cell, rs, cs):
print(cell(r, c).rjust(col_size), end='') print(cell(r, c).rjust(col_size), end='')
print('') print('')
class Progress: class Progress:
def __init__(self, name, guess): def __init__(self, name, guess):
self.reset(name, guess, show=False) self.reset(name, guess, show=False)
@ -131,23 +135,27 @@ class Progress:
print(f'{self.percentage}%', end='', flush=True) print(f'{self.percentage}%', end='', flush=True)
print('\r', end='') print('\r', end='')
progress = Progress('', 1) progress = Progress('', 1)
######################## ########################
# Encodering naar logica # Encodering naar logica
print('Start encoding') print('Start encoding')
os = list(machine.outputs) # outputs os = list(machine.outputs) # outputs
rids = [i for i in range(c)] # components rids = [i for i in range(c)] # components
vpool = IDPool() vpool = IDPool()
cnf = CNF() cnf = CNF()
# Een hulp variabele voor False en True, maakt de andere variabelen eenvoudiger # Een hulp variabele voor False en True, maakt de andere variabelen eenvoudiger
def var_const(b): def var_const(b):
return(vpool.id(('const', b))) return vpool.id(('const', b))
cnf.append([var_const(True)]) cnf.append([var_const(True)])
cnf.append([-var_const(False)]) cnf.append([-var_const(False)])
# Voor elke relatie en elke twee elementen o1 en o2, is er een variabele die # Voor elke relatie en elke twee elementen o1 en o2, is er een variabele die
# aangeeft of o1 en o2 gerelateerd zijn. Er is 1 variabele voor xRy en yRx, dus # aangeeft of o1 en o2 gerelateerd zijn. Er is 1 variabele voor xRy en yRx, dus
# symmetrie is al ingebouwd. Reflexiviteit is ook ingebouwd. # symmetrie is al ingebouwd. Reflexiviteit is ook ingebouwd.
@ -156,7 +164,8 @@ def var_rel(rid, o1, o2):
return var_const(True) return var_const(True)
[so1, so2] = sorted([o1, o2]) [so1, so2] = sorted([o1, o2])
return(vpool.id(('rel', rid, so1, so2))) return vpool.id(('rel', rid, so1, so2))
# De relatie op outputs geeft een relaties op states. Deze relatie moet ook een # De relatie op outputs geeft een relaties op states. Deze relatie moet ook een
# bisimulatie zijn. # bisimulatie zijn.
@ -165,12 +174,14 @@ def var_state_rel(rid, s1, s2):
return var_const(True) return var_const(True)
[ss1, ss2] = sorted([s1, s2]) [ss1, ss2] = sorted([s1, s2])
return(vpool.id(('state_rel', rid, ss1, ss2))) return vpool.id(('state_rel', rid, ss1, ss2))
# Voor elke relatie, en elke equivalentie-klasse, kiezen we precies 1 state # Voor elke relatie, en elke equivalentie-klasse, kiezen we precies 1 state
# als representant. Deze variabele geeft aan welk element. # als representant. Deze variabele geeft aan welk element.
def var_state_rep(rid, s): def var_state_rep(rid, s):
return(vpool.id(('state_rep', rid, s))) return vpool.id(('state_rep', rid, s))
# Contraints zodat de relatie een equivalentie relatie is. We hoeven alleen # Contraints zodat de relatie een equivalentie relatie is. We hoeven alleen
# maar transitiviteit te encoderen, want refl en symm zijn ingebouwd in de var. # maar transitiviteit te encoderen, want refl en symm zijn ingebouwd in de var.
@ -197,7 +208,7 @@ if args.add_state_trans:
# (Aka: the bijbehorende quotienten zijn joint-injective.) # (Aka: the bijbehorende quotienten zijn joint-injective.)
progress.reset('injectivity', guess=len(os) * (len(os) - 1) / 2) progress.reset('injectivity', guess=len(os) * (len(os) - 1) / 2)
for xi, xo in enumerate(os): for xi, xo in enumerate(os):
for yo in os[xi+1:]: for yo in os[xi + 1 :]:
# Tenminste een rid moet een verschil maken # Tenminste een rid moet een verschil maken
cnf.append([-var_rel(rid, xo, yo) for rid in rids]) cnf.append([-var_rel(rid, xo, yo) for rid in rids])
progress.add() progress.add()
@ -229,7 +240,7 @@ for rid in rids:
# Belangrijkste: een element is een representant, of equivalent met een # Belangrijkste: een element is een representant, of equivalent met een
# eerder element. We forceren hiermee dat de solver representanten moet # eerder element. We forceren hiermee dat de solver representanten moet
# kiezen (voor aan de lijst). # kiezen (voor aan de lijst).
cnf.append([var_state_rep(rid, sx)] + [var_state_rel(rid, sx, sy) for sy in states[:ix]] ) cnf.append([var_state_rep(rid, sx)] + [var_state_rel(rid, sx, sy) for sy in states[:ix]])
for sy in states[:ix]: for sy in states[:ix]:
# rx en ry kunnen niet beide een representant zijn, tenzij ze # rx en ry kunnen niet beide een representant zijn, tenzij ze
@ -244,6 +255,7 @@ print('size constraints')
cnf_optim = CardEnc.atmost([var_state_rep(rid, sx) for rid in rids for sx in machine.states], total_size, vpool=vpool) cnf_optim = CardEnc.atmost([var_state_rep(rid, sx) for rid in rids for sx in machine.states], total_size, vpool=vpool)
cnf.extend(cnf_optim) cnf.extend(cnf_optim)
def print_eqrel(rel, xs): def print_eqrel(rel, xs):
print_table(lambda r, c: 'Y' if rel(r, c) else '·', xs, xs) print_table(lambda r, c: 'Y' if rel(r, c) else '·', xs, xs)
@ -261,15 +273,14 @@ with Solver(bootstrap_with=cnf) as solver:
print('unsat :-(') print('unsat :-(')
exit() exit()
print(f'sat :-)') print('sat :-)')
# Even omzetten in een makkelijkere data structuur # Even omzetten in een makkelijkere data structuur
print('- get model') print('- get model')
m = solver.get_model() m = solver.get_model()
model = {} model = {}
for l in m: for l in m:
if l < 0: model[-l] = False model[abs(l)] = l > 0
else: model[l] = True
if args.verbose: if args.verbose:
for rid in rids: for rid in rids:

48
other/decompose_observation_table.py
View file

@ -11,18 +11,20 @@ from pysat.formula import CNF
################################### ###################################
# Wat dingetjes over Mealy machines # Wat dingetjes over Mealy machines
# Voorbeeld: 2n states, input-alfabet 'a' en 'b', outputs [0...n-1] # Voorbeeld: 2n states, input-alfabet 'a' en 'b', outputs [0...n-1]
def rick_koenders_machine(N): def rick_koenders_machine(N):
transition_fun = {((n, False), 'a') : ((n+1) % N, False) for n in range(N)} transition_fun = {((n, False), 'a'): ((n + 1) % N, False) for n in range(N)}
transition_fun |= {(((n+1) % N, True), 'a') : (n % N, 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)} 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), '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)} output_fun |= {((n, b), 'b'): 0 for b in [False, True] for n in range(N)}
initial_state = (0, False) initial_state = (0, False)
inputs = ['a', 'b'] inputs = ['a', 'b']
outputs = [n for n in range(N)] outputs = [n for n in range(N)]
return {'transition_fun': transition_fun, 'output_fun': output_fun, 'initial_state': initial_state, 'inputs': inputs, 'outputs': outputs} return {'transition_fun': transition_fun, 'output_fun': output_fun, 'initial_state': initial_state, 'inputs': inputs, 'outputs': outputs}
def mealy_sem_q(machine, word, state): def mealy_sem_q(machine, word, state):
if len(word) == 0: if len(word) == 0:
return None return None
@ -31,9 +33,11 @@ def mealy_sem_q(machine, word, state):
else: else:
return mealy_sem_q(machine, word[1:], machine['transition_fun'][(state, word[0])]) return mealy_sem_q(machine, word[1:], machine['transition_fun'][(state, word[0])])
def mealy_sem(machine, word): def mealy_sem(machine, word):
return mealy_sem_q(machine, word, machine['initial_state']) return mealy_sem_q(machine, word, machine['initial_state'])
def print_table(cell, rs, cs): def print_table(cell, rs, cs):
first_col_size = max([len(str(r)) for r in rs]) first_col_size = max([len(str(r)) for r in rs])
col_size = 1 + max([len(str(c)) for c in cs]) col_size = 1 + max([len(str(c)) for c in cs])
@ -52,7 +56,7 @@ def print_table(cell, rs, cs):
################ ################
# Voorbeeld data # Voorbeeld data
machine = rick_koenders_machine(4) # 8 states machine = rick_koenders_machine(4) # 8 states
# L* table: Niet noodzakelijk volledig, werkt ook met minder data, maar ik # L* table: Niet noodzakelijk volledig, werkt ook met minder data, maar ik
# weet niet wat voor garanties we dan kunnen geven. Het is sowieso maar de # weet niet wat voor garanties we dan kunnen geven. Het is sowieso maar de
@ -60,7 +64,7 @@ machine = rick_koenders_machine(4) # 8 states
rows = ['', 'a', 'aa', 'aaa', 'aaaa', 'b', 'ab', 'aab', 'aaab'] rows = ['', 'a', 'aa', 'aaa', 'aaaa', 'b', 'ab', 'aab', 'aaab']
cols = ['a', 'aa', 'aaa', 'aaaa', 'b', 'ab', 'ba', 'abab'] cols = ['a', 'aa', 'aaa', 'aaaa', 'b', 'ab', 'ba', 'abab']
print_table(lambda r, c: str(mealy_sem(machine, r+c)), rows, cols) print_table(lambda r, c: str(mealy_sem(machine, r + c)), rows, cols)
# We zoeken 2 componenten met gezamelijke grootte 6 (minder dan 8) # We zoeken 2 componenten met gezamelijke grootte 6 (minder dan 8)
# als de de total_size te laag is => UNSAT => duurt lang # als de de total_size te laag is => UNSAT => duurt lang
@ -71,18 +75,21 @@ total_size = 6
######################## ########################
# Encodering naar logica # Encodering naar logica
print('Start encoding') print('Start encoding')
os = machine['outputs'] # outputs os = machine['outputs'] # outputs
rids = [i for i in range(c)] # components rids = [i for i in range(c)] # components
vpool = IDPool() vpool = IDPool()
cnf = CNF() cnf = CNF()
# Een hulp variabele voor False en True, maakt de andere variabelen eenvoudiger # Een hulp variabele voor False en True, maakt de andere variabelen eenvoudiger
def var_const(b): def var_const(b):
return(vpool.id(('const', b))) return vpool.id(('const', b))
cnf.append([var_const(True)]) cnf.append([var_const(True)])
cnf.append([-var_const(False)]) cnf.append([-var_const(False)])
# Voor elke relatie en elke twee elementen o1 en o2, is er een variabele die # Voor elke relatie en elke twee elementen o1 en o2, is er een variabele die
# aangeeft of o1 en o2 gerelateerd zijn. Er is 1 variabele voor xRy en yRx, dus # aangeeft of o1 en o2 gerelateerd zijn. Er is 1 variabele voor xRy en yRx, dus
# symmetrie is al ingebouwd. Reflexiviteit is ook ingebouwd. # symmetrie is al ingebouwd. Reflexiviteit is ook ingebouwd.
@ -91,7 +98,8 @@ def var_rel(rid, o1, o2):
return var_const(True) return var_const(True)
[so1, so2] = sorted([o1, o2]) [so1, so2] = sorted([o1, o2])
return(vpool.id(('rel', rid, so1, so2))) return vpool.id(('rel', rid, so1, so2))
# De relatie op outputs geeft een relaties op rijen. Deze zijn geindexeerd # De relatie op outputs geeft een relaties op rijen. Deze zijn geindexeerd
# met de woorden uit 'rows'. # met de woorden uit 'rows'.
@ -100,12 +108,14 @@ def var_row_rel(rid, r1, r2):
return var_const(True) return var_const(True)
[sr1, sr2] = sorted([r1, r2]) [sr1, sr2] = sorted([r1, r2])
return(vpool.id(('row_rel', rid, sr1, sr2))) return vpool.id(('row_rel', rid, sr1, sr2))
# Voor elke relatie, en elke equivalentie-klasse, kiezen we precies 1 rij # Voor elke relatie, en elke equivalentie-klasse, kiezen we precies 1 rij
# als representant. Deze variabele geeft aan welk element. # als representant. Deze variabele geeft aan welk element.
def var_row_rep(rid, r): def var_row_rep(rid, r):
return(vpool.id(('row_rep', rid, r))) return vpool.id(('row_rep', rid, r))
# Contraints zodat de relatie een equivalentie relatie is. We hoeven alleen # Contraints zodat de relatie een equivalentie relatie is. We hoeven alleen
# maar transitiviteit te encoderen, want refl en symm zijn ingebouwd in de var. # maar transitiviteit te encoderen, want refl en symm zijn ingebouwd in de var.
@ -130,7 +140,7 @@ for rid in rids:
# (Aka: the bijbehorende quotienten zijn joint-injective.) # (Aka: the bijbehorende quotienten zijn joint-injective.)
print('- injectivity (o)') print('- injectivity (o)')
for xi, xo in enumerate(os): for xi, xo in enumerate(os):
for yo in os[xi+1:]: for yo in os[xi + 1 :]:
# Tenminste een rid moet een verschil maken # Tenminste een rid moet een verschil maken
cnf.append([-var_rel(rid, xo, yo) for rid in rids]) cnf.append([-var_rel(rid, xo, yo) for rid in rids])
@ -147,7 +157,7 @@ for rid in rids:
cnf.append([-var_rel(rid, ox, oy) for (ox, oy) in oss] + [var_row_rel(rid, rx, ry)]) cnf.append([-var_rel(rid, ox, oy) for (ox, oy) in oss] + [var_row_rel(rid, rx, ry)])
# rx ~ ry => oxi ~ oyi # rx ~ ry => oxi ~ oyi
for (ox, oy) in oss: for ox, oy in oss:
cnf.append([-var_row_rel(rid, rx, ry), var_rel(rid, ox, oy)]) cnf.append([-var_row_rel(rid, rx, ry), var_rel(rid, ox, oy)])
# De constraints die zorgen dat representanten ook echt representanten zijn. # De constraints die zorgen dat representanten ook echt representanten zijn.
@ -157,7 +167,7 @@ for rid in rids:
# Belangrijkste: een element is een representant, of equivalent met een # Belangrijkste: een element is een representant, of equivalent met een
# eerder element. We forceren hiermee dat de solver representanten moet # eerder element. We forceren hiermee dat de solver representanten moet
# kiezen (voor aan de lijst). # kiezen (voor aan de lijst).
cnf.append([var_row_rep(rid, rx)] + [var_row_rel(rid, rx, ry) for ry in rows[:ix]] ) cnf.append([var_row_rep(rid, rx)] + [var_row_rel(rid, rx, ry) for ry in rows[:ix]])
for ry in rows[:ix]: for ry in rows[:ix]:
# rx en ry kunnen niet beide een representant zijn, tenzij ze # rx en ry kunnen niet beide een representant zijn, tenzij ze
# niet gerelateerd zijn. # niet gerelateerd zijn.
@ -169,6 +179,7 @@ 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_optim = CardEnc.atmost([var_row_rep(rid, rx) for rid in rids for rx in rows], total_size, vpool=vpool)
cnf.extend(cnf_optim) cnf.extend(cnf_optim)
def print_eqrel(rel, xs): def print_eqrel(rel, xs):
print_table(lambda r, c: 'Y' if rel(r, c) else '·', xs, xs) print_table(lambda r, c: 'Y' if rel(r, c) else '·', xs, xs)
@ -185,15 +196,14 @@ with Solver(bootstrap_with=cnf) as solver:
print('unsat :-(') print('unsat :-(')
exit() exit()
print(f'sat :-)') print('sat :-)')
# Even omzetten in een makkelijkere data structuur # Even omzetten in een makkelijkere data structuur
print('- get model') print('- get model')
m = solver.get_model() m = solver.get_model()
model = {} model = {}
for l in m: for l in m:
if l < 0: model[-l] = False model[abs(l)] = l > 0
else: model[l] = True
for rid in rids: for rid in rids:
print(f'Relation {rid}:') print(f'Relation {rid}:')

28
other/decompose_set.py
View file

@ -17,10 +17,10 @@ from pysat.formula import CNF
# langzaam vb.: n = 151, c = 4 en total_size = 15 # langzaam vb.: n = 151, c = 4 en total_size = 15
n = 151 n = 151
c = 4 c = 4
total_size = 15 # als deze te laag is => UNSAT => duurt lang total_size = 15 # als deze te laag is => UNSAT => duurt lang
os = [i for i in range(n)] # outputs os = [i for i in range(n)] # outputs
rids = [i for i in range(c)] # components rids = [i for i in range(c)] # components
# Optimale decompositie met slechts verzamelingen. Zie ook A007600 (omkering # Optimale decompositie met slechts verzamelingen. Zie ook A007600 (omkering
# A000792) in de OEIS, dit groeit met ongeveer O(log(n)). Ik weet niet hoeveel # A000792) in de OEIS, dit groeit met ongeveer O(log(n)). Ik weet niet hoeveel
@ -37,13 +37,16 @@ print('Start encoding')
vpool = IDPool() vpool = IDPool()
cnf = CNF() cnf = CNF()
# Een hulp variabele voor False en True, maakt de andere variabelen eenvoudiger # Een hulp variabele voor False en True, maakt de andere variabelen eenvoudiger
def var_const(b): def var_const(b):
return(vpool.id(('bool', b))) return vpool.id(('bool', b))
cnf.append([var_const(True)]) cnf.append([var_const(True)])
cnf.append([-var_const(False)]) cnf.append([-var_const(False)])
# Voor elke relatie en elke twee elementen o1 en o2, is er een variabele die # Voor elke relatie en elke twee elementen o1 en o2, is er een variabele die
# aangeeft of o1 en o2 gerelateerd zijn. Er is 1 variabele voor xRy en yRx, dus # aangeeft of o1 en o2 gerelateerd zijn. Er is 1 variabele voor xRy en yRx, dus
# symmetrie is al ingebouwd. Reflexiviteit is ook ingebouwd. # symmetrie is al ingebouwd. Reflexiviteit is ook ingebouwd.
@ -52,12 +55,14 @@ def var_rel(rid, o1, o2):
return var_const(True) return var_const(True)
[so1, so2] = sorted([o1, o2]) [so1, so2] = sorted([o1, o2])
return(vpool.id(('var_rel', rid, so1, so2))) return vpool.id(('var_rel', rid, so1, so2))
# Voor elke relatie, en elke equivalentie-klasse, kiezen we precies 1 element # Voor elke relatie, en elke equivalentie-klasse, kiezen we precies 1 element
# als representant. Deze variabele geeft aan welk element. # als representant. Deze variabele geeft aan welk element.
def var_rep(rid, o): def var_rep(rid, o):
return(vpool.id(('var_rep', rid, o))) return vpool.id(('var_rep', rid, o))
# Contraints zodat de relatie een equivalentie relatie is. We hoeven alleen # Contraints zodat de relatie een equivalentie relatie is. We hoeven alleen
# maar transitiviteit te encoderen, want refl en symm zijn ingebouwd in de var. # maar transitiviteit te encoderen, want refl en symm zijn ingebouwd in de var.
@ -74,7 +79,7 @@ for rid in rids:
# (Aka: the bijbehorende quotienten zijn joint-injective.) # (Aka: the bijbehorende quotienten zijn joint-injective.)
print('- injectivity') print('- injectivity')
for xi, xo in enumerate(os): for xi, xo in enumerate(os):
for yo in os[xi+1:]: for yo in os[xi + 1 :]:
# Tenminste een rid moet een verschil maken # Tenminste een rid moet een verschil maken
cnf.append([-var_rel(rid, xo, yo) for rid in rids]) cnf.append([-var_rel(rid, xo, yo) for rid in rids])
@ -85,8 +90,8 @@ for rid in rids:
# Belangrijkste: een element is een representant, of equivalent met een # Belangrijkste: een element is een representant, of equivalent met een
# later element. We forceren hiermee dat de solver representanten moet # later element. We forceren hiermee dat de solver representanten moet
# kiezen (achter aan de lijst). # kiezen (achter aan de lijst).
cnf.append([var_rep(rid, xo)] + [var_rel(rid, xo, yo) for yo in os[xi+1:]] ) cnf.append([var_rep(rid, xo)] + [var_rel(rid, xo, yo) for yo in os[xi + 1 :]])
for _, yo in enumerate(os[xi+1:], xi+1): for _, yo in enumerate(os[xi + 1 :], xi + 1):
# xo en yo kunnen niet beide een representant zijn, tenzij ze # xo en yo kunnen niet beide een representant zijn, tenzij ze
# niet gerelateerd zijn. # niet gerelateerd zijn.
cnf.append([-var_rep(rid, xo), -var_rep(rid, yo), -var_rel(rid, xo, yo)]) cnf.append([-var_rep(rid, xo), -var_rep(rid, yo), -var_rel(rid, xo, yo)])
@ -109,15 +114,14 @@ with Solver(bootstrap_with=cnf) as solver:
print('unsat :-(') print('unsat :-(')
exit() exit()
print(f'sat :-)') print('sat :-)')
# Even omzetten in een makkelijkere data structuur # Even omzetten in een makkelijkere data structuur
print('- get model') print('- get model')
m = solver.get_model() m = solver.get_model()
model = {} model = {}
for l in m: for l in m:
if l < 0: model[-l] = False model[abs(l)] = l > 0
else: model[l] = True
# print equivalence classes # print equivalence classes
count = 0 count = 0

13
other/fsm-examples.py
View file

@ -1,5 +1,6 @@
import argparse import argparse
class RKMachine: class RKMachine:
# Rick Koenders came up with this example in the case of N=3. # Rick Koenders came up with this example in the case of N=3.
# FSM will have 2*N states, but can be decomposed into N + 2 states. # FSM will have 2*N states, but can be decomposed into N + 2 states.
@ -10,12 +11,12 @@ class RKMachine:
self.outputs = [n for n in range(N)] self.outputs = [n for n in range(N)]
self.states = [(n, b) for b in [False, True] for n in range(N)] self.states = [(n, b) for b in [False, True] for n in range(N)]
self.transition_map = {((n, 0), 'a') : ((n+1) % N, 0) for n in range(N)} self.transition_map = {((n, 0), 'a'): ((n + 1) % N, 0) for n in range(N)}
self.transition_map |= {(((n+1) % N, 1), 'a') : (n % N, 1) for n in range(N)} self.transition_map |= {(((n + 1) % N, 1), 'a'): (n % N, 1) for n in range(N)}
self.transition_map |= {((n, b), 'b') : (n, not b) for b in [False, True] for n in range(N)} self.transition_map |= {((n, b), 'b'): (n, not b) for b in [False, True] for n in range(N)}
self.output_map = {((n, b), 'a') : n for b in [False, True] for n in range(N)} self.output_map = {((n, b), 'a'): n for b in [False, True] for n in range(N)}
self.output_map |= {((n, b), 'b') : 0 for b in [False, True] for n in range(N)} self.output_map |= {((n, b), 'b'): 0 for b in [False, True] for n in range(N)}
def state_to_string(self, s): def state_to_string(self, s):
(n, b) = s (n, b) = s
@ -27,6 +28,7 @@ class RKMachine:
def output(self, s, a): def output(self, s, a):
return self.output_map[(s, a)] return self.output_map[(s, a)]
def fsm_to_dot(name, m): def fsm_to_dot(name, m):
def transition_string(s, i, o, t): def transition_string(s, i, o, t):
return f'{s} -> {t} [label="{i}/{o}"]' return f'{s} -> {t} [label="{i}/{o}"]'
@ -44,6 +46,7 @@ def fsm_to_dot(name, m):
return ret return ret
parser = argparse.ArgumentParser() parser = argparse.ArgumentParser()
parser.add_argument('machine', nargs='?', default='rk', choices=['rk']) parser.add_argument('machine', nargs='?', default='rk', choices=['rk'])
parser.add_argument('-n', type=int, default=3, help='size parameter') parser.add_argument('-n', type=int, default=3, help='size parameter')

20
other/partitions.py
View file

@ -4,21 +4,24 @@ from math import prod
N = 99999 N = 99999
C = 16 C = 16
# precondition k <= n # precondition k <= n
def all_partitions_(n, k): def all_partitions_(n, k):
if n == 0: if n == 0:
return [[]] return [[]]
acc = [] acc = []
for j in range(1, k+1): for j in range(1, k + 1):
ps = all_partitions_(n-j, min(n-j, j)) ps = all_partitions_(n - j, min(n - j, j))
acc.extend([[j]+p for p in ps]) acc.extend([[j] + p for p in ps])
return acc return acc
def all_partitions(n): def all_partitions(n):
return all_partitions_(n, n) return all_partitions_(n, n)
def highest_product(n): def highest_product(n):
ps = all_partitions(n) ps = all_partitions(n)
@ -37,20 +40,22 @@ def highest_product(n):
return highest_prod return highest_prod
def tabulate(upper): def tabulate(upper):
highest_n_per_c = {} highest_n_per_c = {}
table = {} table = {}
for s in range(1, upper+1): for s in range(1, upper + 1):
res = highest_product(s) res = highest_product(s)
for c, n in res.items(): for c, n in res.items():
for n2 in range(highest_n_per_c.get(c, 0)+1, min(n, N)+1): for n2 in range(highest_n_per_c.get(c, 0) + 1, min(n, N) + 1):
table[(n2, c)] = s table[(n2, c)] = s
highest_n_per_c[c] = n highest_n_per_c[c] = n
return {(n, c): s for (n, c), s in table.items() if s <= n} return {(n, c): s for (n, c), s in table.items() if s <= n}
def trim_tab(tab): def trim_tab(tab):
best_s = {} best_s = {}
best_c = {} best_c = {}
@ -65,6 +70,7 @@ def trim_tab(tab):
return {(n, c): s for (n, c), s in tab.items() if c <= best_c[n] or s <= best_s[n]} 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): def print_table(tab0):
tab = trim_tab(tab0) tab = trim_tab(tab0)
@ -79,10 +85,10 @@ def print_table(tab0):
prev_row = '' prev_row = ''
for n in range(1, N+1): for n in range(1, N + 1):
best = None best = None
row = '' row = ''
for c in range(1, C+1): for c in range(1, C + 1):
if (n, c) in tab: if (n, c) in tab:
row += ' ' + str(tab[(n, c)]).rjust(col_width[c]) row += ' ' + str(tab[(n, c)]).rjust(col_width[c])
if not best or tab[(n, c)] < best[0]: if not best or tab[(n, c)] < best[0]: