Scientific Program > Talks by Speaker > Frank Stefan

Most real-world applications in context of routing and scheduling involve special side constraints to model applied conditions and resource requirements. Especially temporal availability of staff members, working hour regulations, inter-route constraints, and other issues regarding interdependencies between resources, respectively synchronization between routes, lead to hard combinatorial optimization problems and specialized algorithms therefor. It is a hard task on its own to get valid solutions for such high-constraint problems. Achieving high-quality results fast is even more challenging. Simple or more specialized typical construction heuristics often fail to find valid solutions at all, while improvement heuristics evoke long running times as well as standard exact approaches.

We propose the integration of satisfiability testing (SAT) to proof feasibility of such problems. For this purpose we describe a generalized SAT encoding for the problems under consideration, which subsequent are solved by state-of-the-art SAT solvers. In addition we outline optimization strategies to obtain high-quality, respectively optimal, solutions. Computational results are reported on different problem classes which illustrate the efficiency of integrating SAT in the solving process.