%load_ext autoreload
%autoreload 2
"""
    Some imports used throughout the notebook
"""
import time

from visualize import *

from cpmpy.transformations.normalize import toplevel_list
from factory import *
from read_data import get_data

import numpy as np
np.set_printoptions(linewidth=90)
# preload solvers
from cpmpy import SolverLookup
names = SolverLookup.solvernames()

Set parameter Username
Academic license - for non-commercial use only - expires 2024-11-09

Explainable Constraint Solving - A Hands-On Tutorial

Ignace Bleukx, Dimos Tsouros, Tias Guns

 

Hands-on: this presentation is an executable Jupyter notebook

https://github.com/CPMpy/XCP-explain

Model + Solve

• What if the model is UNSAT?
• What if the solution is unexpected?
• What if the user wants to change something?

--> Trustworthy & Explainable AI

Trustworthy & Explainable constraint solving

Human-aware AI:

• Respect human agency
• Support users in decision making
• Provide explanations and learning opportunities

Acknowledges that a 'model' is only an approximation,
that it might result in undesirable solutions.

Explainable AI (XAI), brief highlights

D. Gunning, 2015: DARPA XAI challenge

"Every explanation is set within a context that depends..." -> domain dependent

M. Fox et al, 2017: Explainable Planning

Need for trust, interaction and transparancy.

T. Miller, 2018: Explainable AI: Beware of Inmates Running the Asylum

Insights from the social sciences: Someone explains something to someone

R. Guidotti, 2018: A survey of methods for explaining black box ML models

The vast majority of work/attention...

'Explaining' constraint propagation?

Concept from Lazy Clause Generation / CP-SAT solvers (Stuckey, 2010)

"every time a propagator determines a domain change of a variable,
it records a clause that explains the domain change."

• someone: one propagator
• something: a clause (disjunction of literals)
• to someone: a SAT solver, not a person

Explainable Constraint Programming (XCP)

In general, "Why X?"        (with X a solution or UNSAT)

To be defined...

Explainable Constraint Programming (XCP)

In general, "Why X?"        (with X a solution or UNSAT)

To be defined... 3 patterns:

• Causal explanation:
  • How was X derived?
• Contrastive explanation:
  • Why X and not Z?
• Conversational explanation:
  • Iteratively refine explanation & model

Causal explanation, mode of interaction:

Then what?

Then what?

1. User is happy with the answer
   (e.g. better understands the problem)
2. User changes the answer and uses that
   (solution interaction; no solver involvement)
3. User changes the model and reiterates
   (e.g. better understands how to model the problem)
4. User interacts with interactive system
   (e.g. conversational explanations)

Hands-on Explainable Constraint Programming (XCP)

• The model: Nurse Rostering
• The system: CPMpy modeling library
• Explain UNSAT:
  • Causal explanations (MUS, OUS, sequence)
  • Conversational explanations
• Explain a solution:
  • Causal explanations
  • Contrastive explanations

The model: Nurse Scheduling

• The assignment of shifts and holidays to nurses.
• Each nurse has their own restrictions and preferences, as does the hospital.

Nurse Rostering: data

Instances from http://www.schedulingbenchmarks.org/

"benchmark test instances from various sources including industrial collaborators and scientific publications."

#instance = "http://www.schedulingbenchmarks.org/nrp/data/Instance1.txt"
instance = "Benchmarks/Instance1.txt"
data = get_data(instance)

# all data is stored as DataFrame tables
data.staff

	# ID	MaxShifts	MaxTotalMinutes	MinTotalMinutes	MaxConsecutiveShifts	MinConsecutiveShifts	MinConsecutiveDaysOff	MaxWeekends	D	name
0	A	D=14	4320	3360	5	2	2	1	14	Megan
1	B	D=14	4320	3360	5	2	2	1	14	Katherine
2	C	D=14	4320	3360	5	2	2	1	14	Robert
3	D	D=14	4320	3360	5	2	2	1	14	Jonathan
4	E	D=14	4320	3360	5	2	2	1	14	William
5	F	D=14	4320	3360	5	2	2	1	14	Richard
6	G	D=14	4320	3360	5	2	2	1	14	Kristen
7	H	D=14	4320	3360	5	2	2	1	14	Kevin

print("Nr of days to schedule:", data.horizon)
print("Nr of shift types:", len(data.shifts))

pd.merge(data.days_off, data.staff[["# ID","name"]], left_on="EmployeeID", right_on="# ID", how="left")

Nr of days to schedule: 14
Nr of shift types: 1

	DayIdx	# ID	name
0	0	A	Megan
1	5	B	Katherine
2	8	C	Robert
3	2	D	Jonathan
4	9	E	William
5	5	F	Richard
6	1	G	Kristen
7	7	H	Kevin

Nurse Rostering: constraints 1/2

hospital constraints/preferences:

• nb of nurses assigned
• max nb of shifts
• max nb of weekend shifts
• min nb of (consecutive) days off
• min/max minutes worked
• min/max consecutive shifts
• shift rotation

Nurse Rostering: constraints 2/2

nurse constraints/preferences:

• specific days off-duty
• specific shift requests (on/off)

The system: http://cpmpy.readthedocs.io

CPMpy is a Constraint Programming and Modeling library in Python,
based on numpy, with direct solver access.

Features used in this tutorial:

• Easy integration with visualisation tools (pandas, matplotlib)
• Object-oriented programming (constraints are Python objects we can create, copy, update)
• Repeatedly solving subsets of constraints (assumption variables)
• Incremental solving (e.g. SAT, MIP/Hitting set)

Nurse Rostering in CPMpy

Variables:

assignment of shift types (0=none) to nurses

nurse_view = cp.intvar(0, len(data.shifts), # lb, ub
                       shape=(len(data.staff), data.horizon),
                       name="nv")
nurse_view

NDVarArray([[nv[0,0], nv[0,1], nv[0,2], nv[0,3], nv[0,4], nv[0,5], nv[0,6], nv[0,7],
             nv[0,8], nv[0,9], nv[0,10], nv[0,11], nv[0,12], nv[0,13]],
            [nv[1,0], nv[1,1], nv[1,2], nv[1,3], nv[1,4], nv[1,5], nv[1,6], nv[1,7],
             nv[1,8], nv[1,9], nv[1,10], nv[1,11], nv[1,12], nv[1,13]],
            [nv[2,0], nv[2,1], nv[2,2], nv[2,3], nv[2,4], nv[2,5], nv[2,6], nv[2,7],
             nv[2,8], nv[2,9], nv[2,10], nv[2,11], nv[2,12], nv[2,13]],
            [nv[3,0], nv[3,1], nv[3,2], nv[3,3], nv[3,4], nv[3,5], nv[3,6], nv[3,7],
             nv[3,8], nv[3,9], nv[3,10], nv[3,11], nv[3,12], nv[3,13]],
            [nv[4,0], nv[4,1], nv[4,2], nv[4,3], nv[4,4], nv[4,5], nv[4,6], nv[4,7],
             nv[4,8], nv[4,9], nv[4,10], nv[4,11], nv[4,12], nv[4,13]],
            [nv[5,0], nv[5,1], nv[5,2], nv[5,3], nv[5,4], nv[5,5], nv[5,6], nv[5,7],
             nv[5,8], nv[5,9], nv[5,10], nv[5,11], nv[5,12], nv[5,13]],
            [nv[6,0], nv[6,1], nv[6,2], nv[6,3], nv[6,4], nv[6,5], nv[6,6], nv[6,7],
             nv[6,8], nv[6,9], nv[6,10], nv[6,11], nv[6,12], nv[6,13]],
            [nv[7,0], nv[7,1], nv[7,2], nv[7,3], nv[7,4], nv[7,5], nv[7,6], nv[7,7],
             nv[7,8], nv[7,9], nv[7,10], nv[7,11], nv[7,12], nv[7,13]]], dtype=object)

Constraints:

Specific days off-duty

for (empl_id, row) in data.days_off.iterrows():
    empl_idx = data.staff.index[data.staff["# ID"] == empl_id][0]
    day_idx = row["DayIdx"]
    
    con = (nurse_view[empl_idx, day_idx] == 0)
    
    con.set_description(f"{data.staff.iloc[empl_idx]['name']} should not work on day {day_idx}")
    print("-",con)

- Megan should not work on day 0
- Katherine should not work on day 5
- Robert should not work on day 8
- Jonathan should not work on day 2
- William should not work on day 9
- Richard should not work on day 5
- Kristen should not work on day 1
- Kevin should not work on day 7

Max consecutive shifts constraints:

for nurse_id, row in data.staff.iterrows():
    max_days = row["MaxConsecutiveShifts"]
    
    # post on rolling window: in max_days+1 window, at least one day off
    k = max_days+1
    for i in range(data.horizon - max_days):
        con = cp.Count(nurse_view[nurse_id, i:i+k], 0) >= 1
        
        con.set_description(f"{row['name']} can work at most {max_days} days in a row")
        print("-",con, "-", con.__repr__())

