schedgen

schedgen is a toolbox to easily generate and work with schedules for SMT solvers and similar automated reasoning tools. It addresses the core part of the problem: to generate from a set of strategies a schedule which slices the available time into short runs with a specific strategy. The user has to come up with good strategies.

The generator utilizes integer programming to find an optimal combination of slice length + strategy. The generated problems are not too difficult and can be solved on a laptop with open source integer programming tools.

The schedgen toolbox was originally developed to be used with the SMT solver veriT, but is solver independent.

Overview

The schedgen toolbox is a standard Python package. It has been tested with Python 3.10. To install the package it is enough to execute

$ python setup.py install

On NixOS one can use the shell.nix file to bring the dependencies into context. On other systems Python3, Pandas, and PuLP is needed.

This will install the following tools that are part of the schedgen toolbox on the user systems.

• schedgen-optimize.py is the main tool that performs the schedule generation. It takes the name of a folder that contains the experiments, a list of time slices, and the total timeout. After the generation is finished the result is written as a schedule into a CSV file. It is also possible to provide an existing scheduler to build a joint schedule. The benchmarks used to generate the schedule can be filtered as described above.
• schedgen-finalize.py takes CSV files describing schedules, as generated by schedgen-optimize.py, and produces a shell script that runs a solver according to the schedules. The user can provide a template for the script and change various parameters used during generation. The default script can pick schedules by {\smtlib} logic.
• schedgen-simulate.py can be used to predict the outcome of running a scheduler. To do so the user has to provide experiments for the strategies included in the schedule, but can use different benchmarks. Furthermore, it is possible to add noise to the simulation.
• schedgen-query.py is a small tool that produces lists of benchmarks for debugging and analysis purposes. For example, it can list the union of the benchmarks solved by some strategies, or find the benchmarks from this list that a specific schedule cannot solve.
• schedgen-visualize.py can be used to visualize one or multiple schedules. It generates a bar plot that represents a schedule visually.

Each of those tools can generate an extensive documentation of the options it exposes via the standard --help option.

Some background information about the toolbox was published at the PAAR workshop.

A schedgen Tutorial

This section shows how the schedgen toolbox can be used. We will build and explore an optimal schedule for some hand-crafted, artificialexample benchmark data. This data can be found in the file contrib/example_data.csv. The first strategy base-strategy}solves 20 benchmarks within one second. The five other strategies extra01 to extra05 solve up to five benchmarks exclusively such that extra01 solves five benchmarks not solved by any other strategy, extra02 solves four, and so on. There is one benchmark unsolved.smt2 that is not solved by any strategy and a strategy bad-strategy that solves only one benchmark in 1.5 seconds. Hence, if the total timeout is six seconds we expect the optimal schedule to run the strategies in the order just presented for one second each. The solving times have been sampled from a normal distribution to ensure the resulting graphs look interesting.

Since the example data is in the CSV format described above the first four lines of base-strategy are:

benchmark;logic;strategy;solved;time
base01.smt2;UF;base-strategy;yes;0.5189
base02.smt2;UF;base-strategy;yes;0.2164
base03.smt2;UF;base-strategy;yes;0.1754
...

The first step is to generate a schedule. To do so we invokethe schedgen-optimize.py command:

$ schedgen-optimize.py -l UF -s 0.9 1.0 1.1 -t 6 \
    -c -d contrib/example_data.csv \
    contrib/example_schedule.csv

The option -l UF selects the UF logic, the option -s 0.9 1.0 1.1 defines the time slices, and -t 6 sets the total timeout. Hence, every picked strategy can run for either 0.9, 1, or 1.1 second. Overall, the schedule is not allowed to use more than 6s. Finally, -c tells the tool to use the CSV parser, and the option -d gives the data location.

The tool then searches the optimal schedule and writes the result to contrib/example_schedule.csv.

The first four lines of the schedule are:

time;strategy
1.100;base-strategy
1.000;extra01
0.900;extra02
...

