This thesis addresses the problem of determining the treewidth of a graph, a key parameter for solving many NP-complete combinatorial problems on graphs. We present a novel approach that encodes the treewidth problem as SAT instances and solves them using modern SAT solvers. The work describes the encoding process and provides a comprehensive comparative analysis of the SAT approach against other exact and heuristic algorithms (PID-BT, CopsAndRobber, QuickBB). Experiments on standard and randomly generated graphs show that the SAT-based method achieves competitive results on small and medium-sized instances while also enabling the verification of heuristic solution optimality.
|
