Menentukan Dimensi Metrik Menggunakan Satisfiability Modulo Theories

Ajiwijaya, Fikri Yudhistira (2026) Menentukan Dimensi Metrik Menggunakan Satisfiability Modulo Theories. Other thesis, Institut Teknologi Sepuluh Nopember.

Text 5002211165-Undergraduate_Thesis.pdf - Accepted Version Restricted to Repository staff only Download (2MB) | Request a copy

Abstract

Dimensi metrik dan dimensi metrik sisi pada sebuah graf merupakan invarian fundamental dalam teori graf. Secara sederhana, dimensi metrik menyatakan banyaknya simpul paling sedikit yang diperlukan untuk membedakan seluruh simpul lain dalam graf, sedangkan dimensi metrik sisi menyatakan hal serupa tetapi untuk membedakan seluruh sisi. Invarian ini memiliki berbagai aplikasi, seperti navigasi jaringan, pelacakan sumber, robotika, dan sistem biologis. Tugas akhir ini mengeksplorasi penggunaan Satisfiability Modulo Theories (SMT) sebagai pendekatan untuk menghitung dimensi metrik dan dimensi metrik sisi. Permasalahan diformulasikan secara deklaratif dalam SMT dan diselesaikan menggunakan solver. Representasi graf kanonik digunakan untuk menghapus redundansi akibat automorfisma, dan eksperimen dilakukan pada seluruh graf terhubung unik dengan 2 hingga 9 simpul, serta beberapa graf berukuran lebih besar. Hasil eksperimen menunjukkan bahwa seluruh formulasi SMT menghasilkan dimensi metrik dan dimensi metrik sisi yang benar. Dari sisi waktu eksekusi, untuk graf berukuran kecil, pendekatan brute-force lebih cepat dibandingkan SMT. Sebaliknya, untuk graf berukuran besar, pendekatan SMT dengan teori pseudo boolean menunjukkan kecepatan eksekusi paling unggul, sementara metode brute-force seluruhnya gagal menyelesaikan perhitungan dalam batas waktu yang ditetapkan. Hasil ini menunjukkan bahwa SMT dapat digunakan untuk menghasilkan invarian graf dimensi metrik yang benar dan dengan tren kenaikan waktu eksekusi yang praktikal semakin bertambahnya ukuran graf.
======================================================================================================================================
The metric dimension and the edge metric dimension of a graph are fundamental invariants in graph theory. Roughly speaking, the metric dimension is the minimum number of vertices needed to distinguish all other vertices in the graph, while the edge metric dimension does the same for the edges. These invariants have a range of applications, such as in network navigation, source tracking, robotics, and biological systems. This thesis explores the use of Satisfiability Modulo Theories (SMT) as an approach to compute the metric dimension and the edge metric dimension. The problems are formulated declaratively in SMT and solved using a solver. Canonical graph representations are employed to remove redundancy caused by automorphisms, and experiments are conducted on all unique connected graphs with 2 to 9 vertices, as well as on some larger graphs. The experimental results show that all SMT formulations produce correct values for metric dimension and edge metric dimension. In terms of execution time, for small-sized graphs, the brute-force approach is faster than SMT. In contrast, for large-sized graphs, the SMT approach with pseudo boolean theory exhibits the best execution performance, while the brute-force method fails entirely to complete the computation within the given time limit. These results indicate that SMT can be used to generate correct graph invariants for metric dimension, with a practical execution-time growth as the graph size grows.

Item Type:	Thesis (Other)
Uncontrolled Keywords:	Dimensi Metrik, Metric Dimension, Dimensi Metrik Sisi, Edge Metric Dimension, Satisfiability Modulo Theories, SMT Solver, NP-hard
Subjects:	Q Science > QA Mathematics > QA166 Graph theory
Divisions:	Faculty of Science and Data Analytics (SCIENTICS) > Mathematics > 44201-(S1) Undergraduate Thesis
Depositing User:	Fikri Yudhistira Ajiwijaya
Date Deposited:	27 Jan 2026 08:47
Last Modified:	27 Jan 2026 08:47
URI:	http://repository.its.ac.id/id/eprint/130422

Actions (login required)

View Item