DOI: 10.5281/zenodo.15741417
title: Benchmark repository for "An Optimization Modulo Theories-based Approach to Cumulative Scheduling with Delays" 2025

description: Benchmarks and benchmark generation scripts for "An Optimization Modulo Theories-based Approach to Cumulative Scheduling with Delays" 2025.

L24.zip consists of benchmarks with the local wwtp 24-hour data.L1104.zip consists of benchmarks with the local wwtp 1104-hour data.

The above two sets of benchmarks are based on data from Helsinki Region Environmental Services Authority (HSY), Finland.

B24.zip consists of benchmarks with BMM2016 real data (https://arxiv.org/abs/1609.05367); B24 has been previously published in BMM2016 (without d_{w,t} values and startLevel_w).

See README.md for details on poetry usage and benchmark generation.

Poetry is needed for benchmark generation (alternatively, all python module imports need to be modified)

`poetry run ./src/wwtp/generate-benchmarks.py -h` for help with the benchmark generation parameters

 

README.md:



# SMT25


## Benchmarks

B24.zip has benchmarks with BMM2016 real data (with artificial delay values and startLevel=0)

L24.zip has benchmarks with the local wwtp 24-hour data

L1104.zip has benchmarks with the local wwtp 1104-hour data


## Prior to benchmark generation

1. `$ cd zenodo-wwtp`, **run all subsequent commands from there only** (parent dir of 'src/': because Poetry is used)


if you want to generate benchmarks yourself (**Benchmark generation commands** below),


2. `unzip solver-binaries.zip` (if you want to generate CP benchmarks, this is needed)

(Poetry version I use: 1.8.4. Installation: `$ curl -sSL https://install.python-poetry.org | python3 - --version 1.8.4`)

3. ` ../zenodo-wwtp/$ poetry shell`

4. `../zenodo-wwtp/$ poetry install` (installs Z3 API, Gurobi API, pandas, Minizinc API, etc)


## Benchmark generation commands

These have already been generated, and can be found in 'instances/': B24.zip, L24.zip and L1104.zip

Descriptions and estimated instance generation times:


1. B24 benchmarks, 12 seconds to generate

` ../zenodo-wwtp/$ poetry run python3 src/wwtp/generate-benchmarks.py --data B24 --sol gurobi z3 --cap 5000 6000 100 --single 50_000 --delays both --val both`

- generates 576 benchmarks

- unzipped size: 230.2 MB


2. L24 benchmarks, 4 seconds to generate

` ../zenodo-wwtp/$ poetry run python3 src/wwtp/generate-benchmarks.py --data L24 --sol gurobi z3 --cap 12_000 30_000 2000 --single 50_000 --delays both --val both`

- generates 528 instances

- unzipped size: 36.3 MB


3. L1104 benchmarks, **2 min 34 seconds** to generate

` ../zenodo-wwtp/$ poetry run python3 src/wwtp/generate-benchmarks.py --data L1104 --sol gurobi z3 --cap 17_000 30_000 1000 --single 50_000 --delays both --val both`

- generates 720 instances

- **unzipped size: 2.3 GB**, zipped 313 MB


The `--sol z3` is used for generating .smt2 instances, `--sol gurobi` for generating .mps instances. `--cap` is for MaxCapacities, `--single 50_000` adds the MaxCapacity of 50 000 that is not in the range specified by `--cap`, `--val both` is for generating both benchmarks with ints and benchmarks with reals (QF_LIA and QF_LRA for Z3).


## If you also want CP benchmarks

`--sol chuffed` option creates .fzn instances for Chuffed specifically, `--sol gecode` for Gecode:

Writing .fzn instances from .mzn is ultimately done (automatically) by the following command: `solver-binaries/MiniZincIDE-2.8.7-bundle-linux-x86_64/bin/minizinc --solver <solvername> -c <mzn_file> <datafile.dzn>`. This binary is provided in this dir (unzip solver-binaries.zip for this). Each 'datafile.dzn' file is generated temporarily and is automatically removed after use. Each .dzn file has a single row, 'PlantCapacity = \<integer value\>'