A reduced codification for the logical representation of Job Shop Scheduling Problems

Abstract

This paper presents the Job Shop Scheduling Problem (JSSP) represented as the well known Satisfiabilty Problem (SAT). Even though the representation of JSSP in SAT is not a new issue, presented here is a new codification that needs fewer clauses in the SAT formula for JSSP instances than those used in previous works. The codification proposed, which has been named the Reduced Sat Formula (RSF), uses the value of the latest starting time of each operation in a JSSP instance to evaluate RSF. The latest starting time is obtained using a procedure that finds the critical path in a graph. This work presents experimental results and analytical arguments showing that the new representation improves efficiency in finding a starting solution for JSSP instances. © Springer-Verlag Berlin Heidelberg 2004.