A Compact SAT Encoding for Non-Preemptive Task Scheduling on Multiple Identical Resources

This paper presents an efficient SAT-solving approach for addressing the NP-hard problem of non-preemptive task scheduling on multiple identical resources. This problem is relevant to various application domains, including automotive, avionics, and industrial automation where tasks compete for shared resources. The proposed approach, called CSE, incorporates several novel optimizations, including a Block encoding technique for efficient continuity constraint representation and specialized symmetry-breaking constraints to prune the search space. We evaluate the performance of CSE compared to state-of-the-art SAT encoding schemes and leading optimization solvers like Google OR-Tools, IBM CPLEX, and Gurobi through extensive experiments across diverse datasets. Our method achieves substantial reductions in solving time and exhibits superior scalability for large problem instances.