Laurent Bartholdi <laurent.bartholdi(a)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.
