planning_SAT.py

# -*- coding: utf-8 -*-
"""
Created on Mon Jul 21 16:56:07 2025

@author: yan-s

Summary of the scheduling problem under constraints (SAT)

Goal:
Generate a work schedule assigning 20 people to posts (stations) over 14 days:

* Days 1 to 6: 11 daytime stations per day
* Day 7 (Sunday): 12 daytime stations
* Nights 8 to 14: 5 night stations per night

The objective is to assign one person per station while respecting constraints on capacity, work distribution, and rest.

Constraints:
C1: Each station must be occupied by exactly one person.
C2: A person can only be assigned to one post per day or night.
C3: Maximum of 4 worked days among days 1 to 6.
C4: Minimum of 2 worked days among days 1 to 6.
C5: Maximum of 3 total assignments between Sunday (day 7) and nights (days 8 to 14).
C6: Minimum of 1 total assignment between Sunday (day 7) and nights (days 8 to 14).
C7: Mandatory rest: if a person works a night (days 8–14), they cannot work the following day.

Modeling:
Variables are named x_p_d_s, where:

* p is the person ID (1 to 20)
* d is the day or night (1 to 14)
* s is the station of the day or night

A variable x_p_d_s is true if person p is assigned to station s on day or night d.

Constraints are encoded as clauses in conjunctive normal form (CNF) for a SAT solver.

Encodings:

* Constraints C1 and C1b use inclusion clauses (at least one person per station) and exclusion clauses (no two people in the same station, or no one person in two stations on the same day).
* Constraints C2A and C2B use auxiliary variables z_p_d indicating if a person works on a given day, then forbid all combinations exceeding the allowed threshold.
* Constraint C3 encodes that if a person works a given night, they cannot be assigned to a station the next day (except Sunday).

Solving:
The CNF clauses are given to a SAT solver (PySAT). If the problem is satisfiable (SAT), a solution is extracted:

* A tabular schedule file "planning_table.csv" organizes assignments by station, with one column per day and night.

Libraries used:

* PySAT: SAT encoding and solving
* itertools: for generating combinations in cardinality constraints
* csv, pandas: to produce readable output files
"""

import pandas as pd
from typing import List
from pysat.formula import CNF, IDPool
from pysat.solvers import Solver
from itertools import combinations

# === Parameters ===
nb_semaines = 3
nb_personnes = 20

stations_jour = 11
stations_dimanche = 12
stations_nuit = 5

# Per week
max_jour = 4
min_jour = 2
max_nuit = 3
min_nuit = 1

# Create days
all_days = []
day_stations = {}
night_stations = {}

for s in range(nb_semaines):
    base = s * 14
    for i in range(7):
        jour_id = base + i * 2
        nuit_id = jour_id + 1
        day_stations[jour_id] = stations_dimanche if i == 6 else stations_jour
        night_stations[nuit_id] = stations_nuit
        all_days.extend([jour_id, nuit_id])

varpool = IDPool()
cnf = CNF()

# === Helper functions ===
def inv_var_id(v: int):
    """Inverse varpool.id: return (p, d, s) from an encoded positive integer."""
    name = varpool.obj(v)
    _, p, d, s = name.split("_")
    return int(p), int(d), int(s)

def write_planning_csv_table(model: List[int], filename: str = "planning_table.csv"):
    # Initialization: (day/night, week, day_of_week) → {station: person}
    shifts = {("day", s, d): {} for s in range(nb_semaines) for d in range(1, 8)}
    shifts.update({("night", s, d): {} for s in range(nb_semaines) for d in range(1, 8)})

    for v in model:
        if v > 0 and varpool.obj(v).startswith("x_"):
            p, d, station = inv_var_id(v)
            semaine = d // 14
            jour_semaine = (d % 14) // 2 + 1  # 1 to 7

            if d % 2 == 0:
                shifts[("day", semaine, jour_semaine)][station] = p
            else:
                shifts[("night", semaine, jour_semaine)][station] = p

    # Create columns: S1 - Monday - day, S1 - Monday - night, ..., S2 - Sunday - night
    cols = ["station"]
    for s in range(nb_semaines):
        for d in range(1, 8):
            cols.append(f"S{s+1}_day{d}")
            cols.append(f"S{s+1}_night{d}")

    rows = []

    # Day stations (1 to 12)
    for s_id in range(1, 13):
        row = {"station": s_id}
        for s in range(nb_semaines):
            for d in range(1, 8):
                row[f"S{s+1}_day{d}"] = shifts[("day", s, d)].get(s_id, 0)
                row[f"S{s+1}_night{d}"] = 0
        rows.append(row)

    # Night stations (13 to 17)
    for s_id in range(1, 6):
        row = {"station": 12 + s_id}
        for s in range(nb_semaines):
            for d in range(1, 8):
                row[f"S{s+1}_day{d}"] = 0
                row[f"S{s+1}_night{d}"] = shifts[("night", s, d)].get(s_id, 0)
        rows.append(row)

    # Final export
    df = pd.DataFrame(rows, columns=cols)
    df.to_csv(filename, index=False)
    print(f"CSV file generated: {filename}")


# === Constraints ===

