Pemecah untuk menemukan titik-titik tetap dari sistem boolean
Intro: Masalahnya
Masalah saya berkaitan dengan memecahkan sistem persamaan yang menemukan titik tetap dari sistem boolean yang dipelajari ($F(X)=X$).
Contoh Sederhana
Membiarkan $\bar{x}=\{x_1,x_2,x_3\} \in \{0,1\}$menjadi beberapa variabel boolean yang menarik. Membiarkan$F=\{f_1,f_2,f_3\}$menjadi fungsi pembaruan untuk variabel-variabel ini (mis$x_i(t+1) = f_i(x(t))$), didefinisikan sebagai fungsi kondisi berikut (mereka didasarkan pada input dari setiap variabel - node dalam konseptualisasi grafik yang sesuai):
$f_1 = \begin{cases} 1, -x_2 \ge 0 \\ 0, \text{otherwise} \end{cases}$, $f_2 = \begin{cases} 1, x_1-x_3 \ge 0 \\ 0, \text{otherwise} \end{cases}$, $f_3 = \begin{cases} 1, x_1+x_3 \ge 0 \\ 0, \text{otherwise} \end{cases}$
Fungsi-fungsi ini terinspirasi oleh pertanyaan ini .
Tujuannya adalah untuk menemukan set jawaban $\bar{x}$ (bisa nol, satu atau banyak per se) yang untuknya $F(\bar{x})=\bar{x}$.
Contoh di atas tentu saja merupakan kasus yang sangat sederhana. Pada akhirnya saya ingin menyelesaikan sistem persamaan seperti itu dengan ratusan variabel. Perhatikan bahwa fungsi kondisi akan selalu berupa kombinasi linier dari setiap input variabel dan variabel selalu boolean .
Pertanyaan
Saya membutuhkan pemecah yang efisien untuk masalah semacam ini (yang dikenal sebagai NP-hard btw!). Misalnya apakah masalah ini dapat dirumuskan sebagai pemrograman kendala dan diselesaikan dengan menggunakan teknik Answer Set Programming (ASP)?
Jawaban
Jadi ternyata ASP bisa digunakan untuk mengatasi masalah ini! Di sini saya memberikan kemungkinan pengkodean masalah dalam file bernama fp.lp:
% variables
var(1..3).
% functions
% f(Function,Coefficient,Variable)
f(1,-1,2).
f(2,1,1).
f(2,-1,3).
f(3,1,1).
f(3,1,3).
% guess assignment to variables
{ init(V) : var(V) }.
% compute functions
next(F) :- var(F), #sum { C,V : f(F,C,V), init(V) } >= 0.
% check if fixed point
:- init(V), not next(V).
:- next(V), not init(V).
#show next/1.
#show init/1.
Menggunakan clingo(versi 5.4.0) dari baris perintah: clingo fp.lpkami mendapatkan TIDAK PUAS untuk contoh khusus ini.
Mengomentari fakta %f(2,1,1).dan menjalankan kembali clingopemecah yang kami dapatkan:
Answer: 1
next(3) init(1) init(3) next(1)
SATISFIABLE
Variabel yang dikembalikan baik dalam predikat init/1dan next/1diterjemahkan ke variabel boolean aktif (1) dan variabel yang hilang ke nilai tidak aktif (0). Hasil yang dikembalikan dengan demikian adalah vektor boolean$\bar{x}=\{x_1=1,x_2=0,x_3=1\}$.
Penghargaan untuk jawaban ini diberikan kepada Roland Kaminski. Berbagai anggota komunitas potassco ASP lainnya memberikan komentar dan solusi yang membantu. Untuk info lebih lanjut tentang ASP, periksa:https://potassco.org/