Saved in:
| Main Authors: | , |
|---|---|
| Format: | Recurso digital |
| Language: | |
| Published: |
Zenodo
2025
|
| Online Access: | https://doi.org/10.5281/zenodo.15741417 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Table of Contents:
- <p>Benchmarks and benchmark generation scripts for "An Optimization Modulo Theories-based Approach to Cumulative Scheduling with Delays" 2025.</p> <p>L24.zip consists of benchmarks with the local wwtp 24-hour data.<br>L1104.zip consists of benchmarks with the local wwtp 1104-hour data.</p> <p>The above two sets of benchmarks are based on data from Helsinki Region Environmental Services Authority (HSY), Finland.</p> <p>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).</p> <p>See README.md for details on poetry usage and benchmark generation.</p> <p>Poetry is needed for benchmark generation (alternatively, all python module imports need to be modified)</p> <p>`poetry run ./src/wwtp/generate-benchmarks.py -h` for help with the benchmark generation parameters</p> <p> </p> <p><strong>README.md</strong>:</p> <div> <div># SMT25</div> <br> <div>## Benchmarks</div> <div>B24.zip has benchmarks with BMM2016 real data (with artificial delay values and startLevel=0)</div> <div>L24.zip has benchmarks with the local wwtp 24-hour data</div> <div>L1104.zip has benchmarks with the local wwtp 1104-hour data</div> <br> <div>## Prior to benchmark generation</div> <div>1. `$ cd zenodo-wwtp`, **run all subsequent commands from there only** (parent dir of 'src/': because Poetry is used)</div> <br> <div>if you want to generate benchmarks yourself (**Benchmark generation commands** below),</div> <br> <div>2. `unzip solver-binaries.zip` (if you want to generate CP benchmarks, this is needed)</div> <div>(Poetry version I use: 1.8.4. Installation: `$ curl -sSL https://install.python-poetry.org | python3 - --version 1.8.4`)</div> <div>3. ` ../zenodo-wwtp/$ poetry shell`</div> <div>4. `../zenodo-wwtp/$ poetry install` (installs Z3 API, Gurobi API, pandas, Minizinc API, etc)</div> <br><br> <div>## Benchmark generation commands</div> <div>These have already been generated, and can be found in 'instances/': B24.zip, L24.zip and L1104.zip</div> <div>Descriptions and estimated instance generation times:</div> <br> <div>1. B24 benchmarks, 12 seconds to generate</div> <div>` ../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`</div> <div>- generates 576 benchmarks</div> <div>- unzipped size: 230.2 MB</div> <br> <div>2. L24 benchmarks, 4 seconds to generate</div> <div>` ../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`</div> <div>- generates 528 instances</div> <div>- unzipped size: 36.3 MB</div> <br> <div>3. L1104 benchmarks, **2 min 34 seconds** to generate</div> <div>` ../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`</div> <div>- generates 720 instances</div> <div>- **unzipped size: 2.3 GB**, zipped 313 MB</div> <br> <div>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).</div> <br><br> <div>## If you also want CP benchmarks</div> <div>`--sol chuffed` option creates .fzn instances for Chuffed specifically, `--sol gecode` for Gecode:</div> <div>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\>'</div> </div>