investigate use of SAT-based synthezis of deterministic automata using non-deterministic input
I believe the code should work as-is, provided we should lift the "deterministic input" restriction, and document that the number of states needed to synthesize a deterministic automaton from a nondeterministic maybe need to be greater.
This came up in an email conversation with Jan Strejček, who assumed the SAT stuff was accepting non-deterministic input.