Single Round Robin tournament scheduling problem

This repository contains the project for the Combinatorial Decision Making and Optimization course in the Master’s Degree in Artificial Intelligence at the University of Bologna.

Build and Run Instructions

This project implements four modelling approaches (CP, SAT, SMT, MIP). All experiments—single-instance execution or full-batch runs—can be reproduced without modifying the source code, using only command-line arguments.

1. Project Structure

CDMO-PROJECT/
├── output/
├── res/
│   ├── CP/
│   ├── MIP/
│   ├── SAT/
│   └── SMT/
├── source/
│   ├── CP/
│   ├── MIP/
│   ├── SAT/
│   ├── SMT/
│   ├── utils/
│   |   ├── __init__.py
│   |   ├── utils.py
|   ├── main.py
│   ├── run_cp.py
│   ├── run_mip.py
│   ├── run_sat.py
│   ├── run_smt.py
│   ├── solution_checker.py
│   └── tables.py
├── Dockerfile
├── docker-compose.yml
├── setup.bat
├── setup.bash
└── ...

Each model is implemented inside its own subfolder (source/CP, source/SMT, etc.). The Dockerfile builds an image capable of running all models.

2. Building and Running the Docker Environment

0. You need Python, pip and docker installed.
1. Run the setup script in order to build the container (This step is needed everytime the code is edited). On windows CMD:

    setup.bat

On MacOS/Linux:

    bash setup.sh

macOS users: If running ./setup.sh gives errors like command not found or unknown docker command: "compose build\r", it may be due to Windows-style line endings. Fix it by running:

sed -i '' 's/\r$//' setup.sh
chmod +x setup.sh

2. Now you can execute from the terminal commands like:

    python source/main.py --mode CP SMT MIP SAT --range 1 45 --check
    python source/run_cp.py --range 1 45 --obj true

3. To stop the container use the following commands:

    exit
    docker-compose stop

In alternative to docker-compose stop the command docker-compose down can be used to DELETE the container from your machine.

3. Running the Project

The project can be executed in two ways:

• 3.1. Running all solver via a the unified main.py interface
• 3.2. Individual solver scripts (run_cp.py, run_sat.py, run_smt.py, run_mip.py)

3.1. Running All Solvers

main.py provides a single command to reproduce all experimental results.

python source/main.py --mode CP SAT SMT MIP --range 1 18 --check

This command:

• Runs every solver (CP, SAT, SMT, MIP)
• On all instances in the range [1, 18]
• Checks each generated solution
• Produces structured result files in each solver’s output directory

3.2. Running a Single Model on a Single Instance

Below are examples to run a model on a single instance for each solver:

CP Example

python source/run_cp.py --range 12 12 --solver chuffed --search ff --obj true --sb false

SAT Example

python source/run_sat.py --range 7 7 --obj false --sb both

SMT Example

python source/run_smt.py --range 3 3 --obj true

MIP Example

python source/run_mip.py --range 2 6 --solver gurobi --obj both --algo dsmplx

Arguments reference

Common to All Solvers

Argument	Meaning	Accepted Values	Required
--range	Instance interval (LOWER UPPER)	two integers	yes
--obj	Whether to run objective model variants	true, false, both	no
--sb	Whether to enable symmetry breaking	true, false, both	no

Arguments Specific to CP

Argument	Description	Values
--solver	CP solver backend	gecode, chuffed
--search	Search heuristic	base, ff, DWD+min, DWD+rand

Arguments Specific to MIP

Argument	Description	Values
--solver	MIP solver backend	cplex, gurobi, all
--algo	Solver algorithm option	default, psmplx, dsmplx, barr, all

4. Solution Validation

To separately validate the outputs produced by the different approaches, run the following command:

python source/solution_checker.py <path_to_solution_directory>

Here, <path_to_solution_directory> refers to the directory that contains the .json solution files generated by the solvers.

5. Generating Comparison Tables

The script source/tables.py automatically builds LaTeX comparison tables for all solver/model combinations using the JSON result files in res/.

You can generate tables for any subset of models and any team-size range:

python source/tables.py --range 1 18 --models CP SAT SMT MIP --obj

This command:

• Reads results from ./res/<MODEL>/<N>.json
• Produces LaTeX tables in ./output/
• Includes objective values (because of --obj)
• Uses the predefined solvers and strategies for each model

To generate decision-mode tables instead omit --obj:

python source/tables.py --range 1 18 --models CP

6. Output File Naming

JSON results use the following key pattern:

<solver>_<obj>_<sb>_<lex>_<strategy>.json

Where:

• solver – solver backend (e.g., gurobi, gecode)
• obj – obj for objective, !obj for decision
• sb – sb if symmetry-breaking enabled, !sb if disabled
• lex – lex if lexicographic ordering applied, !lex otherwise
• strategy – solver strategy or algorithm (base, ff, psmplx, etc.)

Examples:

• gurobi_obj_!sb_!lex_psmplx.json → Gurobi, objective, no symmetry-breaking, no lex, primal simplex
• gecode_!obj_sb_base.json → Gecode, decision mode, symmetry-breaking, base strategy

Example Output

Running:

python source/tables.py --range 8 14 --models CP

produces a file such as:

output/chuffed_CP_!obj.tex

containing:

Teams	chuffed+sb (base)	chuffed+sb (ff)	chuffed+sb (DWD+min)	chuffed+!sb (base)	chuffed+!sb (ff)	chuffed+!sb (DWD+min)
8	0	0	0	0	0	0
10	0	0	0	0	2	32
12	0	0	0	38	12	N/A
14	0	9	5	27	N/A	N/A

Columns are labeled with the different tried approaches, while cells contain the runtime in seconds (in the decision version) or the best objective value (in the optimization version), found by the given approach on the given instance, using a certain search strategy. If the instance is solved to optimality, the objective value is emphasized in bold. If the instance is proved to be unsatisfiable, it's indicated as ’UNSAT’. If no answer is obtained within the time limit, it's indicated with a ’N/A’.

Project Overview

This project investigates the Single Round Robin (SRR) sport-tournament scheduling problem from a combinatorial-optimisation perspective. In an SRR tournament, every team must play every other team exactly once across (n-1) weeks, with (n/2) matches played in parallel each week. We formalise the problem using a common set of instance variables (teams, weeks, periods, slots) shared across all modelling approaches.

The core decision variable assigns a team to each match position ((p,w,s)), and the schedule must satisfy four structural constraints:

1. Even number of teams
2. Each pair of teams meets exactly once
3. Each team plays exactly one match per week
4. No team appears more than twice in the same period

The optimisation objective minimises the maximum imbalance between home and away games for any team.

To study this problem, we implement and compare four modelling paradigms:

• Constraint Programming (CP)
• Boolean Satisfiability (SAT)
• Satisfiability Modulo Theories (SMT)
• Mixed-Integer Programming (MIP)

Each solver is equipped with objective and symmetry-breaking variants, unified under a single command-line interface. All experiments are reproducible using the provided Docker environment and were run under controlled conditions (single thread, 300-second time limit per instance) on an Intel i7-1165G7 host machine.