Combinatorial optimization for job sequencing with one common and multiple secondary resources by using a SAT solver augmented with a domain-specific heuristic
More Info
expand_more
expand_more
Abstract
This paper solves job sequencing with one common and multiple secondary resources (JSOCMSR) problem by encoding it as a Boolean satisfiability (SAT) problem and applying domain-specific heuristics to improve the SAT solver’s performance. JSOCMSR problem is an NP-hard scheduling problem where each job utilizes two resources: a shared resource and a secondary job-dependent resource. First, the problem was modeled as an instance of SAT and then the SAT solver was augmented with a static greedy variable-ordering heuristic. This heuristic has led to significant improvement in the solver’s speed compared to a generic SAT heuristic for problem instances of larger size.