Saya membaca di Wikipedia bahwa penyatuan adalah proses penyelesaian masalah kepuasan.
Pada saat yang sama, saya tahu bahwa pemecah seperti itu disebut "pemecah SAT" atau "pemecah SMT". Jadi, apakah mereka berbeda nama untuk hal yang sama?
Jika Anda mengatakan bahwa mereka berbeda, harap tunjukkan kesalahan dalam perawatan saya.
Jawaban:
Pemecah SAT memecahkan Masalah Kepuasan Boolean . Ini adalah "masalah menentukan apakah variabel formula Boolean yang diberikan dapat ditugaskan sedemikian rupa untuk membuat rumus tersebut dievaluasi menjadi TRUE."
Contohnya adalah menemukan penugasan nilai kebenaran pada variabel sedemikian rupa sehingga ( a ∨ b ∨ c ) ∧ ( ¬ a ∨ ¬ b ∨ c ) ∧ ( a ∨ ¬ b ∨ ¬ c ) ∧ ( ¬ a ∨ b ∨ ¬ c ) benar. Seorang pemecah SAT dapat mengembalikan solusi seperti a = t r u e ,a,b,c (a∨b∨c)∧(¬a∨¬b∨c)∧(a∨¬b∨¬c)∧(¬a∨b∨¬c) a=true , c = t r u e .b=true c=true
Pemecah SMT memecahkan masalah yang lebih umum, yaitu Modulo Teori Kepuasan . Ini adalah "masalah keputusan untuk formula logis sehubungan dengan kombinasi teori latar belakang yang dinyatakan dalam logika orde pertama klasik dengan kesetaraan". Teori-teori ini dapat mencakup "teori bilangan real, teori bilangan bulat, dan teori berbagai struktur data seperti daftar, array, vektor bit, dan sebagainya."
Contoh, diberikan variabel yang diketik dan y : i n t dan f : i n t → i n t , menanyakan apakah yang berikut adalah f ( x + 2 ) ≠ f ( y - 1 ) ∧ x = ( y - 4 ) memuaskan. Seorang pemecah SMT akan menjawab ya, dengan solusi x = - 2 , yx:int y:int f:int→int f(x+2)≠f(y−1)∧x=(y−4) x=−2 , f ( 0 ) = 1
dan f ( 1 ) = 3 .y=2 f(0)=1 f(1)=3
Unifikasi adalah teknik khusus yang membutuhkan dua istilah dan menemukan substitusi yang akan membuat istilah itu sama. Sebagai contoh, diberikan istilah dan b o o k ( D. ~ Smith , y , 2010 ) , unifikasi akan menghasilkan substitusi { x ↦ D. Smith , y ↦ "Fishing" } . Unifikasi kemungkinan digunakan di dalam pemecah SMT.book(x,"Fishing",2010) book(D.~Smith,y,2010) {x↦D. Smith,y↦"Fishing"}
sumber