From 7ddb1bb45cb8902b3d652ece67583988b687d9fd Mon Sep 17 00:00:00 2001
From: Joshua Moerman <lakseru@gmail.com>
Date: Wed, 26 Jan 2022 09:52:25 +0100
Subject: [PATCH] Some more cleaning up and comments

---
 README.md     | 19 ++++++++++++++++---
 satuio/ads.py | 22 +++++++++++++++++++---
 2 files changed, 35 insertions(+), 6 deletions(-)

diff --git a/README.md b/README.md
index 1abf0bb..48c43f0 100644
--- a/README.md
+++ b/README.md
@@ -1,13 +1,24 @@
 satuio
 ======
 
-Using SAT solvers to construct UIOs and ADSs for Mealy machines.
+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.
 
 
 ## Dependencies
 
 This project uses Python3. It uses the following packages which can be
-installed with `pip`.
+installed with `pip` as follows:
+
+```bash
+pip3 install pysat tqdm rich
+```
 
 * [`pysat`](https://github.com/pysathq/pysat)
 * [`tqdm`](https://github.com/tqdm/tqdm)
@@ -17,7 +28,9 @@ 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.
+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.)
 
 ```bash
 # Finding UIO sequences of fixed length in a Mealy machine
diff --git a/satuio/ads.py b/satuio/ads.py
index e4e6a9a..cd3cbb8 100644
--- a/satuio/ads.py
+++ b/satuio/ads.py
@@ -7,6 +7,11 @@ usage, please run
 
   python3 ads.py --help
 
+Note: it is not advised to construct an ADS for the whole machine
+in this way. The encoding takes a very long time, and the solver
+will have a hard time. Use the algorithm by Lee and Yannakakis
+instead (the ADS-problem for the whole state space is in P).
+
 © Joshua Moerman, Open Universiteit, 2022
 """
 
@@ -47,7 +52,7 @@ parser.add_argument('--states', help='For which states to compute an ADS', nargs
 args = parser.parse_args()
 
 if args.states == None or len(args.states) <= 1:
-  raise ValueError('Should specify at leasta 2 states')
+  raise ValueError('Should specify at least 2 states')
 
 # reading the automaton
 (alphabet, outputs, all_states, delta, labda) = read_machine(args.filename)
@@ -172,7 +177,9 @@ for s in tqdm(states, desc="CNF diffs"):
   for t in states:
     # We skip s == t, since those state are equivalent.
     # I am not sure whether we can skip s <= t, since our construction
-    # below is not symmetrical.
+    # below is not symmetrical. We do however include a clause which
+    # states that the dvars are symmetrical. This should help the
+    # solver a little bit.
     if s == t:
       continue
 
@@ -319,7 +326,16 @@ measure_time("Done with total time")
 
 # TODO: we know that dvar(s, t, i) is an equivalence relation for
 # each i. Do we help the solver when asserting that? Or will that
-# make the solving slower?
+# make the solving slower? One problem: transitivity requires n^3
+# many clauses... (Symmetry is already implemented.)
+
+# TODO: try to see whether the other implication of d2var -> d2var
+# makes the solving more efficient. The clauses are redundant, but
+# it might help. It also makes sure that enumerating several models
+# are actually different ADSs.
+
+# TODO: the same for difference -> dvar. We only do one implication,
+# and perhaps adding the other makes it faster.
 
 # TODO: prune the tree in the end. (Some states will have shorter
 # words than others.)