SAT Solver dengan DPLL dalam Pemrograman Deklaratif

Abstract

SAT Solver adalah perangkat lunak untuk
menyelesaikan SAT Problem. Penelitian ini bertujuan
membangun SAT Solver dengan konsep pemrograman deklaratif
dan bahasa pemrograman Prolog dengan menggunakan
Algoritma DPLL. Penelitian ini merupakan bagian dari penelitian
tentang sistem eksplorasi Formal Context dengan constraint.
Setelah pengujian, dapat disimpulkan bahwa SAT Solver dari
penelitian ini dapat menyelesaikan SAT Problem. Salah satu
problem yang diujikan adalah problem Sudoku, yang dinyatakan
dalam SAT Problem dengan 729 variabel dan paling sedikit 8829
klausa.