`strategy` metacommand - Walnut-Theorem-Prover/Walnut GitHub Wiki

Several Walnut papers describe determinizations of intermediate automata that sometimes take multiple days and use over a terabyte of memory, often minimizing into a small DFA.

Sometimes, due to the structure of a particular NFA, a different determinization strategy can be vastly more efficient. For example, the OTF algorithms have been known to solve some Walnut calculations 100x faster and with 100x less resources than with the standard Subset Construction (OTF performance examples). If you encounter a determinization that is slow or consuming too many resources, consider switching strategies.

Strategy metacommand

From Walnut help:

[Walnut]$ help [strategy];
=== Help: [strategy] ===
The "strategy" metacommand allows different strategies for determinization of intermediate automata, rather than the default SC (Subset Construction).

Implemented strategies are Brzozowski's_algorithm and several new OTF algorithms.

Example

[Walnut]$ def cmp "?lsd_3 Ak (k<n) => TP[t][i+k]=TP[u][j+k]"::

We see that the following intermediate automaton takes a lot of resources, although it will eventually finish. In Walnut 5, this took 76 gigabytes of RAM and 2000s. In Walnut 7, this takes more than 15 gigabytes of RAM and over 440s (here you see Walnut crashing on my laptop).

      Determinizing [#3, strategy: SC]: 100 states        
        Progress: Added 100 states - 23694 states left in queue - 23794 reachable states - 211ms
        Progress: Added 1000 states - 71284 states left in queue - 72284 reachable states - 4205ms
        Progress: Added 10000 states - 104511 states left in queue - 114511 reachable states - 36531ms
...
        Progress: Added 140000 states - 2289 states left in queue - 142289 reachable states - 431361ms
        Determinized: 142311 states - 439631ms
        Minimizing: 142311 states.
./walnut.sh: line 6: 215483 Killed                  java -Xmx15000M -jar build/libs/Walnut-all.jar "$@"

However, with OTF's CCLS, this is trivial:

[Walnut]$ [strategy 3 CCLS]def cmp "?lsd_3 Ak (k<n) => TP[t][i+k]=TP[u][j+k]"::

     Determinizing [#3, strategy: CCLS]: 100 states
      Calculating simulation relations; this can be resource-intensive
      Simulation altered to 101 states
      Found 1839 simulation relations
        Progress: Explored 0 states - 1 states left in queue - 1 states added - 658ms
        Progress: Explored 100 states - 415 states left in queue - 515 states added - 739ms
        Progress: Explored 1000 states - 167 states left in queue - 1167 states added - 1013ms
      Determinized: 1399 states - 1166ms
      Minimizing: 1399 states.
      Minimized:432 states - 383ms.

OTF's BRZ-CCLS is slightly slower in this case but also works:

[Walnut]$ [strategy 3 BRZ-CCLS]def cmp "?lsd_3 Ak (k<n) => TP[t][i+k]=TP[u][j+k]"::

Determinizing [#3, strategy: Brzozowski-CCLS]: 100 states
      Reverse -- Determinizing with strategy:CCLS.
      Calculating simulation relations; this can be resource-intensive
...
      Determinized: 432 states - 14728ms
      Minimizing: 432 states.
      Minimized:432 states - 187ms.

Which determinization strategy should you use?

This is an unsolved problem (related to determinization being NP-complete). Still, a rule of thumb is try CCLS, then BRZ-CCLS. If the simulation step takes too long (sometimes with large NFAs), CCL, BRZ-CCL, and BRZ may be better options.

If the NFA size is very large (over say 300,000 states), then the OTF strategies are likely not practical, and we recommend trying BRZ.

`strategy` metacommand - Walnut-Theorem-Prover/Walnut GitHub Wiki