diff --git a/other/decomp-sat.py b/other/decomp-sat.py index 4219496..7688939 100644 --- a/other/decomp-sat.py +++ b/other/decomp-sat.py @@ -2,6 +2,10 @@ from pysat.examples.fm import FM from pysat.formula import IDPool from pysat.formula import WCNF +### Gebruik: +# Stap 1: pip 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. @@ -128,12 +132,3 @@ with FM(wcnf) as fm: # count moet gelijk zijn aan cost print(f'total size = {count}') - - -# with RC2(cnf) as rc2: -# for m in rc2.enumerate(): -# print('model {0} has cost {1}'.format(m, rc2.cost)) - -# with FM(cnf) as fm: -# m = fm.compute() -# print('model {0} has cost {1}'.format(fm.model, fm.cost))