Syntax-Guided Pruning Rule Synthesis for Single Machine Scheduling

Machine scheduling problems model the allocation and sequencing of jobs on limited processing resources. Single Machine Scheduling Problems consider the special case in which all jobs share a single processing resource. They arise in settings such as sequencing jobs on a production line, ordering aircraft on a runway, or assigning patients to a shared medical scanner.

Many Single Machine Scheduling variants are computationally challenging and NP-hard in their general formulation, often making the direct use of exact methodologies intractable. Despite this, their constraints and objectives often exhibit structure that exact methods can exploit through pruning rules, which discard provably dominated regions of the search space without compromising optimality.

I am currently exploring the general use of Satisfiability Modulo Theories for the verification and synthesis of pruning rules in Single Machine Scheduling. This work is currently in progress, and will be updated upon completion.