{"id":"212d8090-afe2-4877-9c7d-c342f1545d14","arxiv_id":"2412.10272","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":3.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A constraint-programming tool for workforce allocation adds explainable conflict visualization and interactive feasibility restoration via MUS/MCS computation and user-weighted task priorities.","lead":"Researchers from Airbus and KU Leuven built a prototype tool that assigns worker teams to scheduled tasks using constraint programming, and shows users why some assignments are impossible. The goal is to make industrial scheduling systems more transparent and let human planners resolve conflicts interactively.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The central scalability assumption for the explanation back-end is untested: MUS/MCS times are reported only for 'few dozen' activities, while the stated industrial range reaches about 1000, so interactive conflict resolution may not transfer to real instances.","rationale":"The reader's weakest assumption and this stress-test pass converge on the same load-bearing risk: the explainability components are only demonstrated on 'few dozen' activities, while the industrial target reaches about 1000 activities. The paper's own text supports this reading: Section 4.1.1 states that the optimization results 'do not constitute a comprehensive benchmark', Section 4.1.2 states that 'further experiments are necessary to draw definitive conclusions', and Section 5 explicitly flags 'scalability challenges for the XAI technology bricks such as MUS computation'. The constraint count in the model grows with the number of activities and teams; deletion-based MUS extraction has a linear number of solver calls, and the interactive MCS re-computation loop multiplies that cost. Therefore the central claim that the tool provides practical interactive conflict resolution in the stated industrial scenario is not yet established. No internal inconsistency or fatal flaw is identified; the prototype and the optimization results are credible evidence for the small-instance version of the claim. The verdict should remain CONDITIONAL: the authors should provide scaling experiments at the industrial upper range and, for the trustworthiness claim, user studies. The proposed concrete test directly targets the scaling gap and would settle whether the concern actually lands.","tokens_in":10455,"tokens_out":6694,"duration_ms":64783,"concrete_test":"Rerun the Section 4.1.2 MUS benchmark and the Section 3.2 MCS-based interactive loop on generated instances at 100, 300, and 1000 activities, maintaining |W| approximately 20 and the 24-hour horizon, using the same Exact solver and 30-second per-solve timeout. Record the end-to-end wall-clock time to produce the first MUS and to complete one user-driven restoration cycle, for example relaxing five constraints with MCS re-computation after each step. If the 1000-activity MUS/MCS computation time is not within an interactive response target of about 60 seconds, the paper's practical claim for the industrial case is unsupported.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The load-bearing assumption is that the explainability back-end, not just the CP-SAT optimization core, will remain within interactive time limits on the industrial instances described in Section 4. Table 1 shows fast optimization, but the explanation experiments in Table 2 are run only on instances with 'a few dozen activities' and report average MUS computation of 0.60-1.13 seconds. The industrial use case is stated as ranging from 'a few dozen activities to possibly up to one thousand' (Section 4). Deletion-based MUS extraction invokes the solver once per constraint (Section 4.1.2); with |W| approximately 20 and about 1000 activities, the model contains tens of thousands of constraints, so even subsecond incremental solves can make full MUS extraction, and especially the iterative MCS re-computation described in Section 3.2, exceed an interactive response budget. This is not an internal contradiction: the paper itself says in Section 5 that the scheduling extension 'raises interesting scalability challenges for the XAI technology bricks such as MUS computation', and Section 4.1.2 cautions that 'further experiments are necessary to draw definitive conclusions'. The missing piece is precisely a scaling experiment at the stated upper range. The related concern that no user study yet supports the 'trustworthiness' claim is secondary; the tool's central claim of offering an interactive conflict-resolution method depends first on whether explanations can be computed fast enough at industrial scale.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents an ongoing project on a constraint programming (CP) based decision-support tool for workforce allocation, with a focus on explainability and trustworthiness. The authors define a Boolean CP model with allocation, non-overlap, compatibility, same-team, and used-team constraints, plus redundant clique and symmetry-breaking constraints. The tool computes and visualizes conflicts via minimal unsatisfiable subsets (MUS) and supports interactive feasibility restoration through local MUS resolution, global minimal correction subset (MCS) guidance, and weighted task-priority fine-tuning. A prototype implemented with CPMpy and Streamlit is described, and preliminary experiments report optimization times and MUS computation times on generated instances of 6, 8, and 24 hours. The paper concludes with planned user studies and a scheduling extension.","tokens_in":10665,"tokens_out":5222,"duration_ms":50732,"significance":"If the prototype performs as claimed, the work is a useful industrial application paper combining standard explainable CP techniques (MUS/MCS) with a human-in-the-loop interface for a realistic workforce allocation problem. The CP model is precisely specified, the MUS/MCS definitions are standard, and the paper clearly acknowledges open limitations, including the need for user studies and scalability challenges. The main value is in demonstrating how existing XAI-for-CP components can be assembled into an interactive tool and in identifying concrete gaps for future work. The contribution is not a new algorithm or proof, and the current empirical evidence is preliminary, so the significance depends on whether the interactive conflict-resolution claim can be shown to hold at the stated industrial scale and with users.","major_comments":[{"comment":"The explainability experiments are run only on instances described as 'a few dozen activities', yet Section 4 states that the industrial use case ranges up to about one thousand activities with |W|≈20. The deletion-based MUS algorithm described in Section 4.1.2 requires one solver call per constraint, and the MCS-based interactive workflow in Section 3.2 re-computes an MCS after each user relaxation; neither cost is measured at the stated upper range. Please report explicit instance sizes in terms of numbers of activities, teams, and constraints, and provide scaling experiments (e.g., 50, 200, 500, 1000 activities) with percentiles or worst-case times rather than only means. Without this, the 'interactive' restoration claim cannot be transferred to the industrial setting.","section":"Section 4.1.2, Table 2"},{"comment":"The column labeled 'optimal' is never defined in the text or the table caption; it appears to be the fraction of instances proven optimal within the 30-second timeout, but this must be stated explicitly. Because the reported t_solve values mix complete solves with timeout-censored runs, the mean is not a clean measure of computation time; report the success rate separately, with medians and quantiles, and state the timeout for each row. The discussion of the symmetry constraints is also ambiguous: in the multi-worker rows, adding symmetry increases t_solve (e.g., 0.06 to 0.18 for len 6), while the text says symmetry and redundant constraints have 'a clear negative effect' on initialization and solving; clarify whether the negative effect claim refers to t_solve or t_total, and distinguish it from the mono-worker setting where symmetry improves the optimality rate.","section":"Section 4.1.1, Table 1"},{"comment":"The statement in the Local Conflict Resolution part that 'few iterations were required to restore feasibility, and we surmise that this observation remains true for real scenarios' is not supported by any reported experiment or iteration count. If this observation is intended to support the practicality of the interactive MUS workflow, provide the number of instances, the number of iterations, and the user actions involved; otherwise, remove the conjecture or clearly mark it as an anecdote.","section":"Section 4.2.4"},{"comment":"The title and abstract claim 'trustworthy' decision-making, but the paper reports no user study or established trust metric; Section 5 explicitly defers user studies to future work. The manuscript should either narrow the claim to the system's potential for trustworthiness and explainability, or include a preliminary evaluation with expert users. This is not a request to prove the psychology of trust, but the current wording overstates what the evidence supports, especially since the abstract describes the tool as 'intended to be evaluated'.","section":"Sections 1, 3, and 5"}],"minor_comments":[{"comment":"There are typos in Table 1 ('T rue', 'F alse', 'T rue T rue') and in Definition 2 ('an only if' should be 'if and only if').","section":"Table 1 and Definition 2"},{"comment":"The phrase 'a few dozen activities' is vague; please report the exact numbers of activities used in the generated instances, as well as the numbers of teams and constraints, so the results are reproducible.","section":"Section 4"},{"comment":"The symmetry-breaking constraint is described as 'lexleader' but never formally defined; either give the definition or cite the exact formulation used.","section":"Section 2.2, constraint 6b"},{"comment":"No code or data repository is provided, which makes the prototype and experiments difficult to reproduce; consider adding a link to the demonstrator or an anonymized experiment package.","section":"General"},{"comment":"The average explanation length is exactly 10 in all three rows, with no reported variance or instance-level detail; report the distribution or at least the standard deviation, and state how many instances were included per row.","section":"Table 2"}],"recommendation":"major_revision","confidential_remarks":"This is a preliminary work-in-progress paper, more suited to a short application/tool track than a full archival journal paper. The central prototype and model description are plausible, and the limitations are acknowledged, but the empirical support is thin and the trustworthiness claim outstrips the evidence. The main technical risk is scalability of the MUS/MCS backend to the stated industrial range; I would condition acceptance on a scaling experiment or an explicit narrowing of the claimed scope. I saw no sign of circularity or fabrication. The editor may also wish to consider whether the paper's novelty relative to existing human-centred feasibility restoration work is sufficient for the venue."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Bottom line: this is an honest tool/position paper, not a results paper. The thing to know: the prototype is real and the CP model is clearly specified; the thing that worries me is that the one number that would make the interactive explainability story work — explanation runtime at the stated industrial scale (up to ~1000 activities) — is missing. The stress-test note lands.\n\nWhat's new is modest. MUS/MCS-based infeasibility explanation is standard, and interactive feasibility restoration has been done before (they cite Senthooran et al. 2021). The contribution is the integration into a concrete workforce-allocation tool with a Gantt-based conflict view and three interaction modes: MUS-by-MUS, MCS with re-computation, and weighted priorities. That integration is useful for the explainable-CP community as a worked example, and the paper is transparent that this is an ongoing project with evaluation still to come.\n\nWhere it's soft: (1) Scalability. Table 2 stops at 24-hour instances with 'a few dozen activities'; the stated industrial range goes to ~1000. Deletion-based MUS extraction solves once per constraint, and the MCS re-computation loop in Section 3.2 repeats that. The authors flag this themselves in Section 5, and Section 4.1.2 says 'further experiments are necessary.' That is not fatal in a paper that is explicitly preliminary, but it is the load-bearing gap. (2) The reported numbers are thin: Table 1 has an 'optimal' column that is never defined (fraction of instances solved to optimality? something else?), and there are no standard deviations or per-instance breakdowns. For 20 instances, means without spread are hard to read. (3) No artifact link and no user study, so 'trustworthiness' remains a design goal rather than a demonstrated property. The paper says as much, which is fine, but the title promises a bit more than the content delivers.\n\nThe citation pattern looks fine, and the model description is precise enough to reimplement. There is no circularity and nothing that looks invented.\n\nWho this is for: people working on explainable CP and human-in-the-loop scheduling who want a concrete example of MUS/MCS interactivity in an industrial context. It deserves a serious referee at a venue that accepts application/system papers about ongoing work, with the expectation that the authors tighten the empirical reporting and, ideally, add a scaling experiment along the lines of the stress-test note.","headline":"Honest tool paper with a clearly specified CP model; the interactive explainability story rests on a scaling assumption the authors themselves admit is untested.","tokens_in":11258,"tokens_out":1995,"would_cite":false,"duration_ms":629694,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper claims that infeasible workforce-allocation problems can be handled transparently by a constraint-programming tool that computes minimal conflicts (MUS) and minimal repairs (MCS), presents them visually, and lets planners…","keywords":["constraint programming","explainable AI","workforce allocation","scheduling","minimal unsatisfiable subset (MUS)","minimal correction subset (MCS)","human-in-the-loop","infeasibility restoration"],"falsifier":"Generate infeasible instances at 100, 500, and 1000 activities with the same constraint types and measure the time to produce one MUS; if average explanation time grows steeply (for example, from seconds to minutes) while optimization remains fast, the interactive promise of the tool fails at industrial scale.","tokens_in":10236,"feed_emoji":"🧩","tokens_out":7481,"duration_ms":63205,"temperature":0.7,"pith_summary":"Workforce allocation in industry often fails because constraints—team availability, skills, non-overlap, travel time—cannot all be met at once, and standard solvers only return 'infeasible' with no reason. The paper is trying to establish that a constraint-programming tool can make such infeasibilities transparent: it computes an irreducible set of conflicting constraints (a MUS) or a minimal set to relax (an MCS), shows them on a Gantt chart, and lets planners restore feasibility interactively. Preliminary runs on generated instances up to 24 hours show that optimization finds optimal allocations in under a second with multiple search workers, and computing one explanation takes about a second. The stated aim is that planners will trust and accept automated schedules because they can see and control why an allocation fails.","feed_headline":"Workforce tool explains why schedules fail and how to repair them","feed_subtitle":"When no team plan exists, it pinpoints conflicting constraints and offers interactive ways to fix them.","key_machinery":"The machinery is a Boolean constraint model plus the MUS/MCS explanation pair. A MUS is an inclusion-minimal subset of constraints that is still unsatisfiable, showing the user the smallest conflict to attack. An MCS is an inclusion-minimal subset whose removal makes the whole constraint set satisfiable, showing the user the cheapest global repair. The tool computes these with deletion-based extraction on a pseudo-Boolean solver running under assumptions, and visualizes the result by solving a size-maximal satisfiable subproblem, drawing allocated tasks in a Gantt chart and putting unallocated tasks on an 'Unset' line. A third mechanism rewrites the 'every task must be allocated' constraint as a weighted objective, so users can tune task priorities and have the solver drop low-weight tasks first.","core_discovery":"The central claim is that infeasibility is not a dead end but material for an interactive dialogue. On a Boolean constraint model where every activity must be assigned exactly one compatible team and no team overlaps its tasks, the tool detects unsatisfiability and mines a Minimal Unsatisfiable Subset—a smallest set of constraints that cannot be satisfied together—then lets the user relax constraints step by step, apply a Minimal Correction Subset globally, or re-prioritize tasks so that a weighted Max-CSP solver drops lower-priority allocations first. On the paper's generated benchmark set, the explanation calculation stays within 0.6–1.13 seconds and explanations stay around 10 constraints regardless of instance length, which supports the claim that explainable conflict resolution is computationally practical at the tested scale.","pith_inferences":["The paper leaves implicit that the three restoration mechanisms are complementary: MUS resolution gives local control, MCS gives global minimal repair, and priority tuning gives preference-driven repair; a natural hypothesis is that different user roles will prefer different mechanisms.","If instance size grows to the stated industrial scale of up to roughly a thousand activities, MUS/MCS computation may need decomposition or step-wise explanations; the paper flags this as future work on the path to a scheduling model.","A testable extension would be to measure whether users who interactively relax constraints produce solutions closer to their implicit planning knowledge than users who accept a solver's optimal solution without explanation.","The 'Unset' visualization trick—solving a size-maximal satisfiable subproblem to draw a Gantt chart for an infeasible instance—could be reused in other scheduling explainability interfaces."],"forward_implications":["If the tool works as described, planners no longer face a binary feasible/infeasible answer; they get a concrete set of constraints to examine and relax.","Interactive MCS relaxation can be iterative: after a user accepts only part of a correction set, the tool recomputes a new MCS, supporting mix-and-match repairs.","The weighted Max-CSP formulation gives a direct way to encode planner expertise as task priorities, turning feasibility restoration into an optimization over user preferences.","Preliminary timing suggests MUS computation scales acceptably for instances up to 24 hours and a few dozen activities, but the paper itself notes that further experiments are needed.","The prototype is intended as a basis for future user studies measuring understandability and acceptance, not just computation time."],"supporting_citations":[{"why":"The handbook reference that supplies the constraint programming paradigm on which the allocation model is built.","marker":"[34]"},{"why":"The Python modeling library used to encode the problem and to compute MUSes and MCSes.","marker":"[11]"},{"why":"The cited source for the formal definitions of minimal unsatisfiable subset and minimal correction subset.","marker":"[23]"},{"why":"The deletion-based MUS extraction algorithm that the tool's conflict computation relies on.","marker":"[25]"},{"why":"The pseudo-Boolean solver used for incremental MUS computation under assumptions.","marker":"[7]"},{"why":"The main solver backend for the optimization experiments, especially its multi-worker portfolio search mode.","marker":"[32]"},{"why":"General treatment of feasibility and infeasibility in optimization that motivates the interactive restoration approach.","marker":"[5]"},{"why":"Step-wise explanation sequences, cited as the proposed route to handle large conflict explanations in future scheduling extensions.","marker":"[1]"}],"fun_headline_variants":["When workforce plans clash, this tool finds the culprit constraints","Explainable AI for workforce: turns infeasibility into dialogue","Find and fix impossible team schedules with minimal conflicts","Unsatisfiable? This tool explains and helps you repair it","Tool pinpoints unsolvable schedules and fixes them interactively"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The weakest load-bearing premise is that the explanation computations stay fast enough on real industrial instances, which can reach roughly a thousand activities, even though the experiments here cover only a few dozen.","fun_headline_variants_meta":{"raw":{"variants":["When workforce plans clash, this tool finds the culprit constraints","Explainable AI for workforce: turns infeasibility into dialogue","Find and fix impossible team schedules with minimal conflicts","Unsatisfiable? This tool explains and helps you repair it","Tool pinpoints unsolvable schedules and fixes them interactively"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000717,"raw_usage":{"total_tokens":3148,"prompt_tokens":799,"completion_tokens":2349,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":415,"completion_tokens_details":{"reasoning_tokens":2267}},"tokens_in":415,"tokens_out":2349,"duration_ms":14292,"temperature":1.0,"reasoning_tokens":2267,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T15:59:02.189041+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Generate infeasible instances at 100, 500, and 1000 activities with the same constraint types and measure the time to produce one MUS; if average explanation time grows steeply (for example, from seconds to minutes) while optimization remains fast, the interactive promise of the tool fails at industrial scale.","supporting_citations":[{"cited_title":"Or-tools","cited_arxiv_id":null,"evidence_quote":"The Python modeling library used to encode the problem and to compute MUSes and MCSes."},{"cited_title":"Simplifying step-wise explanation sequences","cited_arxiv_id":null,"evidence_quote":"Step-wise explanation sequences, cited as the proposed route to handle large conflict explanations in future scheduling extensions."}],"review_version":1}