Module interval_sched 

Interval scheduling in O(n log n) via a sweep line — the matching/Hall reasoner reaching into resource allocation over time.

Given n tasks, each an interval [start, end), and m interchangeable machines (or green windows, or registers), can every task run with no two overlapping tasks on one machine? This is colouring the tasks’ interval graph (overlap = edge), and interval graphs are perfect, so the chromatic number equals the largest clique — here, the maximum number of tasks overlapping at any instant. Hence it is feasible iff peak overlap ≤ m, decided by one sweep over the endpoints. When it overflows, the m+1 tasks active at the peak are a clique that needs m+1 machines — a Hall/pigeonhole certificate, exactly the structure Z3 grinds in the colouring encoding but we settle in near-linear time. Both outcomes are independently re-checkable.

Structs

Interval

A half-open task interval [start, end).

Enums

ScheduleOutcome

The outcome of scheduling onto m machines.

Functions

is_overflow_witness

Re-check an overflow witness: all the listed tasks pairwise overlap and there are more than machines of them — a clique that cannot be coloured with machines colours.

is_valid_schedule

Re-check a schedule: every assigned machine is in range and no two overlapping tasks share one.

peak_concurrency

The peak number of tasks active simultaneously — the interval graph’s clique number / chromatic number, i.e. the fewest machines (or registers) that suffice. One sweep, O(n log n).

schedule_or_overflow

Decide whether tasks can be scheduled on machines machines. Sweeps the endpoints to find the peak overlap: feasible iff that peak is ≤ machines, with a greedy interval colouring as the assignment, else the overflowing overlap-clique as the certificate.