SAT Solving with Fragmented Hamiltonian Path Constraints for Wire Arc Additive Manufacturing

In Wire Arc Additive Manufactoring (WAAM), an object is welded from scratch. Finding feasible welding paths that make use of the potential of the technology is a computationally complex problem as it requires planning paths in 3D. All parts of the object to be manufactured have to be visited in few welding paths. The search for such welding paths in 3D can be mapped to searching for a fragmented Hamiltonian path in a mathematical graph. We propose a SAT-based approach to finding such fragmented Hamiltonian paths that is suitable for planning WAAM paths. We show how to encode the search for such paths as a mix of SAT clauses and one non-clausal constraint that can be integrated into the SAT solver itself. The reasoning power of the solver enables us to impose additional constraints coming from the application domain on the planned paths, and we show experimentally that in this way, we can find welding paths for relatively complex object geometries.