CDMOproject

Project for the Combinatorial Decision Making & Optimization course of the MAster's Degree in Artificial Intelligence of UniBo

Docker usage (quick guide)

WARNING: The Dockerfile was tested on both x86 and arm architectures (for arm you need to add the flag when building the image: --platform linux/amd64), but the SMT solver CVC5 is not set up to work on arm architecture.

This README explains how to build and run the project image using only Docker CLI. It documents the available flags that the container entrypoint accepts, shows concrete examples, and lists the available versions and which version token to pass when you want to run a specific experiment.

All commands assume you run them from the project root where the Dockerfile and the source/ directory live.

---

Build the Docker image

Build the image once (from project root):

docker build -t sts-container .

---

Mount host folders into the container

You should mount your working source/ and res/ directories into the container so the container uses your code and writes outputs back to the host:

# Unix / macOS (bash / zsh)
-v "$(pwd)/source:/CDMO/source" -v "$(pwd)/res:/CDMO/res"

On PowerShell use ${PWD} instead of $(pwd).

---

Entrypoint behavior & supported flags

The container entrypoint accepts two styles of invocation:

1. No arguments (batch mode) If you run the container without passing any arguments, the entrypoint will sequentially run every approach and runs the same scripts that genereted the json files: CP, SMT, MIP — invoking python /CDMO/source/<APPROACH>/main.py for each approach with default parameters.

   docker run --rm \
     -v "$(pwd)/source:/CDMO/source" \
     -v "$(pwd)/res:/CDMO/res" \
     sts-container

2. Only the approach The entrypoint will run a single approach only, that generate the json files in /CDMO/res/<APPROACH>/n.json.

   docker run --rm -v "$(pwd)/source:/CDMO/source" -v "$(pwd)/res:/CDMO/res" \
     sts-container MIP

3. Single-approach mode (positional or flag style) If you pass arguments, the entrypoint will run a single approach and a single verion among the possible (see underneath) only.

   • Positional form:

     docker run --rm -v "$(pwd)/source:/CDMO/source" -v "$(pwd)/res:/CDMO/res" \
       sts-container MIP 8 v1

     This runs python /CDMO/source/MIP/main.py --instance 8 --version v1.

   • Flag form:

     docker run --rm -v "$(pwd)/source:/CDMO/source" -v "$(pwd)/res:/CDMO/res" \
       sts-container -- --approach MIP --n 8 --version v1

     This runs the same main.py and forwards --n 8 --version v1.

Supported flags (forwarded by the entrypoint)

• --approach <APPROACH> — one of CP, SMT, MIP (case-insensitive).
• --n or --instance <int> — instance size (even integer).
• --version <str> — version token (e.g. v1).
• -h, --help — show help (entrypoint prints usage).

---

CP: available versions

The following list serves as index to know which version runs a particular model (all the cited model are described in the report).

version	meaning / which implementation is used
v1	Will run the naive_model not balanced, with 'gecode' solver
v2	Will run the better_model not balanced, with 'gecode' solver
v3	Will run the better_model not balanced, with 'chuffed' solver
v4	Will run the better_model_chan not balanced, with 'chuffed' solver
v5	Will run the circle_met_model not balanced, with 'chuffed' solver
v6	Will run the circle_met_model_chan, not balanced, with 'chuffed' solver
v7	Will run the circle_met_model_chan, balanced with HAP_v1, with 'chuffed' solver
v8	Will run the circle_met_model_chan, balanced with HAP_v2, with 'chuffed' solver

---

SMT: available versions

This is the list of the versions which are available for SMT.

version	meaning / which implementation is used
v1	Will run the model with the Z3 solver on the pysmt encoding in decision version
v2	Will run the model with the Z3 solver on the pysmt encoding in optimization version
v3	Will run the model with the CVC5 solver on the pysmt encoding in decision version
v4	Will run the model with the CVC5 solver on the pysmt encoding in optimization version
v5	Will run the model with the OptiMathSAT solver on the pysmt encoding in decision version
v6	Will run the model with the OptiMathSAT solver on the pysmt encoding in optimization version
v7	Will run the model with the Z3 solver on the Z3py encoding in decision version
v8	Will run the model with the Z3 solver on the Z3py encoding in optimization version
v9	Will run the model with the CVC5 solver on the Z3py encoding in decision version
v10	Will run the model with the CVC5 solver on the Z3py encoding in optimization version
v11	Will run the model with the OptiMathSAT solver on the Z3py encoding in decision version
v12	Will run the model with the OptiMathSAT solver on the Z3py encoding in optimization version

Single-version mode

• When just --version is passed, that version is run with all the even instances from 4 to 18;
• When just --n is passed, that instance is run with all the twelve versions;
• When both --version and --n are passed, then the chosen instance on the chosen version is performed;
• When none of the two is passed, all the feasible instances will be run, so the one which on the report timeout, will not run.

---

MIP: available versions

This is the list of the versions which are available for MIP.

version	meaning / which implementation is used
v1	the best CBC and GLPK base — feasible model
v2	Useful to verify the behaviour of CBC i!=j and compare it to v1/v3.
v3	the best CBC and GLPK i<j-balanced.
v4	the best CBC and GLPK pre - feasible/balanced.
v5	seed-sensitivity sweep — runs the same CBC base-feasible case over many seeds (0, 1234567, 26, 42, 262626, 424242, 878641, 5656565). Usefull to see how changing seed, changes the the performance of the same model.
v6	GLPK robustness & cuts — multiple GLPK combos (seeds, cuts on/off, base vs i<j) usefull to check the performance of GLPK
v7	Runs a CBC-balanced instance over some seeds using the $obj_{func}$ $min-max$ and the $min-sum$ versions.

Where results are written

• Batch mode (no args): the MIP batch writes files into:

  /CDMO/res/MIP/{nn}.json
  

• Single-version mode (when you pass --version and --instance) the script writes to:

  /CDMO/res/additional_tests/{n}.json
  

Entrypoint interactive shell in the container (dev debugging)

If you want a shell inside the image (mounting your source/res), decomment the dev code inside the dockerfile and comment the part about PRODUCTION script.
Build the new image and run the command:

docker run --rm -it \
  -v "$(pwd)/source:/CDMO/source" \
  -v "$(pwd)/res:/CDMO/res" \
  sts-container /bin/bash

Then you can run commands manually inside the container, e.g.:

python /CDMO/source/MIP/main.py --instance 8 --version v1