The first column indicates how long the strategy in the second column should be used. As enforced by the synthetic data, the generated schedule uses the strategies in the order outlined above.

Furthermore, the output by the tool predicts how well the schedule will perform. It prints the number of benchmarks solved in the given timeout and the sum of the time needed to solve those benchmarks.

['UF']: This schedule solves 35/37 benchmarks.
        Time needed: 52.19s.

Two benchmarks are not solved by this strategy: the benchmark only solved by the bad strategy and the benchmark not solved by any strategy. Furthermore, we learn that solving all benchmarks solved by this schedule will take 52.19 seconds. The output also tells us the solving time before order optimization, but in this case nothing changes.

The simulator can give us a better prediction of the schedule performance, but let us first visualize the schedule:

$ schedgen-visualize.py -t 6 -p out.pgf \
    contrib/example_schedule.csv

\in{Figure}[fig:sched-vis] shows the result of this command. The -t option works as before and defines the overall timeout. The options -c -p out.pgf tells the visualizer to generate a TikZ picture. If this option is omitted, the tool instead opens a window that shows the schedules. Finally, the tool expects a list of pre-schedules to visualize.

Since the different strategies are all used for roughly the same timeout, every strategy is shown as a block of similar size. Because some strategies are used for less than one second, there is a small gap of 0.1 seconds at the end. By default the visualizer simply assigns a number to each strategy when it is used the first time. Strategies often correspond to command line options and those can be long. A number ensures that there are no printing problems, but makes it possible to compare different schedules based on the same strategies.

It is possible to customize the names used for some strategies and to highlight them. This is done with the help of a shorthand file: a CSV file with three columns. As in all other CSV files, the fields are separated by a semicolon and there must be a header line. The strategy column lists the full strategy string, the shorthand column gives the name that should be printed, and the highlight can be set to true to indicate that the strategy should be highlighted (false otherwise). Strategies not listed in the shorthand files get assigned a number and stay unhighlighted. In \in{Figure}[fig:sched-vis] the base strategy and the second additional strategy are highlighted and every strategy has a custom shorthand name. The command to produce this figure is:

$ schedgen-visualize.py -t 6 -c -p out.pgf \
    -a contrib/example_shorthand.csv \
    contrib/example_schedule.csv

Let us now simulate the generated schedule. To do so we can use the simulation tool:

$ schedgen-simulate.py -l UF -t 6 \
    -c -d contrib/example_data.csv \
    --mu 0.05 --sigma 0.01 --seed 1 \
    contrib/example_schedule.csv simulation_1.txt 

The options -l, -t, -c, and -d are as for the other tools. The tool expects two positional arguments.First, the schedule to simulate and; second, the file to write the results to. The output is always using the GridTPT format, independent of the input format. The remaining options are --mu, --sigma, and --seed. Those control the random jitter that is applied to each solving time in the input dataset. The jitter is sampled from a normal distribution. The options --mu and --sigma control the mean and the standard deviation, respectively. To ensure simulations can be repeated it is possible to fix an integer seed for the random number generator with the option --seed. In this case we choose a slight jitter.

The cumulative density functions generated by the simulation are shown in the figure above. As expected, the graph for the simulation with slight jitter follows almost exactly the base strategy for the first second. The plot also shows the result of using more jitter (μ = 0.2, σ = 0.05). In this case two benchmarks are no longer solved. The script used to generate these graphs is the script contrib/cdf.py in the repository.

If we want to have a list of the benchmarks not solved by the schedule, we can use the schedgen-query tool:

$ schedgen-query.py -c -d contrib/example_data.csv \
    -q unsolved contrib/example_schedule.csv
special01.smt2
unsolved.smt2

The option -q unsolved asks the tool to print the list of all benchmarks not solved. An alternative is -q compare that shows benchmarks not solved by any strategy. To see the benchmarks that are solved by any strategy together with the minimal solving time, the -q best option can be used. Finally, -q schedule lists all benchmarks solved by the given schedule together with the predicted solving time (without jitter).