arrow
Return

Employee Scheduling With SAT-Based Pseudo-Boolean Constraint Solving

delete2021-01-01
delete0
delete
OA
AI
R
Robert Nieuwenhuis
A
Albert Oliveras
E
Enric Rodríguez-Carbonell *
E
Emma Rollón
DOI:10.1109/ACCESS.2021.3120597delete
deleteOriginal
deleteOriginal request for help
deleteShare
deleteSave
Abstract

Abstract

En 中文
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.
Keywords:
Scheduling
Schedules
Costs
Companies
Processor scheduling
Space exploration
Operations research
Employee scheduling
0-1 integer linear program
propositional satisfiability

Journal

IEEE Access cover
IEEE Access
IF:
3.6
Papers:
9.8W
Citations:
29.4W

Organization

U
universitat politecnica de catalunya
Scholars:
1.9W
Papers: 1.6W
Citations: 17