Self-reconfiguration of manufacturing systems using Satisfiability Modulo Theory

Industrial companies increasingly face frequent and complex changes requiring rapid adaptation. These changes may be internal–such as equipment breakdowns–or external, such as the arrival of urgent orders or delayed deliveries. To address such variations, companies can implement actions ranging from simple adjustments to process logic (e.g., equipment re-parameterisation or rescheduling) to more substantial modifications, such as altering the composition or layout of production system equipment. This research focuses on the latter case, specifically on system reconfiguration. With the growing complexity of production systems and the critical nature of related challenges (e.g., safety, financial, and technological concerns), the reconfiguration process demands effective decision-support tools. This underscores the need to integrate self-reconfiguration capabilities into production systems. In this paper, we propose a self-reconfiguration algorithm composed of three phases: (1) detection of the need for reconfiguration, (2) diagnosis of the need and search for alternative solutions, and (3) definition of a new layout. To automate the resolution of the reconfiguration problem, we formulate it as a constraint satisfaction problem, modelled using Satisfiability Modulo Theories (SMT) logic equations and solved with an SMT solver. A case study is provided to illustrate the feasibility and potential of the proposed self-reconfiguration approach and algorithm.