- Megan can work at most 5 days in a row - count([nv[0,0],nv[0,1],nv[0,2],nv[0,3],nv[0,4],nv[0,5]],0) >= 1
- Megan can work at most 5 days in a row - count([nv[0,1],nv[0,2],nv[0,3],nv[0,4],nv[0,5],nv[0,6]],0) >= 1
- Megan can work at most 5 days in a row - count([nv[0,2],nv[0,3],nv[0,4],nv[0,5],nv[0,6],nv[0,7]],0) >= 1
- Megan can work at most 5 days in a row - count([nv[0,3],nv[0,4],nv[0,5],nv[0,6],nv[0,7],nv[0,8]],0) >= 1
- Megan can work at most 5 days in a row - count([nv[0,4],nv[0,5],nv[0,6],nv[0,7],nv[0,8],nv[0,9]],0) >= 1
- Megan can work at most 5 days in a row - count([nv[0,5],nv[0,6],nv[0,7],nv[0,8],nv[0,9],nv[0,10]],0) >= 1
- Megan can work at most 5 days in a row - count([nv[0,6],nv[0,7],nv[0,8],nv[0,9],nv[0,10],nv[0,11]],0) >= 1
- Megan can work at most 5 days in a row - count([nv[0,7],nv[0,8],nv[0,9],nv[0,10],nv[0,11],nv[0,12]],0) >= 1
- Megan can work at most 5 days in a row - count([nv[0,8],nv[0,9],nv[0,10],nv[0,11],nv[0,12],nv[0,13]],0) >= 1
- Katherine can work at most 5 days in a row - count([nv[1,0],nv[1,1],nv[1,2],nv[1,3],nv[1,4],nv[1,5]],0) >= 1
- Katherine can work at most 5 days in a row - count([nv[1,1],nv[1,2],nv[1,3],nv[1,4],nv[1,5],nv[1,6]],0) >= 1
- Katherine can work at most 5 days in a row - count([nv[1,2],nv[1,3],nv[1,4],nv[1,5],nv[1,6],nv[1,7]],0) >= 1
- Katherine can work at most 5 days in a row - count([nv[1,3],nv[1,4],nv[1,5],nv[1,6],nv[1,7],nv[1,8]],0) >= 1
- Katherine can work at most 5 days in a row - count([nv[1,4],nv[1,5],nv[1,6],nv[1,7],nv[1,8],nv[1,9]],0) >= 1
- Katherine can work at most 5 days in a row - count([nv[1,5],nv[1,6],nv[1,7],nv[1,8],nv[1,9],nv[1,10]],0) >= 1
- Katherine can work at most 5 days in a row - count([nv[1,6],nv[1,7],nv[1,8],nv[1,9],nv[1,10],nv[1,11]],0) >= 1
- Katherine can work at most 5 days in a row - count([nv[1,7],nv[1,8],nv[1,9],nv[1,10],nv[1,11],nv[1,12]],0) >= 1
- Katherine can work at most 5 days in a row - count([nv[1,8],nv[1,9],nv[1,10],nv[1,11],nv[1,12],nv[1,13]],0) >= 1
- Robert can work at most 5 days in a row - count([nv[2,0],nv[2,1],nv[2,2],nv[2,3],nv[2,4],nv[2,5]],0) >= 1
- Robert can work at most 5 days in a row - count([nv[2,1],nv[2,2],nv[2,3],nv[2,4],nv[2,5],nv[2,6]],0) >= 1
- Robert can work at most 5 days in a row - count([nv[2,2],nv[2,3],nv[2,4],nv[2,5],nv[2,6],nv[2,7]],0) >= 1
- Robert can work at most 5 days in a row - count([nv[2,3],nv[2,4],nv[2,5],nv[2,6],nv[2,7],nv[2,8]],0) >= 1
- Robert can work at most 5 days in a row - count([nv[2,4],nv[2,5],nv[2,6],nv[2,7],nv[2,8],nv[2,9]],0) >= 1
- Robert can work at most 5 days in a row - count([nv[2,5],nv[2,6],nv[2,7],nv[2,8],nv[2,9],nv[2,10]],0) >= 1
- Robert can work at most 5 days in a row - count([nv[2,6],nv[2,7],nv[2,8],nv[2,9],nv[2,10],nv[2,11]],0) >= 1
- Robert can work at most 5 days in a row - count([nv[2,7],nv[2,8],nv[2,9],nv[2,10],nv[2,11],nv[2,12]],0) >= 1
- Robert can work at most 5 days in a row - count([nv[2,8],nv[2,9],nv[2,10],nv[2,11],nv[2,12],nv[2,13]],0) >= 1
- Jonathan can work at most 5 days in a row - count([nv[3,0],nv[3,1],nv[3,2],nv[3,3],nv[3,4],nv[3,5]],0) >= 1
- Jonathan can work at most 5 days in a row - count([nv[3,1],nv[3,2],nv[3,3],nv[3,4],nv[3,5],nv[3,6]],0) >= 1
- Jonathan can work at most 5 days in a row - count([nv[3,2],nv[3,3],nv[3,4],nv[3,5],nv[3,6],nv[3,7]],0) >= 1
- Jonathan can work at most 5 days in a row - count([nv[3,3],nv[3,4],nv[3,5],nv[3,6],nv[3,7],nv[3,8]],0) >= 1
- Jonathan can work at most 5 days in a row - count([nv[3,4],nv[3,5],nv[3,6],nv[3,7],nv[3,8],nv[3,9]],0) >= 1
- Jonathan can work at most 5 days in a row - count([nv[3,5],nv[3,6],nv[3,7],nv[3,8],nv[3,9],nv[3,10]],0) >= 1
- Jonathan can work at most 5 days in a row - count([nv[3,6],nv[3,7],nv[3,8],nv[3,9],nv[3,10],nv[3,11]],0) >= 1
- Jonathan can work at most 5 days in a row - count([nv[3,7],nv[3,8],nv[3,9],nv[3,10],nv[3,11],nv[3,12]],0) >= 1
- Jonathan can work at most 5 days in a row - count([nv[3,8],nv[3,9],nv[3,10],nv[3,11],nv[3,12],nv[3,13]],0) >= 1
- William can work at most 5 days in a row - count([nv[4,0],nv[4,1],nv[4,2],nv[4,3],nv[4,4],nv[4,5]],0) >= 1
- William can work at most 5 days in a row - count([nv[4,1],nv[4,2],nv[4,3],nv[4,4],nv[4,5],nv[4,6]],0) >= 1
- William can work at most 5 days in a row - count([nv[4,2],nv[4,3],nv[4,4],nv[4,5],nv[4,6],nv[4,7]],0) >= 1
- William can work at most 5 days in a row - count([nv[4,3],nv[4,4],nv[4,5],nv[4,6],nv[4,7],nv[4,8]],0) >= 1
- William can work at most 5 days in a row - count([nv[4,4],nv[4,5],nv[4,6],nv[4,7],nv[4,8],nv[4,9]],0) >= 1
- William can work at most 5 days in a row - count([nv[4,5],nv[4,6],nv[4,7],nv[4,8],nv[4,9],nv[4,10]],0) >= 1
- William can work at most 5 days in a row - count([nv[4,6],nv[4,7],nv[4,8],nv[4,9],nv[4,10],nv[4,11]],0) >= 1
- William can work at most 5 days in a row - count([nv[4,7],nv[4,8],nv[4,9],nv[4,10],nv[4,11],nv[4,12]],0) >= 1
- William can work at most 5 days in a row - count([nv[4,8],nv[4,9],nv[4,10],nv[4,11],nv[4,12],nv[4,13]],0) >= 1
- Richard can work at most 5 days in a row - count([nv[5,0],nv[5,1],nv[5,2],nv[5,3],nv[5,4],nv[5,5]],0) >= 1
- Richard can work at most 5 days in a row - count([nv[5,1],nv[5,2],nv[5,3],nv[5,4],nv[5,5],nv[5,6]],0) >= 1
- Richard can work at most 5 days in a row - count([nv[5,2],nv[5,3],nv[5,4],nv[5,5],nv[5,6],nv[5,7]],0) >= 1
- Richard can work at most 5 days in a row - count([nv[5,3],nv[5,4],nv[5,5],nv[5,6],nv[5,7],nv[5,8]],0) >= 1
- Richard can work at most 5 days in a row - count([nv[5,4],nv[5,5],nv[5,6],nv[5,7],nv[5,8],nv[5,9]],0) >= 1
- Richard can work at most 5 days in a row - count([nv[5,5],nv[5,6],nv[5,7],nv[5,8],nv[5,9],nv[5,10]],0) >= 1
- Richard can work at most 5 days in a row - count([nv[5,6],nv[5,7],nv[5,8],nv[5,9],nv[5,10],nv[5,11]],0) >= 1
- Richard can work at most 5 days in a row - count([nv[5,7],nv[5,8],nv[5,9],nv[5,10],nv[5,11],nv[5,12]],0) >= 1
- Richard can work at most 5 days in a row - count([nv[5,8],nv[5,9],nv[5,10],nv[5,11],nv[5,12],nv[5,13]],0) >= 1
- Kristen can work at most 5 days in a row - count([nv[6,0],nv[6,1],nv[6,2],nv[6,3],nv[6,4],nv[6,5]],0) >= 1
- Kristen can work at most 5 days in a row - count([nv[6,1],nv[6,2],nv[6,3],nv[6,4],nv[6,5],nv[6,6]],0) >= 1
- Kristen can work at most 5 days in a row - count([nv[6,2],nv[6,3],nv[6,4],nv[6,5],nv[6,6],nv[6,7]],0) >= 1
- Kristen can work at most 5 days in a row - count([nv[6,3],nv[6,4],nv[6,5],nv[6,6],nv[6,7],nv[6,8]],0) >= 1
- Kristen can work at most 5 days in a row - count([nv[6,4],nv[6,5],nv[6,6],nv[6,7],nv[6,8],nv[6,9]],0) >= 1
- Kristen can work at most 5 days in a row - count([nv[6,5],nv[6,6],nv[6,7],nv[6,8],nv[6,9],nv[6,10]],0) >= 1
- Kristen can work at most 5 days in a row - count([nv[6,6],nv[6,7],nv[6,8],nv[6,9],nv[6,10],nv[6,11]],0) >= 1
- Kristen can work at most 5 days in a row - count([nv[6,7],nv[6,8],nv[6,9],nv[6,10],nv[6,11],nv[6,12]],0) >= 1
- Kristen can work at most 5 days in a row - count([nv[6,8],nv[6,9],nv[6,10],nv[6,11],nv[6,12],nv[6,13]],0) >= 1
- Kevin can work at most 5 days in a row - count([nv[7,0],nv[7,1],nv[7,2],nv[7,3],nv[7,4],nv[7,5]],0) >= 1
- Kevin can work at most 5 days in a row - count([nv[7,1],nv[7,2],nv[7,3],nv[7,4],nv[7,5],nv[7,6]],0) >= 1
- Kevin can work at most 5 days in a row - count([nv[7,2],nv[7,3],nv[7,4],nv[7,5],nv[7,6],nv[7,7]],0) >= 1
- Kevin can work at most 5 days in a row - count([nv[7,3],nv[7,4],nv[7,5],nv[7,6],nv[7,7],nv[7,8]],0) >= 1
- Kevin can work at most 5 days in a row - count([nv[7,4],nv[7,5],nv[7,6],nv[7,7],nv[7,8],nv[7,9]],0) >= 1
- Kevin can work at most 5 days in a row - count([nv[7,5],nv[7,6],nv[7,7],nv[7,8],nv[7,9],nv[7,10]],0) >= 1
- Kevin can work at most 5 days in a row - count([nv[7,6],nv[7,7],nv[7,8],nv[7,9],nv[7,10],nv[7,11]],0) >= 1
- Kevin can work at most 5 days in a row - count([nv[7,7],nv[7,8],nv[7,9],nv[7,10],nv[7,11],nv[7,12]],0) >= 1
- Kevin can work at most 5 days in a row - count([nv[7,8],nv[7,9],nv[7,10],nv[7,11],nv[7,12],nv[7,13]],0) >= 1

