Aplicação do Max-SAT Parcial Ponderado para Otimização do Problema do Caixeiro-Viajante

Abstract

Boolean Satisfiability (SAT) is a problem of great relevance in both theoretical and practical terms. SAT solvers can solve various combinatorial problems successfully in computer science and artificial intelligence. With recent advances in solver heuristics, many industrial problems can be solved quickly and efficiently with the application of SAT solvers, in particular, the weighted partial Maximum Satisfiability Problem (Max-SAT) plays a key role in solving problems of the combinatorial optimization class. The Traveling Salesman Problem (TSP) is among the main combinatorial optimization problems studied, due to its application in real-life scenarios covering different fields of knowledge, such as operations research, electronics, mathematics, engineering, genetics, and computer science. The aim is to determine the minimum cost route that visits all the vertices and returns to the starting point. Thus, this research aims to propose a post-improvement procedure for the traveling salesman problem using a reduction of the problem to a weighted partial Max-SAT. Adapting the Christofides solution and improving the initial route, the proposed modeling is applied as a post-improvement process to the improvement already carried out by the 2-Opt algorithm. Benchmarking with different instances of the TSPLIB library was carried out to analyze the approach’s impact on the solution’s quality. The results suggest an improvement in the quality of the solution at a reasonable computational cost.