Optimization based on timed Petri nets using CP-SAT - an integrated SAT and CP solver

Abstract

A simple but general semantics for timed Petri nets is presented in this paper. Based on this semantics, an optimization formulation is introduced and implemented in a recently developed optimization solver, where a satisfiability (SAT) solver is integrated with constraint programming (CP). The solver, called CP-SAT, is a part of Google’s OR-Tools. The optimization formulation includes both concurrent and alternative sequences of operations, involving shared as well as alternative resources. The proposed optimization strategy is compared with the SAT/SMT-based solver Z3Opt and Gurobi’s mixed integer linear programming (MILP) solver. The conclusion is that the computation time for CP-SAT is much shorter than for Z3Opt, while MILP is able to handle deep problems, including long sequences with many transitions, with similar computational performance as CP-SAT. On the other hand, CP-SAT is much faster than MILP for wide problems, including many parallel sequences. An evaluation of an industrial-sized flexible manufacturing system, which involves uncontrollable events, also demonstrates how efficient and easy to implement the proposed strategy is compared to existing results. In addition, it is also demonstrated how basic functionality in SAT and constraint programming are related and integrated in CP-SAT. The conclusion is that the strength of CP-SAT depends on its successful integration of search, inference, and OR-based relaxation on top of a satisfiability solver.