From a067d158f47ed419fea9a15c60a0aaa119af364a Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Wed, 5 Jun 2024 10:46:27 +0200 Subject: [PATCH] New feature in SAT solving script: weak decomposition --- other/decompose_fsm_optimise.py | 93 ++++++++++++++----- .../optimal_decomposition_of_sets.txt | 0 2 files changed, 69 insertions(+), 24 deletions(-) rename other/{ => results}/optimal_decomposition_of_sets.txt (100%) diff --git a/other/decompose_fsm_optimise.py b/other/decompose_fsm_optimise.py index 6d12c94..8829552 100644 --- a/other/decompose_fsm_optimise.py +++ b/other/decompose_fsm_optimise.py @@ -3,6 +3,7 @@ from pysat.card import ITotalizer from pysat.formula import IDPool from pysat.formula import CNF +import signal import math import argparse @@ -10,17 +11,22 @@ import argparse # Stap 1: pip3 install python-sat # Stap 2: python3 decompose_fsm.py -h +timeout = False +timeout_seconds = 3*60 +record_sizes = False +record_file = './results/log.txt' + 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('-w', '--weak', default=False, action="store_true", help='look for weak decomposition') 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('filename', help='path to .dot file') args = parser.parse_args() -# als de de total_size te laag is => UNSAT => duurt lang +# Aantal componenten. c = 1 is zinloos, maar zou moeten werken c = args.components - -assert c >= 1 # c = 1 is zinloos, maar zou moeten werken +assert c >= 1 ################################### @@ -86,8 +92,18 @@ with open(args.filename) as file: print(machine) N = len(machine.states) -print(f'Initial size: {N}') +print(f'Input FSM: {N} states, {len(machine.inputs)} inputs, and {len(machine.outputs)} outputs') +if timeout: + def timeout_handler(signum, frame): + with open(record_file, 'a') as file: + last_two_comps = '/'.join(args.filename.split('/')[-2:]) + file.write(f'{last_two_comps}\t{N}\t{len(machine.inputs)}\t{len(machine.outputs)}\t{args.weak}\t{c}\tTIMEOUT\n') + print('TIMEOUT') + exit() + + signal.signal(signal.SIGALRM, timeout_handler) + signal.alarm(timeout_seconds) ################################### # Utility functions @@ -240,12 +256,26 @@ for rid in rids: progress.add() # Tot slot willen we weinig representanten. Dit doen we met een "atmost" -# formule. Idealiter zoeken we naar de total_size, maar die staat nu vast. -lower_bound = int(math.floor(c * (N-1)**(1/c))) -upper_bound = int(N + c - 1) -print(f'size constraints {lower_bound} {upper_bound}') -cnf_optim = ITotalizer([var_state_rep(rid, sx) for rid in rids for sx in machine.states], ubound=upper_bound, top_id=vpool.top) -cnf.extend(cnf_optim.cnf.clauses) +# formule. We gaan een binaire zoek doen met incremental sat solving. +rhs = None +if args.weak: + lower_bound = int(math.floor((N-1)**(1/c))) + upper_bound = int(N) + print(f'weak size constraints {lower_bound} {upper_bound}') + rhs = [] + for rid in rids: + with ITotalizer([var_state_rep(rid, sx) for sx in machine.states], ubound=upper_bound, top_id=vpool.top) as cnf_optim: + vpool.occupy(vpool.top + 1, cnf_optim.top_id) + vpool.top = cnf_optim.top_id + cnf.extend(cnf_optim.cnf.clauses) + rhs.append(cnf_optim.rhs) +else: + lower_bound = int(math.floor(c * (N-1)**(1/c))) + upper_bound = int(N + c - 1) + print(f'size constraints {lower_bound} {upper_bound}') + with ITotalizer([var_state_rep(rid, sx) for rid in rids for sx in machine.states], ubound=upper_bound, top_id=vpool.top) as cnf_optim: + cnf.extend(cnf_optim.cnf.clauses) + rhs = cnf_optim.rhs ################################## # Probleem oplossen met solver :-) @@ -253,24 +283,35 @@ print('Start solving') print('- copying formula') with Solver(bootstrap_with=cnf) as solver: print('===============') + sat = None while upper_bound - lower_bound >= 2: mid_size = int((lower_bound + upper_bound) / 2) - print(f'Trying {lower_bound} < {mid_size} < {upper_bound}') - sat = solver.solve(assumptions=[-cnf_optim.rhs[mid_size]]) + print(f'Trying {lower_bound} < {mid_size} < {upper_bound}', end='', flush=True) + if args.weak: + assumptions = [-rhs[rid][mid_size] for rid in rids] + sat = solver.solve(assumptions=assumptions) + else: + sat = solver.solve(assumptions=[-rhs[mid_size]]) if sat: + print('\tdown') upper_bound = mid_size continue else: + print('\tup') lower_bound = mid_size continue - total_size = upper_bound - print(f'done searching, found size = {total_size}') - sat = solver.solve(assumptions=[-cnf_optim.rhs[total_size]]) + bound = upper_bound + print(f'done searching, found bound = {bound}') + + if args.weak: + assumptions = [-rhs[rid][bound] for rid in rids] + sat = solver.solve(assumptions=assumptions) + else: + sat = solver.solve(assumptions=[-rhs[bound]]) assert sat # Even omzetten in een makkelijkere data structuur - print('- get model') m = solver.get_model() model = {} for l in m: @@ -286,20 +327,23 @@ with Solver(bootstrap_with=cnf) as solver: print(f'State relation {rid}:') print_eqrel(lambda x, y: model[var_state_rel(rid, x, y)], machine.states) - # print equivalence classes - count = 0 + # Precieze groottes van elk component tellen + counts = [] for rid in rids: - if args.verbose: - print(f'component {rid}') + count = 0 # Eerst verzamelen we de representanten for s in machine.states: if model[var_state_rep(rid, s)]: count += 1 if args.verbose: - print(f'- representative state {s}') + print(f'comp {rid} -> representative state {s}') + counts.append(count) - # count moet gelijk zijn aan cost (of kleiner) - print(f'Reduced size = {count}') + print(f'Reduced sizes = {counts} = {sum(counts)}') + if record_sizes: + with open(record_file, 'a') as file: + last_two_comps = '/'.join(args.filename.split('/')[-2:]) + file.write(f'{last_two_comps}\t{N}\t{len(machine.inputs)}\t{len(machine.outputs)}\t{args.weak}\t{c}\t{sum(counts)}\t{sorted(counts, reverse=True)}\n') projections = {} for rid in rids: @@ -321,7 +365,8 @@ with Solver(bootstrap_with=cnf) as solver: projections[rid][o] = f'cls_{rid}_{count}' if not others: - projections[rid][repr] = f'{repr}' + # Aangeven dat het een unieke output is + projections[rid][repr] = f'cls_{rid}_{count}_u' count += 1 diff --git a/other/optimal_decomposition_of_sets.txt b/other/results/optimal_decomposition_of_sets.txt similarity index 100% rename from other/optimal_decomposition_of_sets.txt rename to other/results/optimal_decomposition_of_sets.txt