Employee Scheduling With SAT-Based Pseudo-Boolean Constraint Solving

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 sc...

Full description

Saved in:
Bibliographic Details
Published in:IEEE access 2021, Vol.9, p.142095-142104
Main Authors: Nieuwenhuis, Robert, Oliveras, Albert, Rodriguez-Carbonell, Enric, Rollon, Emma
Format: Article
Language:English
Subjects:
0–1 integer linear program
Automobile rentals
Boolean
Boolean algebra
Companies
Costs
Employee scheduling
Operations research
Processor scheduling
propositional satisfiability
Schedules
Scheduling
Solvers
Space exploration
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2169-3536
2169-3536
DOI:10.1109/ACCESS.2021.3120597