Laurent Bartholdi laurent.bartholdi@gmail.com writes:
Ah, OK, thanks. Is there a good reason to do the log-encoding, or is it actually fine to have a classical alphabet a,b,c, ... and encode each letter as (a & !b & !c, !a & b & !c, !a & !b & c, ...)?
It all depends on what operations you plan to do on those automata. Some operations are exponential in the number of atomic propositions, so it is often best to have fewer of those.
If you only plan to two intersections and emptiness checks, a one-hot encoding (what you suggested) is probably fine.
If you need to work with complete automata at some point (e.g., maybe for complementation), one-hot encoding will be hard to work with. You want the disjunction of the encodings of all letters in your alphabet to be equal to true, so that completing an automaton does not "invent" encodings that correspond to no letters.