Object-oriented Nurse Rostering CPMpy model factory

factory = NurseSchedulingFactory(data)
model, nurse_view = factory.get_full_model()  # CPMpy model with all constraints
model.solve(solver="ortools")

True

nurse_view.value()

array([[0, 1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 1],
       [1, 1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0],
       [1, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 1, 0, 0],
       [1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0],
       [0, 1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 1],
       [1, 1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1],
       [0, 0, 1, 1, 1, 0, 0, 1, 1, 1, 0, 0, 1, 1],
       [1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 0]])

Nurse rostering in CPMpy: visualisation, with pandas

def visualize(sol, factory):
    weeks = [f"Week {i + 1}" for i in range(factory.data.horizon // 7)]
    weekdays = ["Mon", "Tue", "Wed", "Thu", "Fri", "Sat", "Sun"]
    nurses = factory.data.staff['name'].tolist()

    df = pd.DataFrame(sol,
                      columns=pd.MultiIndex.from_product((weeks, weekdays)),
                      index=factory.data.staff.name)
    mapping = factory.idx_to_name
    df = df.map(lambda v: mapping[v] if v is not None and v < len(mapping) else '')  # convert to shift names

    for shift_type in factory.shift_name_to_idx:
        if shift_type == "F":continue
        sums = (df == shift_type).sum()  # cover for each shift type
        req = factory.data.cover["Requirement"][factory.data.cover["ShiftID"] == shift_type]
        req.index = sums.index
        df.loc[f'Cover {shift_type}'] = sums.astype(str) + "/" + req.astype(str)
    df["Total shifts"] = (df != "F").sum(axis=1)  # shifts done by nurse
    subset = (df.index.tolist()[:-len(factory.data.shifts)], df.columns[:-1])
    style = df.style.set_table_styles([{'selector': '.data', 'props': [('text-align', 'center')]},
                                       {'selector': '.col_heading', 'props': [('text-align', 'center')]},
                                       {'selector': '.col7', 'props': [('border-left',"2px solid black")]}])
    style = style.map(lambda v: 'border: 1px solid black', subset=subset)
    style = style.map(color_shift, factory=factory, subset=subset)  # color cells
    return style

from visualize import *

Nurse rostering in CPMpy: visualisation, with pandas

visualize(nurse_view.value(), factory)

	Week 1							Week 2							Total shifts
	Mon	Tue	Wed	Thu	Fri	Sat	Sun	Mon	Tue	Wed	Thu	Fri	Sat	Sun
name
Megan	F	D	D	D	D	F	F	D	D	F	F	D	D	D	9
Katherine	D	D	D	D	D	F	F	D	D	F	F	D	D	F	9
Robert	D	D	D	F	F	D	D	F	F	D	D	D	F	F	8
Jonathan	D	D	F	F	F	D	D	D	D	D	F	F	F	F	7
William	F	D	D	D	D	F	F	D	D	F	F	D	D	D	9
Richard	D	D	D	D	D	F	F	D	D	F	F	F	D	D	9
Kristen	F	F	D	D	D	F	F	D	D	D	F	F	D	D	8
Kevin	D	D	F	F	F	F	F	F	D	D	D	D	D	F	7
Cover D	5/5	7/7	6/6	5/4	5/5	2/5	2/5	6/6	7/7	4/4	2/2	5/5	6/6	4/4	14

Hands-on Explainable Constraint Programming (XCP)

• The model: Nurse Rostering
• The system: CPMpy modeling library
• Explain UNSAT:
  • Causal explanations (MUS, OUS, sequence)
  • Conversational explanations
• Explain a solution:
  • Causal explanations
  • Contrastive explanations

Minimal Unsatisfiable Subsets (MUS)

• Model nurse rostering problem as decision problem
  (no objective)

• Nurse preferences are also hard constraints

# model as decision model
factory = NurseSchedulingFactory(data)
model, nurse_view = factory.get_decision_model()  # CMPpy DECISION Model
model.solve()

False

... no solution found

constraints = toplevel_list(model.constraints, merge_and=False) # normalization for later
print(f"Model has {len(constraints)} constraints:")
for cons in constraints: print("-", cons)

Model has 168 constraints:
- Megan cannot work more than 14 shifts of type 1
- Katherine cannot work more than 14 shifts of type 1
- Robert cannot work more than 14 shifts of type 1
- Jonathan cannot work more than 14 shifts of type 1
- William cannot work more than 14 shifts of type 1
- Richard cannot work more than 14 shifts of type 1
- Kristen cannot work more than 14 shifts of type 1
- Kevin cannot work more than 14 shifts of type 1
- Megan cannot work more than 4320min
- Katherine cannot work more than 4320min
- Robert cannot work more than 4320min
- Jonathan cannot work more than 4320min
- William cannot work more than 4320min
- Richard cannot work more than 4320min
- Kristen cannot work more than 4320min
- Kevin cannot work more than 4320min
- Megan cannot work more than 3360min
- Katherine cannot work more than 3360min
- Robert cannot work more than 3360min
- Jonathan cannot work more than 3360min
- William cannot work more than 3360min
- Richard cannot work more than 3360min
- Kristen cannot work more than 3360min
- Kevin cannot work more than 3360min
- Megan can work at most 5 days before having a day off
- Megan can work at most 5 days before having a day off
- Megan can work at most 5 days before having a day off
- Megan can work at most 5 days before having a day off
- Megan can work at most 5 days before having a day off
- Megan can work at most 5 days before having a day off
- Megan can work at most 5 days before having a day off
- Megan can work at most 5 days before having a day off
- Megan can work at most 5 days before having a day off
- Katherine can work at most 5 days before having a day off
- Katherine can work at most 5 days before having a day off
- Katherine can work at most 5 days before having a day off
- Katherine can work at most 5 days before having a day off
- Katherine can work at most 5 days before having a day off
- Katherine can work at most 5 days before having a day off
- Katherine can work at most 5 days before having a day off
- Katherine can work at most 5 days before having a day off
- Katherine can work at most 5 days before having a day off
- Robert can work at most 5 days before having a day off
- Robert can work at most 5 days before having a day off
- Robert can work at most 5 days before having a day off
- Robert can work at most 5 days before having a day off
- Robert can work at most 5 days before having a day off
- Robert can work at most 5 days before having a day off
- Robert can work at most 5 days before having a day off
- Robert can work at most 5 days before having a day off
- Robert can work at most 5 days before having a day off
- Jonathan can work at most 5 days before having a day off
- Jonathan can work at most 5 days before having a day off
- Jonathan can work at most 5 days before having a day off
- Jonathan can work at most 5 days before having a day off
- Jonathan can work at most 5 days before having a day off
- Jonathan can work at most 5 days before having a day off
- Jonathan can work at most 5 days before having a day off
- Jonathan can work at most 5 days before having a day off
- Jonathan can work at most 5 days before having a day off
- William can work at most 5 days before having a day off
- William can work at most 5 days before having a day off
- William can work at most 5 days before having a day off
- William can work at most 5 days before having a day off
- William can work at most 5 days before having a day off
- William can work at most 5 days before having a day off
- William can work at most 5 days before having a day off
- William can work at most 5 days before having a day off
- William can work at most 5 days before having a day off
- Richard can work at most 5 days before having a day off
- Richard can work at most 5 days before having a day off
- Richard can work at most 5 days before having a day off
- Richard can work at most 5 days before having a day off
- Richard can work at most 5 days before having a day off
- Richard can work at most 5 days before having a day off
- Richard can work at most 5 days before having a day off
- Richard can work at most 5 days before having a day off
- Richard can work at most 5 days before having a day off
- Kristen can work at most 5 days before having a day off
- Kristen can work at most 5 days before having a day off
- Kristen can work at most 5 days before having a day off
- Kristen can work at most 5 days before having a day off
- Kristen can work at most 5 days before having a day off
- Kristen can work at most 5 days before having a day off
- Kristen can work at most 5 days before having a day off
- Kristen can work at most 5 days before having a day off
- Kristen can work at most 5 days before having a day off
- Kevin can work at most 5 days before having a day off
- Kevin can work at most 5 days before having a day off
- Kevin can work at most 5 days before having a day off
- Kevin can work at most 5 days before having a day off
- Kevin can work at most 5 days before having a day off
- Kevin can work at most 5 days before having a day off
- Kevin can work at most 5 days before having a day off
- Kevin can work at most 5 days before having a day off
- Kevin can work at most 5 days before having a day off
- Megan should work at least 2 days before having a day off
- Katherine should work at least 2 days before having a day off
- Robert should work at least 2 days before having a day off
- Jonathan should work at least 2 days before having a day off
- William should work at least 2 days before having a day off
- Richard should work at least 2 days before having a day off
- Kristen should work at least 2 days before having a day off
- Kevin should work at least 2 days before having a day off
- Megan should work at most 1 weekends
- Katherine should work at most 1 weekends
- Robert should work at most 1 weekends
- Jonathan should work at most 1 weekends
- William should work at most 1 weekends
- Richard should work at most 1 weekends
- Kristen should work at most 1 weekends
- Kevin should work at most 1 weekends
- Megan has a day off on Mon 1
- Katherine has a day off on Sat 1
- Robert has a day off on Tue 2
- Jonathan has a day off on Wed 1
- William has a day off on Wed 2
- Richard has a day off on Sat 1
- Kristen has a day off on Tue 1
- Kevin has a day off on Mon 2
- Megan should have at least 2 consecutive days off
- Katherine should have at least 2 consecutive days off
- Robert should have at least 2 consecutive days off
- Jonathan should have at least 2 consecutive days off
- William should have at least 2 consecutive days off
- Richard should have at least 2 consecutive days off
- Kristen should have at least 2 consecutive days off
- Kevin should have at least 2 consecutive days off
- Megan requests to work shift D on Wed 1
- Megan requests to work shift D on Thu 1
- Katherine requests to work shift D on Mon 1
- Katherine requests to work shift D on Tue 1
- Katherine requests to work shift D on Wed 1
- Katherine requests to work shift D on Thu 1
- Katherine requests to work shift D on Fri 1
- Robert requests to work shift D on Mon 1
- Robert requests to work shift D on Tue 1
- Robert requests to work shift D on Wed 1
- Robert requests to work shift D on Thu 1
- Robert requests to work shift D on Fri 1
- Jonathan requests to work shift D on Tue 2
- Jonathan requests to work shift D on Wed 2
- Richard requests to work shift D on Mon 1
- Richard requests to work shift D on Tue 1
- Kevin requests to work shift D on Wed 2
- Kevin requests to work shift D on Thu 2
- Kevin requests to work shift D on Fri 2
- Kevin requests to work shift D on Sat 2
- Kevin requests to work shift D on Sun 2
- Robert requests to not work shift D on Sat 2
- Robert requests to not work shift D on Sun 2
- Richard requests to not work shift D on Tue 2
- Kevin requests to not work shift D on Wed 1
- Kevin requests to not work shift D on Thu 1
- Shift D on Mon 1 must be covered by 5 nurses out of 8
- Shift D on Tue 1 must be covered by 7 nurses out of 8
- Shift D on Wed 1 must be covered by 6 nurses out of 8
- Shift D on Thu 1 must be covered by 4 nurses out of 8
- Shift D on Fri 1 must be covered by 5 nurses out of 8
- Shift D on Sat 1 must be covered by 5 nurses out of 8
- Shift D on Sun 1 must be covered by 5 nurses out of 8
- Shift D on Mon 2 must be covered by 6 nurses out of 8
- Shift D on Tue 2 must be covered by 7 nurses out of 8
- Shift D on Wed 2 must be covered by 4 nurses out of 8
- Shift D on Thu 2 must be covered by 2 nurses out of 8
- Shift D on Fri 2 must be covered by 5 nurses out of 8
- Shift D on Sat 2 must be covered by 6 nurses out of 8
- Shift D on Sun 2 must be covered by 4 nurses out of 8

Trim model to minimal set of constraints

... minimize cognitive burden for user

How to compute a MUS?

Deletion-based MUS algorithm

[Joao Marques-Silva. Minimal Unsatisfiability: Models, Algorithms and Applications. ISMVL 2010. pp. 9-14]

def mus_naive(constraints):
    m = cp.Model(constraints)
    assert m.solve() is False, "Model should be UNSAT"
    
    core = constraints
    i = 0
    while i < len(core):
        subcore = core[:i] + core[i+1:]
        if cp.Model(subcore).solve():
            i += 1 # removing makes it SAT, need to keep
        else:
            core = subcore # can safely delete 
    return core

How to compute a MUS?

CPMpy implements an incremental version of this, using assumption variables

• cpmpy.tools.mus

from cpmpy.tools.mus import mus

solver = "ortools"
subset = mus(model.constraints, solver=solver) 

print("Length of MUS:", len(subset))
for cons in subset: print("-", cons)

Length of MUS: 11
- Kevin requests to work shift D on Sun 2
- Robert requests to work shift D on Fri 1
- Robert requests to work shift D on Thu 1
- Robert requests to work shift D on Wed 1
- Robert requests to work shift D on Tue 1
- Robert requests to work shift D on Mon 1
- Richard has a day off on Sat 1
- Katherine has a day off on Sat 1
- Kevin should work at most 1 weekends
- Robert can work at most 5 days before having a day off
- Shift D on Sat 1 must be covered by 5 nurses out of 8

visualize_constraints(subset, nurse_view, factory)

	Week 1							Week 2							Total shifts
	Mon	Tue	Wed	Thu	Fri	Sat	Sun	Mon	Tue	Wed	Thu	Fri	Sat	Sun
name
Megan															14
Katherine															14
Robert															14
Jonathan															14
William															14
Richard															14
Kristen															14
Kevin															14
Cover D	0/5	0/7	0/6	0/4	0/5	0/5	0/5	0/6	0/7	0/4	0/2	0/5	0/6	0/4	14

Many MUS'es may exist...

Liffiton, M.H., & Malik, A. (2013). Enumerating infeasibility: Finding multiple MUSes quickly. In Proceedings of the 10th International Conference on Integration of AI and OR Techniques in Constraint Programming (CPAIOR 2013) (pp. 160–175)

# MARCO MUS/MSS enumeration
from explanations.marco_mcs_mus import do_marco
solver = "ortools"  # default solver
if "exact" in cp.SolverLookup.solvernames(): solver = "exact"  # fast for increment solving
    
t0 = time.time()
cnt = 0
for (kind, sset) in do_marco(model, solver=solver):
    if kind == "MUS":
        print("M", end="")
        cnt += 1
    else: print(".", end="") # MSS
    
    if time.time() - t0 > 20:  break  # for tutorial: break after 20s
print(f"\nFound {cnt} MUSes in", time.time() - t0)

MMM.....M.
Found 4 MUSes in 20.594057083129883

Many MUS'es may exist...

This problem has just 168 constraints, yet 100.000+ MUSes exist...

Which one to show?

In explanations less is more, so lets find the smallest one directly!

Correction subsets and MUS'es

Hitting set duality

Given all correction subsets, smallest minimal unsatisfiable subset
= smallest hitting set to MCS'es

Enumerating all correction subsets is also expensive...

Compute the smallest incrementally!

How to calculate a Smallest MUS (sMUS)?

1. Initialize sets-to-hit $\mathcal{H}$ (e.g. insert set of all constraints)
2. Find smallest hitting set $S$ and check if SAT
3. If SAT: take complement of $S$ and add this correction subset $K$ to sets-to-hit $\mathcal{H}$ Optionally: shrink $K$ to smaller correction subset
4. Repeat until $S$ is UNSAT: smallest unsatisfiable subset found

from explanations.subset import smus

small_subset = smus(model.constraints, solver="ortools", hs_solver="gurobi")

print("Length of sMUS:", len(small_subset))
for cons in small_subset:  
    print("-", cons)

Length of sMUS: 3
- Robert has a day off on Tue 2
- Richard requests to not work shift D on Tue 2
- Shift D on Tue 2 must be covered by 7 nurses out of 8

visualize_constraints(small_subset, nurse_view, factory)

	Week 1							Week 2							Total shifts
	Mon	Tue	Wed	Thu	Fri	Sat	Sun	Mon	Tue	Wed	Thu	Fri	Sat	Sun
name
Megan															14
Katherine															14
Robert															14
Jonathan															14
William															14
Richard															14
Kristen															14
Kevin															14
Cover D	0/5	0/7	0/6	0/4	0/5	0/5	0/5	0/6	0/7	0/4	0/2	0/5	0/6	0/4	14

Step-wise explanation

• We were lucky, the SMUS is pretty understandable
• What if its not?
• Disect MUS into smaller steps
  -> Step-wise Explanations

Ignace Bleukx, Jo Devriendt, Emilio Gamba, Bart Bogaerts, Tias Guns. Simplifying Step-wise Explanation Sequences. 29th International Conference on Principles and Practice of Constraint Programming (CP23), 2023.

Any MUS

subset = mus(model.constraints)

visualize_constraints(subset, nurse_view, factory)

	Week 1							Week 2							Total shifts
	Mon	Tue	Wed	Thu	Fri	Sat	Sun	Mon	Tue	Wed	Thu	Fri	Sat	Sun
name
Megan															14
Katherine															14
Robert															14
Jonathan															14
William															14
Richard															14
Kristen															14
Kevin															14
Cover D	0/5	0/7	0/6	0/4	0/5	0/5	0/5	0/6	0/7	0/4	0/2	0/5	0/6	0/4	14

Let's find a sequence of step-wise explanations of this MUS

from explanations.stepwise import find_sequence

seq = find_sequence(subset)

Found sequence of length 11
Filtered sequence to length 11

nurse_view.clear()
visualize_step(seq[0], nurse_view, factory)

Propagating constraint: Robert requests to work shift D on Fri 1

	Week 1							Week 2							Total shifts
	Mon	Tue	Wed	Thu	Fri	Sat	Sun	Mon	Tue	Wed	Thu	Fri	Sat	Sun
name
Megan															14
Katherine															14
Robert					D										14
Jonathan															14
William															14
Richard															14
Kristen															14
Kevin															14
Cover D	0/5	0/7	0/6	0/4	1/5	0/5	0/5	0/6	0/7	0/4	0/2	0/5	0/6	0/4	14

visualize_step(seq[1], nurse_view, factory)

Propagating constraint: Robert requests to work shift D on Wed 1

	Week 1							Week 2							Total shifts
	Mon	Tue	Wed	Thu	Fri	Sat	Sun	Mon	Tue	Wed	Thu	Fri	Sat	Sun
name
Megan															14
Katherine															14
Robert			D		D										14
Jonathan															14
William															14
Richard															14
Kristen															14
Kevin															14
Cover D	0/5	0/7	1/6	0/4	1/5	0/5	0/5	0/6	0/7	0/4	0/2	0/5	0/6	0/4	14

visualize_step(seq[2], nurse_view, factory)

Propagating constraint: Robert requests to work shift D on Tue 1

	Week 1							Week 2							Total shifts
	Mon	Tue	Wed	Thu	Fri	Sat	Sun	Mon	Tue	Wed	Thu	Fri	Sat	Sun
name
Megan															14
Katherine															14
Robert		D	D		D										14
Jonathan															14
William															14
Richard															14
Kristen															14
Kevin															14
Cover D	0/5	1/7	1/6	0/4	1/5	0/5	0/5	0/6	0/7	0/4	0/2	0/5	0/6	0/4	14

visualize_step(seq[3], nurse_view, factory)

Propagating constraint: Katherine has a day off on Sat 1

	Week 1							Week 2							Total shifts
	Mon	Tue	Wed	Thu	Fri	Sat	Sun	Mon	Tue	Wed	Thu	Fri	Sat	Sun
name
Megan															14
Katherine						F									13
Robert		D	D		D										14
Jonathan															14
William															14
Richard															14
Kristen															14
Kevin															14
Cover D	0/5	1/7	1/6	0/4	1/5	0/5	0/5	0/6	0/7	0/4	0/2	0/5	0/6	0/4	14

visualize_step(seq[4], nurse_view, factory)

Propagating constraint: Kevin requests to work shift D on Sun 2

	Week 1							Week 2							Total shifts
	Mon	Tue	Wed	Thu	Fri	Sat	Sun	Mon	Tue	Wed	Thu	Fri	Sat	Sun
name
Megan															14
Katherine						F									13
Robert		D	D		D										14
Jonathan															14
William															14
Richard															14
Kristen															14
Kevin														D	14
Cover D	0/5	1/7	1/6	0/4	1/5	0/5	0/5	0/6	0/7	0/4	0/2	0/5	0/6	1/4	14

visualize_step(seq[5], nurse_view, factory)

Propagating constraint: Robert requests to work shift D on Mon 1

	Week 1							Week 2							Total shifts
	Mon	Tue	Wed	Thu	Fri	Sat	Sun	Mon	Tue	Wed	Thu	Fri	Sat	Sun
name
Megan															14
Katherine						F									13
Robert	D	D	D		D										14
Jonathan															14
William															14
Richard															14
Kristen															14
Kevin														D	14
Cover D	1/5	1/7	1/6	0/4	1/5	0/5	0/5	0/6	0/7	0/4	0/2	0/5	0/6	1/4	14

visualize_step(seq[6], nurse_view, factory)

Propagating constraint: Kevin should work at most 1 weekends

	Week 1							Week 2							Total shifts
	Mon	Tue	Wed	Thu	Fri	Sat	Sun	Mon	Tue	Wed	Thu	Fri	Sat	Sun
name
Megan															14
Katherine						F									13
Robert	D	D	D		D										14
Jonathan															14
William															14
Richard															14
Kristen															14
Kevin						F								D	13
Cover D	1/5	1/7	1/6	0/4	1/5	0/5	0/5	0/6	0/7	0/4	0/2	0/5	0/6	1/4	14

visualize_step(seq[7], nurse_view, factory)

Propagating constraint: Richard has a day off on Sat 1

	Week 1							Week 2							Total shifts
	Mon	Tue	Wed	Thu	Fri	Sat	Sun	Mon	Tue	Wed	Thu	Fri	Sat	Sun
name
Megan															14
Katherine						F									13
Robert	D	D	D		D										14
Jonathan															14
William															14
Richard						F									13
Kristen															14
Kevin						F								D	13
Cover D	1/5	1/7	1/6	0/4	1/5	0/5	0/5	0/6	0/7	0/4	0/2	0/5	0/6	1/4	14

visualize_step(seq[8], nurse_view, factory)

Propagating constraint: Robert requests to work shift D on Thu 1

	Week 1							Week 2							Total shifts
	Mon	Tue	Wed	Thu	Fri	Sat	Sun	Mon	Tue	Wed	Thu	Fri	Sat	Sun
name
Megan															14
Katherine						F									13
Robert	D	D	D	D	D										14
Jonathan															14
William															14
Richard						F									13
Kristen															14
Kevin						F								D	13
Cover D	1/5	1/7	1/6	1/4	1/5	0/5	0/5	0/6	0/7	0/4	0/2	0/5	0/6	1/4	14

visualize_step(seq[9], nurse_view, factory)

Propagating constraint: Robert can work at most 5 days before having a day off

	Week 1							Week 2							Total shifts
	Mon	Tue	Wed	Thu	Fri	Sat	Sun	Mon	Tue	Wed	Thu	Fri	Sat	Sun
name
Megan															14
Katherine						F									13
Robert	D	D	D	D	D	F									13
Jonathan															14
William															14
Richard						F									13
Kristen															14
Kevin						F								D	13
Cover D	1/5	1/7	1/6	1/4	1/5	0/5	0/5	0/6	0/7	0/4	0/2	0/5	0/6	1/4	14

visualize_step(seq[10], nurse_view, factory)

Propagating constraint: Shift D on Sat 1 must be covered by 5 nurses out of 8

	Week 1							Week 2							Total shifts
	Mon	Tue	Wed	Thu	Fri	Sat	Sun	Mon	Tue	Wed	Thu	Fri	Sat	Sun
name
Megan															14
Katherine						F									13
Robert	D	D	D	D	D	F									13
Jonathan															14
William															14
Richard						F									13
Kristen															14
Kevin						F								D	13
Cover D	1/5	1/7	1/6	1/4	1/5	0/5	0/5	0/6	0/7	0/4	0/2	0/5	0/6	1/4	14

Prefered MUS

Some users may be looking for a specific conflict, such as ones avoiding changes in vacation days for nurses

Using QuickXplain, we can find such prefered MUS

Junker, Ulrich. "Preferred explanations and relaxations for over-constrained problems." AAAI-2004. 2004.

def define_order(cons):
    if "day off" in str(cons):
        return 100 # we do not want to mess with vacation days
    return 10 # else

constraints = toplevel_list(model.constraints, merge_and=False)
constraints = sorted(constraints, key=define_order)

# find core with quickXplain
from cpmpy.tools.mus import quickxplain

prefered_subset = quickxplain(constraints, solver="ortools")
for cons in prefered_subset: print("-",cons)

- Megan should work at most 1 weekends
- Katherine should work at most 1 weekends
- Robert should work at most 1 weekends
- Jonathan should work at most 1 weekends
- William should work at most 1 weekends
- Richard should work at most 1 weekends
- Shift D on Sat 1 must be covered by 5 nurses out of 8
- Shift D on Sat 2 must be covered by 6 nurses out of 8

visualize_constraints(prefered_subset, nurse_view, factory)

	Week 1							Week 2							Total shifts
	Mon	Tue	Wed	Thu	Fri	Sat	Sun	Mon	Tue	Wed	Thu	Fri	Sat	Sun
name
Megan															14
Katherine															14
Robert															14
Jonathan															14
William															14
Richard															14
Kristen															14
Kevin															14
Cover D	0/5	0/7	0/6	0/4	0/5	0/5	0/5	0/6	0/7	0/4	0/2	0/5	0/6	0/4	14

Hands-on Explainable Constraint Programming (XCP)

• The model: Nurse Rostering
• The system: CPMpy modeling library
• Explain UNSAT:
  • Causal explanations (MUS, OUS, sequence)
  • Conversational explanations
• Explain a solution:
  • Causal explanations
  • Contrastive explanations

Fixing UNSAT Models

How to change the model, in order to find a solution?

First idea:

find subset of soft constraints to keep
=
find constraints to be removed, e.g. remove a correction subset!

How to compute a Minimal Correction Subset of an UNSAT problem?

Approach 1: grow-based MCS/MSS

Iterate over constraints and partition

def mcs_naive(constraints):
    mss = []  # grow a satisfiable subset one-by-one
    mcs = []  # everything else is in the minimum conflict set
    
    for cons in constraints:
        if cp.Model(mss + [cons]).solve():
            mss.append(cons)  # adding it remains SAT
        else:
            mcs.append(cons)  # UNSAT, causes conflict
    
    return mcs

from explanations.subset import mcs  # using assumption variables

corr_subset = mcs(model.constraints)

print("By removing these constraints, the model becomes SAT:")
for cons in corr_subset: print("-",cons)
    
visualize_constraints(corr_subset, nurse_view, factory)

By removing these constraints, the model becomes SAT:
- Shift D on Sun 1 must be covered by 5 nurses out of 8
- Shift D on Sat 1 must be covered by 5 nurses out of 8
- Shift D on Mon 2 must be covered by 6 nurses out of 8
- Shift D on Thu 2 must be covered by 2 nurses out of 8
- Shift D on Tue 2 must be covered by 7 nurses out of 8

	Week 1							Week 2							Total shifts
	Mon	Tue	Wed	Thu	Fri	Sat	Sun	Mon	Tue	Wed	Thu	Fri	Sat	Sun
name
Megan															14
Katherine															14
Robert															14
Jonathan															14
William															14
Richard															14
Kristen															14
Kevin															14
Cover D	0/5	0/7	0/6	0/4	0/5	0/5	0/5	0/6	0/7	0/4	0/2	0/5	0/6	0/4	14

mss = set(toplevel_list(model.constraints, merge_and=False)) - set(corr_subset)
        
corrected_model = cp.Model(list(mss))
assert corrected_model.solve()

visualize(nurse_view.value(), factory)

	Week 1							Week 2							Total shifts
	Mon	Tue	Wed	Thu	Fri	Sat	Sun	Mon	Tue	Wed	Thu	Fri	Sat	Sun
name
Megan	F	D	D	D	D	F	F	D	D	F	F	F	D	D	8
Katherine	D	D	D	D	D	F	F	F	F	F	F	D	D	F	7
Robert	D	D	D	D	D	F	F	F	F	D	D	F	F	F	7
Jonathan	D	D	F	F	D	D	F	F	D	D	D	F	F	F	7
William	F	D	D	F	F	F	F	D	D	F	F	D	D	D	7
Richard	D	D	D	F	F	F	F	F	F	D	D	D	D	F	7
Kristen	F	F	D	D	D	F	F	F	F	F	D	D	D	D	7
Kevin	D	D	F	F	F	F	F	F	F	D	D	D	D	D	7
Cover D	5/5	7/7	6/6	4/4	5/5	1/5	0/5	2/6	3/7	4/4	5/2	5/5	6/6	4/4	14

How to compute a Minimal Correction Subset of an UNSAT problem?

Approach 2: Max-CSP

MAX-CSP problem, maximize number of satisfied constraints

Maximize sum of truth-value of consrtaints

=> Finds largest MSS = complement of cardinality-minimal MCS!

def partition_csp(constraints):
    
    ind = cp.boolvar(shape=len(constraints))  # Boolean indicator variable for each constraint
    
    maxsat_model = cp.Model(ind.implies(constraints))  # add reified constraints
    maxsat_model.maximize(cp.sum(ind))  # find largest MSS = smallest MCS
    
    assert maxsat_model.solve()
    
    mss = [c for a,c in zip(ind, constraints) if a.value() is True]
    mcs = [c for a,c in zip(ind, constraints) if a.value() is False]
    
    return mss, mcs

mss, mcs = partition_csp(constraints)

print("By removing these constraints, the model becomes SAT:")
for cons in mcs: print("-",cons)
    
visualize_constraints(mcs, nurse_view, factory)

By removing these constraints, the model becomes SAT:
- Richard requests to not work shift D on Tue 2
- Shift D on Sat 1 must be covered by 5 nurses out of 8
- Shift D on Sun 1 must be covered by 5 nurses out of 8
- Robert has a day off on Tue 2

	Week 1							Week 2							Total shifts
	Mon	Tue	Wed	Thu	Fri	Sat	Sun	Mon	Tue	Wed	Thu	Fri	Sat	Sun
name
Megan															14
Katherine															14
Robert															14
Jonathan															14
William															14
Richard															14
Kristen															14
Kevin															14
Cover D	0/5	0/7	0/6	0/4	0/5	0/5	0/5	0/6	0/7	0/4	0/2	0/5	0/6	0/4	14

What does the corrected model look like?

corrected_model = cp.Model(list(mss))
assert corrected_model.solve()

visualize(nurse_view.value(), factory)

	Week 1							Week 2							Total shifts
	Mon	Tue	Wed	Thu	Fri	Sat	Sun	Mon	Tue	Wed	Thu	Fri	Sat	Sun
name
Megan	F	D	D	D	D	F	F	D	D	F	F	D	D	F	8
Katherine	D	D	D	D	D	F	F	D	D	F	F	F	D	D	9
Robert	D	D	D	D	D	F	F	D	D	D	F	F	F	F	8
Jonathan	D	D	F	F	D	D	F	F	D	D	D	D	F	F	8
William	F	D	D	F	F	F	F	D	D	F	F	D	D	D	7
Richard	D	D	D	F	F	F	F	D	D	D	F	F	D	D	8
Kristen	F	F	D	D	D	F	F	D	D	F	F	D	D	F	7
Kevin	D	D	F	F	F	F	F	F	F	D	D	D	D	D	7
Cover D	5/5	7/7	6/6	4/4	5/5	1/5	0/5	6/6	7/7	4/4	2/2	5/5	6/6	4/4	14

Unsatisfied constraints can be interpreted as penalty of solution

=> Max-CSP solution minimizes penalty

Weighted version allows for fine grained control over penalties!

=> Optimal MSS instead of cardinality-maximal one

Fixing UNSAT Models

Removing constraints from the model is drastic...

In the previous solution, no nurses on Sunday? What if you break your leg that day?

Second idea:

Slightly violate constraints which allows for relaxation of constraints

E.g. feasbility restoration by modifying rather then removing constraints

Relaxation of constraints

• Boolean constraints can only be turned on/off
• Numerical constraints can be violated to some extend
• Introduce slack for each numerical constraint
• Slack indicates how much a constraint may be violated
  • = fine grained penalty of solution!
• Minimize aggregate of slack values

Senthooran I, Klapperstueck M, Belov G, Czauderna T, Leo K, Wallace M, Wybrow M, Garcia de la Banda M. Human-centred feasibility restoration in practice. Constraints. 2023 Jul 20:1-41.

Relaxation of constraints

E.g., allow violation of cover constraints
--> Allow shifts to be slightly under/overstaffed

slack_model, slack_nurse_view, slack_under, slack_over = factory.get_slack_model()  # CMPpy Model

for _, cover in factory.data.cover.iterrows():
    # read the data
    day = cover["# Day"]
    shift = factory.shift_name_to_idx[cover["ShiftID"]]
    requirement = cover["Requirement"]
    
    nb_nurses = cp.Count(nurse_view[:, day], shift)
    expr = nb_nurses == requirement - slack_under[day] + slack_over[day]

Minimize global violation

slack_model, slack_nurse_view, slack_under, slack_over = factory.get_slack_model()  # CMPpy Model
slack = cp.cpm_array(np.append(slack_under, slack_over))

slack_model.minimize(cp.sum(slack)) # minimize global violation

assert slack_model.solve()
style = visualize(slack_nurse_view.value(), factory, highlight_cover=True)
style.data.loc["Slack under"] = list(slack_under.value()) + [" "]
style.data.loc["Slack over"] = list(slack_over.value()) + [" "]
display(style)

	Week 1							Week 2							Total shifts
	Mon	Tue	Wed	Thu	Fri	Sat	Sun	Mon	Tue	Wed	Thu	Fri	Sat	Sun
name
Megan	F	D	D	D	D	F	F	D	D	D	F	F	D	D	9
Katherine	D	D	D	D	D	F	F	D	D	F	F	F	D	D	9
Robert	D	D	D	D	D	F	F	F	F	D	D	D	F	F	8
Jonathan	D	D	F	F	F	D	D	D	D	D	F	F	F	F	7
William	F	D	D	F	F	F	F	D	D	F	F	D	D	D	7
Richard	D	D	D	F	F	F	D	D	F	F	D	D	F	F	7
Kristen	F	F	D	D	D	F	F	D	D	F	F	D	D	F	7
Kevin	D	D	F	F	F	F	F	F	F	D	D	D	D	D	7
Cover D	5/5	7/7	6/6	4/4	4/5	1/5	2/5	6/6	5/7	4/4	3/2	5/5	5/6	4/4	14
Slack under	0	0	0	0	1	4	3	0	2	0	0	0	1	0
Slack over	0	0	0	0	0	0	0	0	0	0	1	0	0	0

Minimize maximum violation

slack_model.minimize(cp.max(slack)) # minimize max violation
 
assert slack_model.solve()
style = visualize(slack_nurse_view.value(), factory, highlight_cover=True)
style.data.loc["Slack under"] = list(slack_under.value()) + [" "]
style.data.loc["Slack over"] = list(slack_over.value()) + [" "]
display(style)

	Week 1							Week 2							Total shifts
	Mon	Tue	Wed	Thu	Fri	Sat	Sun	Mon	Tue	Wed	Thu	Fri	Sat	Sun
name
Megan	F	F	D	D	D	D	F	F	D	D	D	F	F	F	7
Katherine	D	D	D	D	D	F	F	F	D	D	F	F	D	D	9
Robert	D	D	D	D	D	F	F	F	F	D	D	F	F	F	7
Jonathan	D	D	F	F	F	F	F	D	D	D	F	F	D	D	7
William	D	D	D	F	F	D	D	D	D	F	F	F	F	F	7
Richard	D	D	D	D	F	F	D	D	F	F	D	D	F	F	8
Kristen	F	F	D	D	D	D	F	F	D	D	D	D	F	F	8
Kevin	D	D	F	F	F	F	F	F	F	D	D	D	D	D	7
Cover D	6/5	6/7	6/6	5/4	4/5	3/5	2/5	3/6	5/7	6/4	5/2	3/5	3/6	3/4	14
Slack under	0	1	0	0	1	2	3	3	2	0	0	2	3	1
Slack over	1	0	0	1	0	0	0	0	0	2	3	0	0	0

Minimize nb of violated constraints

slack_model.minimize(cp.sum(slack != 0)) # minimize nb of violated constraints
 
assert slack_model.solve()
style = visualize(slack_nurse_view.value(), factory, highlight_cover=True)
style.data.loc["Slack under"] = list(slack_under.value()) + [" "]
style.data.loc["Slack over"] = list(slack_over.value()) + [" "]
display(style)

	Week 1							Week 2							Total shifts
	Mon	Tue	Wed	Thu	Fri	Sat	Sun	Mon	Tue	Wed	Thu	Fri	Sat	Sun
name
Megan	F	D	D	D	F	F	F	D	D	F	F	D	D	D	8
Katherine	D	D	D	D	D	F	F	D	D	D	F	F	F	F	8
Robert	D	D	D	D	D	F	F	F	F	D	D	F	F	F	7
Jonathan	D	D	F	F	F	F	F	D	D	D	F	F	D	D	7
William	F	D	D	D	D	F	F	D	D	F	F	D	D	F	8
Richard	D	D	D	D	D	F	F	F	F	F	F	D	D	F	7
Kristen	F	F	D	D	D	F	F	D	D	F	F	D	D	D	8
Kevin	D	D	F	F	F	F	F	F	F	D	D	D	D	D	7
Cover D	5/5	7/7	6/6	6/4	5/5	0/5	0/5	5/6	5/7	4/4	2/2	5/5	6/6	4/4	14
Slack under	0	0	0	0	0	5	5	1	2	0	0	0	0	0
Slack over	0	0	0	2	0	0	0	0	0	0	0	0	0	0

Or minimize any combination

obj1 = cp.max(slack)       # minimize max violation
obj2 = cp.sum(slack != 0)  # minimize nb of violations
obj3 = cp.sum(slack)       # minimize global violation

slack_model.minimize(10000 * obj1 + 1000 * obj2 + obj3) # multi-objective optimization

assert slack_model.solve()
style = visualize(slack_nurse_view.value(), factory, highlight_cover=True)
style.data.loc["Slack under"] = list(slack_under.value()) + [" "]
style.data.loc["Slack over"] = list(slack_over.value()) + [" "]
display(style)

	Week 1							Week 2							Total shifts
	Mon	Tue	Wed	Thu	Fri	Sat	Sun	Mon	Tue	Wed	Thu	Fri	Sat	Sun
name
Megan	F	D	D	D	D	F	F	D	D	D	F	F	D	D	9
Katherine	D	D	D	D	D	F	F	D	D	F	F	F	D	D	9
Robert	D	D	D	D	D	F	F	F	F	D	D	D	F	F	8
Jonathan	D	D	F	F	F	D	D	D	D	D	F	F	F	F	7
William	F	D	D	F	F	D	D	D	F	F	D	D	F	F	7
Richard	D	D	D	F	F	F	D	D	F	F	D	D	F	F	7
Kristen	F	F	D	D	D	F	F	D	D	F	F	D	D	D	8
Kevin	D	D	F	F	F	F	F	F	F	D	D	D	D	D	7
Cover D	5/5	7/7	6/6	4/4	4/5	2/5	3/5	6/6	4/7	4/4	4/2	5/5	4/6	4/4	14
Slack under	0	0	0	0	1	3	2	0	3	0	0	0	2	0
Slack over	0	0	0	0	0	0	0	0	0	0	2	0	0	0

Hands-on Explainable Constraint Programming (XCP)

• The model: Nurse Rostering
• The system: CPMpy modeling library
• Explain UNSAT:
  • Causal explanations (MUS, OUS, sequence)
  • Conversational explanations
• Explain a solution:
  • Causal explanations
  • Contrastive explanations

Reformulation as Optimization problem

• Using hard constraints and soft constraints
  • Put fine grained penalty on violation of soft constraints
• Preferences modeled as soft constraints, minimize penalty of unsatisfied preferences

model, nurse_view = factory.get_full_model()
assert model.solve()
opt_sol = nurse_view.value()
display(visualize(opt_sol, factory))
print("Total penalty:", model.objective_value())
print("Time to calculate:", model.status().runtime, "s")

	Week 1							Week 2							Total shifts
	Mon	Tue	Wed	Thu	Fri	Sat	Sun	Mon	Tue	Wed	Thu	Fri	Sat	Sun
name
Megan	F	D	D	D	D	F	F	F	D	D	F	F	D	D	8
Katherine	D	D	D	D	D	F	F	D	D	F	F	D	D	F	9
Robert	D	D	D	F	F	D	D	D	F	F	D	D	F	F	8
Jonathan	D	D	F	F	F	D	D	D	D	D	F	F	F	F	7
William	F	D	D	D	D	F	F	D	D	F	F	D	D	D	9
Richard	D	D	D	F	F	F	F	D	D	D	F	F	D	D	8
Kristen	F	F	D	D	D	F	F	D	D	F	F	D	D	D	8
Kevin	D	D	F	F	D	D	F	F	D	D	D	D	F	F	8
Cover D	5/5	7/7	6/6	4/4	5/5	3/5	2/5	6/6	7/7	4/4	2/2	5/5	5/6	4/4	14

Total penalty: 607
Time to calculate: 0.182697 s

Multiple solutions

• User not satisfied with optimal solution?

• There could be multiple optimal solutions

• Find (a subset of) them by converting to a decision problem

  • Enforcing the optimal objective value

• Use solveAll()

opt_model = cp.Model(model.constraints) # init new model
opt_model += (model.objective_ == model.objective_value()) # force objective

opt_model.solveAll(solver="ortools", solution_limit=3,
                   display=lambda: display(visualize(nurse_view.value(), factory)))  # callback that visualizes sols

	Week 1							Week 2							Total shifts
	Mon	Tue	Wed	Thu	Fri	Sat	Sun	Mon	Tue	Wed	Thu	Fri	Sat	Sun
name
Megan	F	D	D	D	D	F	F	D	D	F	F	D	D	D	9
Katherine	D	D	D	D	D	F	F	F	D	D	F	F	D	D	9
Robert	D	D	D	F	F	D	D	D	F	F	D	D	F	F	8
Jonathan	D	D	F	F	F	D	D	D	D	D	F	F	F	F	7
William	F	D	D	D	D	F	F	D	D	F	F	D	D	D	9
Richard	D	D	D	F	F	F	F	D	D	D	F	F	D	D	8
Kristen	F	F	D	D	D	F	F	D	D	F	F	D	D	F	7
Kevin	D	D	F	F	D	D	D	F	F	D	D	D	F	F	8
Cover D	5/5	7/7	6/6	4/4	5/5	3/5	3/5	6/6	6/7	4/4	2/2	5/5	5/6	4/4	14

	Week 1							Week 2							Total shifts
	Mon	Tue	Wed	Thu	Fri	Sat	Sun	Mon	Tue	Wed	Thu	Fri	Sat	Sun
name
Megan	F	D	D	D	D	F	F	D	D	F	F	D	D	F	8
Katherine	D	D	D	D	D	F	F	F	D	D	F	F	D	D	9
Robert	D	D	D	F	F	D	D	D	F	F	D	D	F	F	8
Jonathan	D	D	F	F	F	D	D	D	D	D	F	F	F	F	7
William	F	D	D	D	D	F	F	D	D	F	F	D	D	D	9
Richard	D	D	D	F	F	F	F	D	D	D	F	F	D	D	8
Kristen	F	F	D	D	D	F	F	D	D	F	F	D	D	D	8
Kevin	D	D	F	F	D	D	D	F	F	D	D	D	F	F	8
Cover D	5/5	7/7	6/6	4/4	5/5	3/5	3/5	6/6	6/7	4/4	2/2	5/5	5/6	4/4	14

	Week 1							Week 2							Total shifts
	Mon	Tue	Wed	Thu	Fri	Sat	Sun	Mon	Tue	Wed	Thu	Fri	Sat	Sun
name
Megan	F	D	D	D	D	F	F	D	D	F	F	D	D	F	8
Katherine	D	D	D	D	D	F	F	F	D	D	F	F	D	D	9
Robert	D	D	D	F	F	D	D	D	F	F	D	D	F	F	8
Jonathan	D	D	F	F	F	D	D	D	D	D	F	F	F	F	7
William	F	D	D	D	D	F	F	D	D	F	F	D	D	D	9
Richard	D	D	D	F	F	F	F	D	D	D	F	F	D	D	8
Kristen	F	F	D	D	D	F	F	D	D	F	F	D	D	D	8
Kevin	D	D	F	F	D	D	F	F	D	D	D	D	F	F	8
Cover D	5/5	7/7	6/6	4/4	5/5	3/5	2/5	6/6	7/7	4/4	2/2	5/5	5/6	4/4	14

3

Causal explanation: Why is there no better solution?

• Reduce to UNSAT problem

• Add better-than optimal objective function as constraint

• Then use the step-wise explanation techniques to explain
  why it is now UNSAT

Bleukx, I., Devriendt, J., Gamba, E., Bogaerts B., & Guns T. (2023). Simplifying Step-wise Explanation Sequences. In International Conference on Principles and Practice of Constraint Programming 2023

opt_model = cp.Model(model.constraints)
opt_model += (model.objective_ < model.objective_value())

opt_model.solve()

False

Hands-on Explainable Constraint Programming (XCP)

• The model: Nurse Rostering
• The system: CPMpy modeling library
• Explain UNSAT:
  • Causal explanations (MUS, OUS, sequence)
  • Conversational explanations
• Explain a solution:
  • Causal explanations
  • Contrastive explanations

Changing the solution

• Some assignment might not be what the user wants
  or expects

• Preferences or constraints not given to the model

• Add given assignment as constraint and solve again

  • May result in less optimal objective value

• Show new (changed) solution to the user

mmodel = model.copy()
mmodel += nurse_view[2,5] == 0 # robert does not want to work on 1st saturday

assert mmodel.solve()
print("Total penalty: ", mmodel.objective_value())

Total penalty:  608

style = highlight_changes(nurse_view, opt_sol, factory)
display(style)

	Week 1							Week 2							Total shifts
	Mon	Tue	Wed	Thu	Fri	Sat	Sun	Mon	Tue	Wed	Thu	Fri	Sat	Sun
name
Megan	F	D	D	F	F	D	D	D	D	D	F	F	F	F	7
Katherine	D	D	D	D	D	F	F	D	D	F	F	F	D	D	9
Robert	D	D	D	D	D	F	F	F	F	D	D	D	D	F	9
Jonathan	D	D	F	F	F	D	D	D	D	D	F	F	F	F	7
William	F	D	D	D	D	F	F	D	D	F	F	D	D	D	9
Richard	D	D	D	F	F	F	F	D	D	F	F	D	D	D	8
Kristen	F	F	D	D	D	F	F	D	D	F	F	D	D	D	8
Kevin	D	D	F	F	D	D	F	F	D	D	D	D	F	F	8
Cover D	5/5	7/7	6/6	4/4	5/5	3/5	2/5	6/6	7/7	4/4	2/2	5/5	5/6	4/4	14

Slightly changing the solution

• Previous solution is very different from original!
  --> Do not want to change everyone's schedule!

• Change only a few parts of it?

• Tradeoff between difference and penalty

ov = mmodel.objective_value()
mmodel += cp.sum(nurse_view != opt_sol)<= 3 # allow to make 3 changes
assert mmodel.solve()
print("Total penalty:", mmodel.objective_value(), "was:", ov)

style = highlight_changes(nurse_view, opt_sol, factory)
display(style)

Total penalty: 707 was: 608

	Week 1							Week 2							Total shifts
	Mon	Tue	Wed	Thu	Fri	Sat	Sun	Mon	Tue	Wed	Thu	Fri	Sat	Sun
name
Megan	F	D	D	D	D	F	F	F	D	D	F	F	D	D	8
Katherine	D	D	D	D	D	F	F	D	D	F	F	D	D	F	9
Robert	D	D	D	D	F	F	D	D	F	F	D	D	F	F	8
Jonathan	D	D	F	F	F	D	D	D	D	D	F	F	F	F	7
William	F	D	D	D	D	F	F	D	D	F	F	D	D	D	9
Richard	D	D	D	F	F	F	F	D	D	D	F	F	D	D	8
Kristen	F	F	D	D	D	F	F	D	D	F	F	D	D	D	8
Kevin	D	D	F	F	D	D	F	F	D	D	D	D	F	F	8
Cover D	5/5	7/7	6/6	5/4	5/5	2/5	2/5	6/6	7/7	4/4	2/2	5/5	5/6	4/4	14

Counterfactual optimisation model

• "Why not Y" -> "Under what conditions would Y
  be optimal?"

• Given: model with linear objective function $w*c$,
  and a 'foil' Y (constraints to satisfy in optimal)
  

• Find: new objective function weights $w'$
  such that optimal solution satisfies $Y$

• Explains necessary changes to the model
  rather than the solution!

[Korikov, Anton, and J. Christopher Beck. "Counterfactual explanations via inverse constraint programming." In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021).]

Counterfactual optimisation model

Find currently optimal solution $X$:

model, nurse_view = factory.get_full_model()

assert model.solve()
print("Total penalty: ", model.objective_value())
visualize(nurse_view.value(), factory)

Total penalty:  607

	Week 1							Week 2							Total shifts
	Mon	Tue	Wed	Thu	Fri	Sat	Sun	Mon	Tue	Wed	Thu	Fri	Sat	Sun
name
Megan	F	D	D	D	D	F	F	D	D	D	F	F	D	D	9
Katherine	D	D	D	D	D	F	F	D	D	F	F	D	D	F	9
Robert	D	D	D	F	F	D	D	F	F	D	D	D	F	F	8
Jonathan	D	D	F	F	F	D	D	D	D	D	F	F	F	F	7
William	F	D	D	D	D	F	F	D	D	F	F	D	D	D	9
Richard	D	D	D	D	D	F	F	D	D	F	F	F	D	D	9
Kristen	F	F	D	D	D	F	F	D	D	F	F	D	D	D	8
Kevin	D	D	F	F	F	F	F	F	D	D	D	D	D	F	7
Cover D	5/5	7/7	6/6	5/4	5/5	2/5	2/5	6/6	7/7	4/4	2/2	5/5	6/6	4/4	14

Counterfactual optimisation model

Robert is unhappy!

nurse = "Robert"
 
for (w,pref) in zip(*model.objective_.args):
    if nurse in str(pref):
        print(f"{pref.value()} \t w:{w} \t{pref} \t")

False 	 w:1 	Robert's requests to work shift D on Mon 1 is denied 	
False 	 w:1 	Robert's requests to work shift D on Tue 1 is denied 	
False 	 w:1 	Robert's requests to work shift D on Wed 1 is denied 	
True 	 w:1 	Robert's requests to work shift D on Thu 1 is denied 	
True 	 w:1 	Robert's requests to work shift D on Fri 1 is denied 	
False 	 w:1 	Robert's requests to not work shift D on Sat 2 is denied 	
False 	 w:1 	Robert's requests to not work shift D on Sun 2 is denied 	

desc = "Robert's requests to work shift D on Fri 1 is denied"
weight,d_on_fri1 = next((w,pref) for w,pref in zip(*model.objective_.args) if str(pref) == desc)
print(f"{d_on_fri1.value()} \t w:{w} \t{d_on_fri1}")

True 	 w:1 	Robert's requests to work shift D on Fri 1 is denied

Counterfactual optimisation model

Robert's request to work on Fri 1 is very important!

How should he minimally change his preferences for that?

foil = {d_on_fri1 : False}  # don't want to have his request for Fri 1 denied!
print("Foil:", foil)
print("\n")

other_prefs = [(w,pref) for w,pref in zip(*model.objective_.args) if nurse in str(pref) and str(pref) != desc]
print(f"{nurse}'s other preferences:")
for w,pref in other_prefs:
    print("- Weight",w,":",pref)

Foil: {not([roster[2,4] == 1]): False}


Robert's other preferences:
- Weight 1 : Robert's requests to work shift D on Mon 1 is denied
- Weight 1 : Robert's requests to work shift D on Tue 1 is denied
- Weight 1 : Robert's requests to work shift D on Wed 1 is denied
- Weight 1 : Robert's requests to work shift D on Thu 1 is denied
- Weight 1 : Robert's requests to not work shift D on Sat 2 is denied
- Weight 1 : Robert's requests to not work shift D on Sun 2 is denied

Counterfactual optimisation model

Algorithmically, it is a beautiful inverse optimisation problem with a multi-solver main/subproblem algorithm

from explanations.counterfactual import inverse_optimize

ov = model.objective_value()
new_obj = inverse_optimize(model=model, minimize=True,
                           user_sol = foil,
                           allowed_to_change = set(p[1] for p in other_prefs))
print(f"Done! Found solution with total penalty {new_obj.value()}, was {ov}\n")

# Let's look at the preferences he should enter, to avoid Fri 1!
print(f"{nurse}'s new preferences:")
for w,pref in zip(*new_obj.args):
    if nurse in str(pref) and str(pref) != desc and w != 1:  # previous weights were 1
        print("Weight",w,":",pref)

Done! Found solution with total penalty 607, was 607

Robert's new preferences:
Weight 0 : Robert's requests to not work shift D on Sun 2 is denied

Hands-on Explainable Constraint Programming (XCP)

• The model: Nurse Rostering
• The system: CPMpy modeling library
• Explain UNSAT:
  • Causal explanations (MUS, OUS, sequence)
  • Conversational explanations
• Explain a solution:
  • Causal explanations
  • Contrastive explanations

Explainable Constraint Programming (XCP)

In general, "Why X?"        (with X a solution or UNSAT)

To be defined... 3 patterns:

• Causal explanation:
  • How was X derived?
• Contrastive explanation:
  • Why X and not Z?
• Conversational explanation:
  • Iteratively refine explanation & model

Connections to wider XAI

• Explanations in planning, e.g. MUGS [Eiflet et al], Model Reconciliation [Chakraborti et al], ...
• Explanations for KR/justifications [Swartout et al], ASP [Fandinno et al], in OWL [Kalyanpur et al], ...
• Formal explanations of ML models (e.g. impl. hitting-set based, [Ignatiev et al])

Explainable Constraint Programming (XCP)

Recurring challenges:

• Definition of explanation: question and answer format
• Computational efficiency
• Explanation selection: which explanation to show
• User Interaction? (visualisation, conversational, statefull, ...)
• Explanation evaluation: computational, formal, user survey, user study, ...

Conclusion

• Explanation of UNSAT/SAT/Opt

• Causal explanations relate back to finding a MUS/OUS

• Need for programmable multi-solver tooling: CPMpy

• Many open challenges and new problems!

• Less developed: contrastive & conversational expl.

• We need incremental CP-solvers!

References mentioned (many more exist!!!)

MUS

• Liffiton, M. H., & Sakallah, K. A. (2008). Algorithms for computing minimal unsatisfiable subsets of constraints. Journal of Automated Reasoning, 40, 1-33.

• Ignatiev, A., Previti, A., Liffiton, M., & Marques-Silva, J. (2015, August). Smallest MUS extraction with minimal hitting set dualization. In International Conference on Principles and Practice of Constraint Programming (pp. 173-182). Cham: Springer International Publishing.

• Joao Marques-Silva. Minimal Unsatisfiability: Models, Algorithms and Applications. ISMVL 2010. pp. 9-14

Feasibility restoration

• Senthooran, I., Klapperstueck, M., Belov, G., Czauderna, T., Leo, K., Wallace, M., ... & De La Banda, M. G. (2021). Human-centred feasibility restoration. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Schloss Dagstuhl-Leibniz-Zentrum für Informatik.

Explaining optimization problems

• Korikov, A., & Beck, J. C. (2021). Counterfactual explanations via inverse constraint programming. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Schloss Dagstuhl-Leibniz-Zentrum für Informatik.

Explanation in planning, ASP, KR

• Eifler, Rebecca, Michael Cashmore, Jörg Hoffmann, Daniele Magazzeni, and Marcel Steinmetz. "A new approach to plan-space explanation: Analyzing plan-property dependencies in oversubscription planning." In Proceedings of the AAAI Conference on Artificial Intelligence, vol. 34, no. 06, pp. 9818-9826. 2020.
• Chakraborti, Tathagata, Sarath Sreedharan, Yu Zhang, and Subbarao Kambhampati. "Plan explanations as model reconciliation: moving beyond explanation as soliloquy." In Proceedings of the 26th International Joint Conference on Artificial Intelligence, pp. 156-163. 2017.
• Fandinno, Jorge, and Claudia Schulz. "Answering the “why” in answer set programming–A survey of explanation approaches." Theory and Practice of Logic Programming 19, no. 2 (2019): 114-203.
• Swartout, William, Cecile Paris, and Johanna Moore. "Explanations in knowledge systems: Design for explainable expert systems." IEEE Expert 6, no. 3 (1991): 58-64.
• Kalyanpur, Aditya, Bijan Parsia, Evren Sirin, and Bernardo Cuenca-Grau. "Repairing unsatisfiable concepts in OWL ontologies." In The Semantic Web: Research and Applications: 3rd European Semantic Web Conference, ESWC 2006 Budva, Montenegro, June 11-14, 2006 Proceedings 3, pp. 170-184. Springer Berlin Heidelberg, 2006.

Formal explantions in ML

• Ignatiev, Alexey, Nina Narodytska, and Joao Marques-Silva. "Abduction-based explanations for machine learning models." In Proceedings of the AAAI Conference on Artificial Intelligence, vol. 33, no. 01, pp. 1511-1519. 2019.