SAT-based minimization of deterministic ω-automata¶

The spot.sat_minimize() Python function is the main entry point for minimizing any deterministic ω-automaton. This notebook demonstrates how to use that function.

Warning: while the automata used in this notebook are quite small, working with large automata can require a lot of RAM and take huge amount of time. In its most straightforward variant, sat_minimize() takes a input automaton (called reference) and then makes a loop to ask a SAT-solver for an equivalent automaton (called candidate) with 1 fewer state at each iteration. If the reference has size ($n_i$, $s_i$), i.e. $n_i$ states, $s_i$ acceptance sets, and the candidate has size $(n_o, s_o)$, the SAT encoding uses $\mathrm{O}(n_i^2\times n_o^2\times 2^{s_i+s_o})$ variables and $\mathrm{O}(n_i^2 \times n_o^3\times 2^{s_i+2s_o}\times |\Sigma|)$ clauses. Reducing the number of acceptance set the therefore the most important way to simplify a problem.

Minimizing DBA¶

Let's take a simple formula and translate it into a DBA:

The above automaton is not minimal and is easily reduced by sat_minimize():

Note that by default SAT-minimize produces a transition-based automaton with the same acceptance condition. State-based acceptance can be requested with the state_based option:

Minimizing deterministic ω-automata with arbitrary acceptance condition¶

Now let's look at examples with more complicated acceptance conditions.
The following Rabin automaton was produced using ltl2dstar 0.5.4 and spot 2.5.2 with

ltlfilt --lbt -f '(FGa | Fb) & FGc'  | ltl2dstar -H --ltl2nba=spin:ltl2tgba@-Ds - -

however we hardcode it so that the notebook can be used even with ltl2dstar installed.

It can be minimized as a 2-state transition-based Rabin automaton:

Or as a 4-state state-based Rabin automaton:

But do we really need 2 rabin pairs? Let's ask if we can get an equivalent with only one pair. (Note that reducing the number of pairs might require more state, but the sat_minimize() function will never attempt to add state unless explicitely instructed to do so. In this case we are therefore looking for a state-based Rabin-1 automaton with at most 4 states.)

Using the display_log option, we can have a hint of what is going on under the hood. Each line in the table shows one call to the SAT solver. The column labeled target.states gives the size of the equivalent automaton we ask the SAT-solver to produce, but some of these states may actually be unreachable in the result. The variables and clauses columns give an indication of the size of the SAT problem. The enc.* and sat.* columns give the user and system time taken to encode and solve the SAT problem (the unit is "ticks", which usually is 1/100 of seconds).

Below we see that the minimization procedure first tried to squeeze the 6-state input into a 3-state automaton, which failed, and then into a 5-state automaton, which was successful. This 5-state automaton was used as input to produce a smaller 4-state automaton.. Essentially this procedure is doing a binary search towards the minimal size.

(In this case it does not matter, but be aware that the number of states displayed in the log table are those of complete automata, while the output of sat_minimize() is trimmed by default.)

Note that we already had a smaller transition-based automaton for this language (in the small variable), and that it actually is more efficient to work from that, as seen in problem sizes displayed in the following log.

How did the procedure look for a complete automaton of size 5 when the input had only 2 states? It's because the input uses transition-based acceptance: to estimate an upper bound of the size of the state-based output, the sat_minimize() procedure converted its transition-based input to state-based acceptance (using the spot.sbacc() function) and counted the number of states in the result.

Such an estimate is not necessarily correct if we request a different acceptance condition. In that case we can actually change the upper-bound using max_states. Below we additionally demonstrate the use of the colored option, to request all transitions to belong to exactly one set, as customary in parity automata.

There are a couple of ways in which we can influence the search for the minimum automaton. We can disable the binary search with sat_naive. In this case, the procedure will try to remove one state at a time. This is not necessary slower than the default binary search, because satisfiable problems are often solved more quickly than unsatisfiable ones.

Variant for incremental SAT solving¶

Using sat_incr=1, we encode the problem of finding an equivalent automaton with $n$ states, and add 6 additional variables and some additional constraints to the problem:

Now using assume directives on variable $v_i$ amounts to testing whether the problem is solved with $n-i$ states, but we do not have to reencode the problem for each test, and the solver can (probably) reuse some of the knowledge it gathered during a previous attempt. We do a binary search on these 6 assumptions, to find some $i$ such that the problem is satisfiable with assumption $v_i$ but not with $v_{i+1}$. If such cast exists, we have found the minimal automaton. If assumption $v_6$ is satisfiable, we re-encode the problem with $n-7$ states and start over. Watch how the number of variables and clauses do not change in the following log.

The number of assumption variables to use in a one encoding can be set with the sat_incr_steps argument. Its default value of 6 was chosen empirically by benchmarking different values.

Another incremental variant consists is the equivalent of forcing $v_1$, $v_2$, ... in order. But to do that we do not need to use any assumption. We just add the constraints that transitions going to state $n-i$ are forbidden. This variant is enabled by option sat_incr=2. As in the previous case, we do a few of those incremental steps (2 by default, but that can be changed with the sat_incr_steps parameter) and then we reencode the problem to reduce its size.

In the log below, line 0 corresponds to the search of an equivalent automaton with the same size, but the simpler co-Büchi acceptance. It works, and most of the time was spent encoding the problem. Then for the next two lines, the minimization function looks for automata of size 5 and 4 without reencoding the problem but simply adding a few constraints to disable the relevant transitions.

Miscellaneous options¶

return_log¶

The return_log can be used to obtain the log table as an object. In that case, sat_minimize() returns a pair, (aut,log) where aut can be None if the minimization failed. Also, the log table contains an extra column that is hidden by display_log: it contains the corresponding automaton in HOA format.

Here is how we can extract the automata from that log:

sat_langmap¶

When using the default binary search approach, the sat_langmap=True can help refine the lower bound by first testing the language-equivalence of all states in the automaton. This allows to form equivalence classes of states, and clearly the minimal automaton needs at least as many states as the number of equivalence states.

For instance in the large automaton we use as example, the 6 states correspond to only two different languages. This can be seen with the highlight_language() function, which colors states with identical languages. This information can be used by the minimization function to search a minimal automaton between 2 and 6 states.

Compare the next two logs, with and without sat_langmap.

states¶

Sometimes we do not want a minimization loop, we just want to generate an equivalent automaton with a given number of states. In that case, we use the states option. However there is no constraint that all states should be reachable, so in the end, you could end with an automaton with fewer states than requested.