SAT and SMT-based Interactive Conguration for Container Vessel Stowage Planning
Christian Kroer · 2012
The container vessel stowage problem is a hard combinatorial optimization problem concerned with the placement of containers on a container vessel, subject to various constraints. It is often the case that stowage coordinators need to modify existing stowage plans, while preserving their optimality. An interactive configuration system can guide the coordinator in this process. Such systems have previously been implemented using binary decision diagrams (BDDs), but this approach has been shown to have limited scalability. This thesis explores the usage of Boolean satisfiability (SAT) and satisfiability modulo theory (SMT) solvers as engines for such systems, to gain a better understanding of the scalability offered by using these approaches. Several methods for encoding the container vessel stowage problem as a SAT or SMT problem are introduced, and experimental results comparing the performance of BDD, SAT and SMT-based interactive configuration are presented, both on the container vessel stowage domain and on several other domains. The results show that SAT and SMTbased approaches suffer from scalability problems on the container vessel stowage domain, while providing strong performance on some other domains. In addition, experiments with simplified versions of the container vessel stowage problem are presented, giving insight on what makes the container vessel stowage problem hard for SAT and SMT-based interactive configuration systems.