Benchmark repository for "An Optimization Modulo Theories-based Approach to Cumulative Scheduling with Delays" 2025

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\>'