Using SAT solvers to construct UIOs and ADSs for Mealy machines (aka finite state machines). Both problems are PSpace-complete, and so a SAT solver does not really make sense. However, with a given bound (encoded unary), the problems are in NP, and so can be encoded in SAT.

There are some Mealy machines in examples directory. And even for the machine with roughly 500 states, the encodings are efficient, and sequences can be found within minutes.

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

pip3 install python-sat tqdm rich

• pysat
• tqdm
• rich

All scripts show their usage with the --help flag. Note that the flags and options are subject to change, since this is WIP. I recommend to read the source code of these scripts to see what is going on. (Or read the upcoming paper.)

# 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

# Returning an unsat core in the case an ADS does not exist
python3 satuio/ads-core.py --help

The solver can be specified (as long as pysat supports it). The default is Glucose3, as that worked well on the examples. After a bit more testing, these work well: g3, mc, m22. These are okay: gc3, gc4, g4, mgh. And these were slow for me: cd, lgl, mcb, mcm, mpl, mg3.

The encoding currectly defaults to seqcounter for cardinality constraints. This seems to work just fine, and I am not even sure the encodings are really different for cardinality of k=1. It could be worth doing more testing to see which is the fastest.

© Joshua Moerman, Open Universiteit, 2022