Teknik Analisis Berbasis SAT/SMT : Teori dan Aplikasi
Abstrak :
Dengan semakin berkembangnya teknologi SAT/SMT solvers, maka teknik analisis menggunakan SAT/SMT solvers juga semakin banyak diadopsi dan diterapkan di berbagai bidang, seperti verifikasi perangkat lunak/keras, analisis statik, perencanaan dan penjadwalan. Permasalahan-permasalahan tersebut memiliki persamaan dalam hal bisa dimodelkan menggunakan persamaan logika dan diberi istilah umum sebagai constraint satisfaction problems atau permasalahan yang harus memenuhi batasan-batasan tertentu. Makalah ini mengulas secara singkat dasar teori pemecahan masalah tersebut menggunakan prinsip satisfiability dan beberapa contoh aplikasinya untuk memecahkan masalah nyata
1 Pendahuluan
Propositional logic atau logika proposisional telah dikenal selama berabad-abad sebagai salah satu landasan penting dalam pemikiran filosofi dan matematika. Dalam perjalanannya, formalisasi logika proposisional ke dalam aljabar Boolean secara bertahap disertai dengan sejumlah besar problem kombinatorial yang dapat dinyatakan sebagai problem propositional satisfiability (SAT). Karena dua peran inilah, SAT berkembang menjadi disiplin ilmu lintas bidang yang cukup matang. Dan SAT juga menjadi permasalahan acuan dalam teori kompleksitas [1]. Banyak contoh permasalahan nyata yang dimodelkan sebagai problem SAT menggunakan berbagai teknik pemodelan. Seperti misalnya, problem verifikasi perangkat lunak/keras, perencanaan, penjadwalan dan perancangan gerbang kombinatorial.
2 Constraint-satisfaction Problems
Dalam bagian ini, akan dibahas definisi constraint-satistaction problems serta dua tipe problem satisfiability, yaitu propositional satisfiability atau SAT (Bagian 2.1) dan satisfiability modulo theories atau SMT (Bagian 2.2)
2.1 Propositional Satisfiability (SAT)
Dalam problem propositional satisfiability atau SAT, solusi yang ingin dicapai adalah menentukan apakah sebuah formula yang tersusun atas variabel Boolean dan operator logika, dapat bernilai benar dengan memilih nilai benar/salah untuk semua variabelnya.
2.2 Satisfiability Modulo Theories (SMT)
Berbeda dengan SAT, SMT merupakan problem untuk menentukan keterpenuhan formula yang berisi teori tingkat pertama yang dapat dihitung. SMT muncul karena banyak ditemukan problem satisfiability di dunia nyata yang tidak mampu ditangkap sepenuhnya oleh SAT [5]. Contoh teori yang muncul dalam SMT adalah Equality and Uninterpreted Functions, Difference logic, array dan Bit vectors.
3 Memecahkan Teka-teki Einstein
Untuk lebih memahami persoalan seperti apakah yang dapat domodelkan dan diselesaikan menggunakan SMT, maka dibagian ini akan diulas bagaimana cara memodelkan teka-teki Einstein sebagai problem SMT.
4 Contoh Aplikasi SAT/SMT
Contoh penyelesaian teka-teki yang disampaikan di bagian sebelumnya, merupakan contoh mainan dan sederhana untuk memahami bagaimana cara memodelkan permasalahan ke dalam problem SMT. Tentu ada banyak permasalahan nyata di dunia nyata yang lebih kompleks dan bisa dipecahkan menggunakan SMT solvers.
4.1 Verifikasi Perangkat Lunak
Dalam proses pembuatan sebuah program komputer atau perangkat lunak. Programmer pada satu titik perlu melakukan pengujian apakah program yang dibuat sudah sesuai dengan yang diinginkan? Apakah terdapat bug di dalam program tersebut?
4.2 Perencanaan
Bayangkan dalam sebuah perusahaan jasa pengiriman barang, yang berusaha untuk menjalankan bisnis dengan optimal. Optimal di sini bisa diartikan mengirim barang sebanyak-banyaknya dengan biaya bahan bakar serendah-rendahnya.