Fuchs, Nickel and Nöllenburg – METROSAT 2022

Description

This paper presents MetroSAT, two logic-based models—MaxSAT and SMT—for computing octolinear schematic metro maps by translating an established ILP formulation into Boolean and SMT constraints. The authors encode integer coordinates (using unary encoding and doubled coordinates) and express hard constraints ensuring octolinearity, preserved radial order at stations, planarity, and minimum edge spacing. Optimization objectives—minimizing line bends, deviation from geographical directions, and total edge length—are implemented as weighted soft clauses in MaxSAT and as weighted objectives in SMT (using Z3’s vZ). Implementation used PySAT/RC2 for MaxSAT and Z3 for SMT, compared against an ILP/Gurobi baseline. Experiments on Vienna and Karlsruhe networks show that ILP is faster on small instances, but MaxSAT and SMT scale better on larger instances where ILP timed out; SMT often performed competitively. The study concludes that logic-based methods are viable alternatives to ILP, highlights implementation details affecting runtime, and suggests further work on SMT theories, solver behaviors, and model formulation optimizations.