# C1: Each station is occupied by exactly one person
for d in all_days:
    num_slots = day_stations.get(d, night_stations.get(d))
    for s in range(1, num_slots + 1):
        lits = [varpool.id(f"x_{p}_{d}_{s}") for p in range(1, nb_personnes + 1)]
        cnf.append(lits)
        for i in range(len(lits)):
            for j in range(i + 1, len(lits)):
                cnf.append([-lits[i], -lits[j]])

# C2: A person can only take one station per day/night (pairwise encoding)
for p in range(1, nb_personnes + 1):
    for d in all_days:
        num_slots = day_stations.get(d, night_stations.get(d))
        lits = [varpool.id(f"x_{p}_{d}_{s}") for s in range(1, num_slots + 1)]
        for i in range(len(lits)):
            for j in range(i + 1, len(lits)):
                cnf.append([-lits[i], -lits[j]])

# C3: Max 4 worked days (days 1 to 6)
for p in range(1, nb_personnes + 1):
    for s in range(nb_semaines):
        base = s * 14
        z_vars = []
        for i in range(6):  # days 1 to 6
            jour = base + i * 2  # 0, 2, 4, 6, 8, 10
            z = varpool.id(f"z_{p}_{jour}")
            z_vars.append(z)
            v_p_d_s = [varpool.id(f"x_{p}_{jour}_{slot}") for slot in range(1, day_stations[jour] + 1)]
            cnf.append([-z] + v_p_d_s)
            for v in v_p_d_s:
                cnf.append([-v, z])
        for combo in combinations(z_vars, max_jour + 1):
            cnf.append([-v for v in combo])

# C4: Min 2 worked days (days 1 to 6)
for p in range(1, nb_personnes + 1):
    for s in range(nb_semaines):
        z_vars = [varpool.id(f"z_{p}_{s * 14 + i * 2}") for i in range(6)]
        for combo in combinations(z_vars, len(z_vars) - min_jour + 1):
            cnf.append(list(combo))

# C5: Max 3 Sundays+nights (days 7 to 14)
for p in range(1, nb_personnes + 1):
    for s in range(nb_semaines):
        base = s * 14
        z_vars = []

        # Sunday (last day)
        jour = base + 12
        z = varpool.id(f"z_{p}_{jour}")
        z_vars.append(z)
        v_p_d_s = [varpool.id(f"x_{p}_{jour}_{slot}") for slot in range(1, day_stations[jour] + 1)]
        cnf.append([-z] + v_p_d_s)
        for v in v_p_d_s:
            cnf.append([-v, z])

        # Nights (odd ids)
        for i in range(7):
            nuit = base + i * 2 + 1  # 1, 3, 5, ...
            z = varpool.id(f"z_{p}_{nuit}")
            z_vars.append(z)
            v_p_d_s = [varpool.id(f"x_{p}_{nuit}_{slot}") for slot in range(1, night_stations[nuit] + 1)]
            cnf.append([-z] + v_p_d_s)
            for v in v_p_d_s:
                cnf.append([-v, z])

        for combo in combinations(z_vars, max_nuit + 1):
            cnf.append([-v for v in combo])


# C6: Min 1 Sunday+night (days 7 to 14)
for p in range(1, nb_personnes + 1):
    for s in range(nb_semaines):
        base = s * 14
        z_vars = [varpool.id(f"z_{p}_{base + 12}")]  # Sunday
        z_vars += [varpool.id(f"z_{p}_{base + i * 2 + 1}") for i in range(7)]  # nights
        for combo in combinations(z_vars, len(z_vars) - min_nuit + 1):
            cnf.append(list(combo))

# C7: Mandatory rest after a night
for p in range(1, nb_personnes + 1):
    for s in range(nb_semaines):
        base = s * 14
        for i in range(6):  # nights Monday to Saturday
            nuit_id = base + i * 2 + 1      # 1, 3, 5, 7, 9, 11
            jour_suivant = nuit_id + 1      # 2, 4, 6, 8, 10, 12
            if jour_suivant not in day_stations:
                continue
            for sn in range(1, night_stations[nuit_id] + 1):
                xn = varpool.id(f"x_{p}_{nuit_id}_{sn}")
                for sd in range(1, day_stations[jour_suivant] + 1):
                    xd = varpool.id(f"x_{p}_{jour_suivant}_{sd}")
                    cnf.append([-xn, -xd])

# === Solving
with Solver(bootstrap_with=cnf.clauses) as solver:
    if solver.solve():
        model = solver.get_model()
        assignments = []
        for lit in model:
            if lit > 0 and varpool.obj(lit).startswith("x_"):
                p, d, s = inv_var_id(lit)
                assignments.append((p, d, s))

        print(f"{len(assignments)} assignments!")

        # Export readable table
        write_planning_csv_table(model)
    else:
        print("UNSAT: constraint too strong.")


"""
TO DO:
    - Add option with one free week
    - Separate Sunday and night
    - Clean functions + add comments
    - Optimize (use built-in function instead of combinations)
    - Switch to OOP ==> idea is to create at_least_one etc. methods on objects
    - Better file handling
    - Handle exceptions
    - Directly integrate planning_transformer
    - GUI?

NB: review overall logic;
    1. create a .json configuration file (people, stations)
    2. apply constraints and run + save a model
    3. transform into a schedule
"""