key: cord-0046678-003r4sjl authors: Ehlers, Rüdiger; Treutler, Kai; Wesling, Volker title: SAT Solving with Fragmented Hamiltonian Path Constraints for Wire Arc Additive Manufacturing date: 2020-06-26 journal: Theory and Applications of Satisfiability Testing - SAT 2020 DOI: 10.1007/978-3-030-51825-7_34 sha: 4a49245bf16248d33f51229673574237b8002dad doc_id: 46678 cord_uid: 003r4sjl 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. Modern additive manufacturing approaches hold a potential to add substantial flexibility to manufacturing processes. In additive manufacturing, an object is built step by step and ground up from raw material. While for plastics, 3D printing is already established, for metal, additive manufacturing is more complex, leading to a plethora of manufacturing approaches with different properties. A notable approach in this context is wire arc additive manufacturing (WAAM), where a metal object is welded from scratch onto a metal ground body using metal from a wire roll [5] . Utilizing an industrial welding robot, the approach enables the processing of relatively high volumes of metal in short time frames with a large number of possible materials (e.g. Titanium, Aluminum, Steels, Copper, . . .) [9, 14] . WAAM is based on arc welding, where an electric current induces the heat necessary to melt both the wire and the surface to which wire material gets attached. Different shielding gases are used to protect the weld from interacting with the air. A typical manufacturing system can be seen in Fig. 1 . The robot welds along a path that needs to be planned in advance. Traditionally, additive manufacturing is done layer by layer, just like for most 3D printers for plastics, so that these paths only need to be planned in 2D. The material properties of metals however depend on how quickly it cools down. For example, for low alloyed steel, the final material properties mainly depend on the time it takes for the material to cool down from 800 • C to 500 • C [4] . Shorter such so-called t8/5 times lead to a stronger and brittle material, while longer times lead to a tougher but weaker material with less residual stresses [4] . This can be exploited by making use of the possibility to stack up material locally during the welding process and to thus deviate from welding layer by layer, so that the material stays warm for a bit longer. The resulting local higher toughness can for instance be useful in the region of highly loaded notches [15] . On the other hand, far-sweeping welding paths speed up cooling, which is useful when a higher strength of the material is locally needed. Such material properties can at the same time be less important in other parts of the object. This gives the planning process some flexibility to attain local material properties, which is a clear advantage of additive manufacturing over traditional manufacturing processes. Planning in full 3D increases the size of the search space for possible welding paths dramatically, making the planning problem combinatorially complex. This observation asks for algorithmic support from computational engines such as SAT solvers. The planning problem has many side-constraints such as gravity (it is not possible to weld underneath a part of the object already welded), which can be encoded as clauses provided to the solver. The object to be welded can be composed of several welding paths, but the number of paths is typically low, as the disturbances caused by the ignition of the welding arc cause the local material properties to be worse and moving the robot head while not welding leads to an additional loss of shielding gas and material. We show in this paper how to search for welding paths with a satisfiability (SAT) solver. We discretize the object to be manufactured into blocks and represent the connections between these blocks in the form of a graph. Two blocks that can be manufactured in succession are connected by an edge in the graph. For this initial study of planning welding paths under cooling time constraints in 3D, we discretize the object parts into cubes, but the approach presented is not restricted to cubes. By searching for a fragmented Hamiltonian path in the graph, i.e., one that consists of multiple independent paths that together visit all vertices, we encode the search for welding paths that together implement the complete object manufacturing process. Additional constraints on the paths encode the process-induced requirements. In our approach, checking if the planned fragmented path satisfies the requested t8/5 times is done after finding a satisfying assignment to all variables. A simplified simulator calculates the temperatures in all blocks during the welding process and implements abstract versions of heat loss due to thermal conduction and radiation. Once in any block with upper and lower t8/5 time limits a t8/5 time span has been observed that lies outside of the specified range, the simulation stops and a clause is generated that requires some part of the welding paths simulated until then to be different. To illustrate a simulation, Fig. 2 shows a visualization the simulator state in the middle of a welding process. This paper is structured as follows: In the next section, we discuss the general approach to encoding the search for a fragmented Hamiltonian path into the SAT problem, including the special considerations from the application domain. Section 3 contains the architecture of our prototype solver, including details on the simulator for the evolution of the temperatures. Section 4 reports some experimental results, followed by a discussion of related work. We conclude with an outlook on future work and explain what role we expect SAT solving to play in additive manufacturing in the future. We assume familiarity with the basics of satisfiability solving (see, e.g., [3] for an introduction) in the following. To describe the encoding of the welding path planning problem as a fragmented Hamiltonian path problem, we first need to define the latter. , and after adding at most k − 1 edges to E, the sequences in S can be connected by the additional edges to a Hamiltonian path in G. The fragmented Hamiltonian path problem is NP-hard since the Hamiltonian path problem (its special case for k = 1) is also NP-hard. We want to use a SAT solver to tackle this problem despite its NP-hardness. Since the fragments of a fragmented Hamiltonian path cannot share vertices, they cannot share edges. We exploit this by defining one Boolean variable x e for every edge e ∈ E to encode whether the edge is part of a fragment or not. The values of these variables can then together completely represent a fragmented Hamiltonian path. Since every node can only be visited once, for every node and every pair of incoming edges of the node, we use a SAT clause requiring one of the respective Boolean edge variables to have a value of false. If a fragment originates in a node, there does not actually need to be an active incoming edge. To encode that there are at most k such nodes, we first allocate variables y v for every node v ∈ V to represent whether a fragment originates from the node. Then, we add a clause y v ∨ (v ,v)∈E x (v ,v) for every vertex v to ensure that all vertices in which no fragment starts have incoming edges. Finally, we use some type of cardinality constraint [13] to ensure that at most k variables in {y v } v∈V have values of true. So far, such an encoding does not guarantee that the edges selected cannot contain cycles, which is disallowed by Definition 1. Pandey and Rintanen [12] showed that acyclicity can be efficiently taken into account by non-clausal constraint that the SAT solver evaluates before deciding next variable values (and after unit propagation), as a clausal encoding needs large numbers of clauses and variables. Following their observations, we use the same approach in this paper. For the WAAM application, the graph represents the discretized blocks of the object to be welded and the order in which successive blocks can be welded. The fragments of a fragmented Hamiltonian path in the graph represent the welding paths that together build up the object. They cannot contain cycles since a block would then be welded twice. As the t8/5 times at the blocks depend on in which order the fragments are welded, we also need to encode this order. Using the assumption that k will normally be small in this application domain, we chose to do so using |V |×k many variables {z v,i } v∈V,1≤i≤k . A variable z v,i should have a value of true iff vertex v belongs to the ith path to be welded. To ensure that these variables have meaningful values, we first encode that every vertex has to be part of at least one fragment number, using |V | many clauses of length k. Then, we encode that all (successor) elements of a path are marked as belonging to the same order. We do so with the clauses Also, to exclude that all paths are marked as having the same index, we add the clauses v,v ∈V,1≤i≤k ¬y v ∨¬y v ∨¬z v,i ∨¬z v ,i which make sure that all path starting points have different fragment numbers. This constraint will be the only one in our encoding that requires a number of clauses quadratic in the number of vertices. The relatively variable-intensive encoding of which vertex belongs to which path number has the benefit that it enables us to concisely encode another important requirement for welding: vertices v that lie above vertices v in the three-dimensional grid cannot be welded in earlier fragments. It suffices to add the clauses v,v s.t. v is directly above v ,1≤i