smt; workforce scheduling; bitvectors; linear arithmetic
en
Abstract:
Für viele Organisationen und Unternehmen ist es von entscheidender Bedeutung ihr Personal optimal einzusetzen, um zum einen die Produktivität zu steigern und zum anderen die Personalkosten möglichst gering zu halten. Zur Verbesserung der Auslastung des Personals, werden Dienstpläne zur Einteilung der Mitarbeiter in verschiedene Schichten erstellt. Hierbei müssen neben den Anforderungen des Unternehmens auch gesetzliche Bestimmungen und indivduelle Interessen der Arbeitnehmer berücksichtigt werden. Dies stellt eine Herausforderung dar, welche selbst mit der Unterstützung aktueller Computersysteme im Allgemeinen nicht effizient gelöst werden kann.<br />In den letzten 40 Jahren wurden zahlreiche computergestützte Methoden zur Lösung von Schichtplanproblemen entwickelt. Dabei wurden neben exakten Verfahren wie dem Constraint Programming auch heuristische Methoden eingesetzt.<br />Exakte Methoden lösen zwar eine große Anzahl an Schichtplanproblemen, können jedoch Pläne für viele Mitarbeiter nicht effizient erstellen. Es ist deshalb von großem Interesse neue exakte Methoden zu entwickeln, welche auch für schwierige Probleme geeignete Dienstpläne berechnen können.<br />In dieser Arbeit wird ein neues exaktes Verfahren für ein spezifisches Schichtplanproblem, Rotating Workforce Scheduling (RWS), vorgestellt.<br />Dafür wird RWS als Satisfiability Modulo Theories (SMT) Problem modelliert. SMT beschreibt ein Entscheidungsproblem welches auf der Erfüllbarkeit von Prädikatenlogik erster Stufe unter der Berücksichtigung bestimmter Theorien beruht. Während das Lösen von SMT Problemen mit SMT-Solvern automatisiert werden kann, stellt das Finden einer geeigneten und effizienten Formulierung in SMT die größte Herausforderung dar. Im Rahmen meiner Diplomarbeit etnwickelte ich zwei Modellierungen für das RWS Problem. Zuerst entwarf ich mit Hilfe von linearer Arithmetik eine elegante Formulierung, die jedoch bei großen Probleminstanzen an ihre Grenzen stößt. Die zweite Modellierung weist diese Limitierung nicht auf, da durch die Verwendung von Bitvektoren und binären Operationen eine kompakte Formulierung und eine Reduktion der Variablen erzielt werden konnte.<br />Beide Ansätze wurden anhand von 20 Probleminstanzen aus der Literatur experimentell evaluiert, wofür verschiedene SMT-Solver eingesetzt wurden. Die Bitvektor Formulierung erzielte im Vergleich zu jener mit linearer Arithmetik bessere Ergebnisse. Der Vergleich mit anderen Methoden aus der Literatur zeigte außerdem, dass SMT-Solving ein kompetitives Verfahren ist, welches Probleminstanzen löst, die andere exakte Verfahren bisher nicht lösen konnten.<br />
de
Rotating workforce scheduling (RWS) is an important real-life problem that appears in a large number of different business areas.<br />Well-constructed workforce schedules can have a significant impact on labor costs, improve productivity and thus influence a company or organization's efficiency. Designing such schedules includes a number of constraints that have to be fulfilled in order to respect legal restrictions or to consider the employee's individual preferences. This makes RWS a difficult task which sometimes even exceeds the possibilities of modern computer systems.<br />Over the last decades many approaches to rotating workforce scheduling have been proposed, including exact methods like constraint programming and heuristic techniques. Although exact approaches provide solutions for many instances, solving large problems is still a challenge to them.<br />Therefore, finding other exact methods able to provide better results for larger problems is an important issue in the field of rotating workforce scheduling.<br />In this thesis, I propose a new approach to RWS by using the recent advances on Satisfiability Modulo Theories (SMT). SMT-solving has been successfully applied to a number of different problems in software verification or test-case generation and moreover to constraint satisfaction problems with practical relevance. While solving can be automated by using a number of so-called SMT-solvers, the most challenging task is to find an efficient formulation of the problem in first-order logic. I developed two new modeling techniques for RWS that encode the problem using formulas over different background theories.<br />The first encoding provides an elegant approach based on linear integer arithmetic. Although this modeling technique showed promising results, it reaches its limits when applied to large-scale problems. To overcome this issue, I proposed a new formulation based on bitvectors in order to achieve a more compact representation of the constraints and a reduced number of variables. These two modeling approaches were experimentally evaluated on benchmark instances from literature using different state-of-the-art SMT-solvers.<br />By comparing the performance of the two encodings to each other, the superiority of the bitvector approach could be determined. Compared to other exact methods, the results of this approach showed a significant improvement in the number of found solutions. The bitvector encoding was able to solve 18 out of 20 benchmark instances, providing a solution to several instances that had not been solved yet by other exact methods.