joshua/satuio
1
Fork 0
mirror of https://github.com/Jaxan/satuio.git synced 2025-04-27 06:37:45 +02:00
Code Issues Releases Activity
Using SAT solvers to construct UIOs and ADSs
14 commits 1 branch 0 tags 215 KiB
Find a file
Joshua Moerman 9dbe5dee5b small change for ads
2022-01-24 15:21:45 +01:00
examples First(ish) version of the UIO solver 2022-01-17 08:56:37 +01:00
satuio small change for ads 2022-01-24 15:21:45 +01:00
.gitignore Initial commit 2022-01-17 08:48:55 +01:00
README.md More efficient UIO solver, by uio-implication and incrementing the length 2022-01-24 14:12:07 +01:00

README.md

satuio

Using SAT solvers to construct UIOs and ADSs for Mealy machines.

Dependencies

This project uses Python3. It uses the following packages which can be installed with pip.

Usage

All scripts show their usage with the --help flag. Note that the flags and options are subject to change, since this is WIP.

# Finding UIO sequences of fixed length in a Mealy machine
python3 satuio/uio.py --help

# Finding UIO sequences while incrementing the length in a Mealy machine
python3 satuio/uio-incr.py --help

# Finding an ADS in a Mealy machine for a set of states
python3 satuio/ads.py --help

The solver can be specified (as long as pysat supports it). The default is Glucose3, as that worked well on the examples.

Copyright

© Joshua Moerman, Open Universiteit, 2022