If the target acceptance is Fin(0)&Inf(1), there is no need to
distinguish between an history of {0,1} and an history of {0}, as a
cycle with either history will be rejected.  This implements this
simplification.  If both the canditate and reference automata
are Rabin automata with n pairs, then we now use at most
  Q * Q' * Q * Q' * 3^n * 3^n
variables to encode the partial cycles histories, versus
  Q * Q' * Q * Q' * 4^n * 4^n
before.

* src/twaalgos/dtgbasat.cc: Implement this.
* src/tests/satmin2.test: More tests.