Open AccessEmployee Scheduling With SAT-Based Pseudo-Boolean Constraint Solving
Author(s) -
Robert Nieuwenhuis,
Albert Oliveras,
Enric Rodriguez-Carbonell,
Emma Rollon
Publication year - 2021
Publication title -
ieee access
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.587
H-Index - 127
ISSN - 2169-3536
DOI - 10.1109/access.2021.3120597
Subject(s) - aerospace , bioengineering , communication, networking and broadcast technologies , components, circuits, devices and systems , computing and processing , engineered materials, dielectrics and plasmas , engineering profession , fields, waves and electromagnetics , general topics for engineers , geoscience , nuclear engineering , photonics and electrooptics , power, energy and industry applications , robotics and control systems , signal processing and analysis , transportation
The aim of this paper is practical: to show that, for at least one important real-world problem, modern SAT-based technology can beat the extremely mature branch-and-cut solving methods implemented in well-known state-of-the-art commercial solvers such as CPLEX or Gurobi . The problem of employee scheduling consists in assigning a work schedule to each of the employees of an organization, in such a way that demands are met, legal and contractual constraints are respected, and staff preferences are taken into account. This problem is typically handled by first modeling it as a 0–1 integer linear program (ILP). Our experimental setup considers as a case study the 0–1 ILPs obtained from the staff scheduling of a real-world car rental company, and carefully compares the performance of CPLEX and Gurobi with our own simple conflict-driven constraint-learning pseudo-Boolean solver.