Abstract

The satisfiability problem (SAT) is a well studied problem in logic which searches for a truth assignment of a set of Boolean variables that evaluates a specific formula to true. The bandwidth minimization problem for graphs (BMPG) is a well studied problem in graphs and requires finding the labels of the nodes of a graph such that the maximum absolute difference among neighbors is minimized. This paper presents a new approach for solving BMPG in the SAT realm. The main contributions of the article are the SAT model based on CNF format, and the approach that solves the BMPG problem based on these models. The approach maps a BMPG instance to a SAT instance, solves the SAT instance using an approximated algorithm, and transforms the SAT solution into the BMPG solution; it was experimentally compared against state-of-the-art BMPG algorithms over a well-known benchmark. The results showed that the quality of the solutions obtained by the approach presented in this paper is comparable to those previously reported. In addition, the development of the SAT model allows that any SAT solver that uses the CNF format can solve BMPG (this includes exact and non-exact algorithms).

Key words: Bandwidth minimization problem, constraint model, CNF format, SAT problem.