Solusi Pendekatan SAT Problem dengan Jaringan Syarf Tiruan Model Learning Vector Quantization

Abstract

Boolean Satisfiability Probelm atau yang sering disingkat dengan SAT Problem merupakan suatu masalah yang menentukan sebuah formula matematika bernilai satisfiable atau unsatisfiable. Sebuah perangkat lunak bagi solusi untuk permasalah SAT disebut dengan SAT Solver. Banyak ilmuan yang mencoba membuat SAT Solver ini menggunakan bermacam-macam metode, salah satunya yaitu, Jaringan Syaraf Tiruan (JST). Sejak dikenalkan pada tahun 1991, JST terus mengalami perkembangan setiap waktu. JST ini memiliki banyak model, namum pada tulisan ini menggunakan JST model Learning Vector Quantization (LVQ). Masukan dari sistem yang akan dibangun ini berupa formula matematika dengan format Conjunctive Normal Form (CNF), kemudian luarannya berupa sebuah kata satisfiable atau unsatisfiable.  Bahasa pemograman Python yang merupakan bahasa pemograman tingkat tinggi akan digunakan untuk membangun sistem.