An Incremental SAT-Based Approach for Solving the Real-Time Taxi-Sharing Service Problem

EasyChair Preprint 3285, version 2

Abstract

This paper deals with a combinatorial optimization problem that models real-time taxi-sharing services; this problem has gained much attention in the areas of both artificial intelligence and computational social science. When a passenger α sends a demand to a taxi control center, the center tries to find an optimal solution to assign an appropriate taxi and re-plan its route for the demand so that the service can minimize the sum of the planned travel time for all served passengers (including α) who are allocated to the same taxi. Because finding a feasible solution to the real-time taxi-sharing service problem is NP-hard, most previous studies have focused on developing a semi-optimization algorithm based on well-known metaheuristics. We propose a novel algorithm based on incremental Boolean satisfiability solving with an extensible framework, to optimize the taxi allocation for demands occurring in real time. Our formulation is also suitable for other objective functions with small changes to the weighted constraints. The experiments, which are based on real-map data using a modified simulation of urban mobility, show that our new approach achieves higher performance with a reasonable computational cost compared to an existing insertion method that has been functioned in a real service application.

Keyphrases: Taxi sharing, combinatorial optimization, route planning

@booklet{EasyChair:3285,
  author    = {Aolong Zha and Qiong Chang and Itsuki Noda},
  title     = {An Incremental SAT-Based Approach for Solving the Real-Time Taxi-Sharing Service Problem},
  howpublished = {EasyChair Preprint 3285},
  year      = {EasyChair, 2020}}