Verifikasi kebenaran penghapusan kuantifier, menggunakan SAT

Membiarkan $x=(x_1,\dots,x_n)$ dan $y=(y_1,\dots,y_n)$ menjadi $n$ -vektor variabel boolean. Saya memiliki predikat boolean $Q(x,y)$ di $x,y$ . Saya memberi teman saya Priscilla $Q(x,y)$ . Sebagai tanggapan, dia memberi saya $P(x)$ , predikat boolean pada $x$ , dan dia mengklaim itu

P (x) \equiv \exists y . Q (x, y),

$P(x) \equiv \exists y . Q(x,y),$

atau dengan kata lain, itu

\forall x . [P (x) \Leftrightarrow \exists y . Q (x, y)] .

$\forall x . [P(x) \Leftrightarrow \exists y . Q(x,y)].$

Saya ingin memverifikasi klaimnya entah bagaimana. Bagaimana Priscilla dapat membantu saya memverifikasi klaim ini?

Anda dapat mengasumsikan keduanya $P$ dan $Q$ direpresentasikan sebagai formula CNF, dan itu tidak terlalu besar (ukuran polinomial, atau sesuatu).

Dalam dunia yang ideal, akan luar biasa jika saya bisa mengurangi masalah memverifikasi klaim ini ke SAT: Saya punya pemecah SAT, dan akan lebih bagus jika saya bisa menggunakan pemecah SAT untuk memverifikasi klaim ini. Namun, saya cukup yakin bahwa tidak mungkin memformulasikan masalah memverifikasi klaim ini secara langsung sebagai instance SAT; menguji validitas formula 2QBF hampir pasti lebih sulit daripada SAT. (Itu $\Leftarrow$ arah mudah dirumuskan sebagai instance SAT, tetapi $\Rightarrow$ arah sulit karena secara inheren melibatkan dua bilangan kuantifikasi.)

Tapi seandainya Priscilla bisa memberi saya beberapa bukti tambahan untuk mendukung klaimnya. Apakah ada beberapa bukti tambahan atau saksi yang bisa diberikan Priscilla kepada saya, yang akan memudahkan saya untuk memverifikasi klaimnya? Secara khusus, apakah ada beberapa bukti atau saksi tambahan yang bisa dia berikan kepada saya, yang akan memudahkan saya untuk merumuskan masalah memverifikasi klaimnya sebagai instance dari SAT (yang kemudian saya dapat menerapkan pemecah SAT saya)?

Salah satu aspek yang tidak biasa dari pengaturan saya adalah bahwa saya berasumsi (heuristik) bahwa saya memiliki oracle untuk SAT. Jika Anda menyukai teori kompleksitas, Anda dapat memikirkannya dengan cara ini: Saya mengambil peran mesin yang dapat menghitung banyak hal $P^{NP}$ (yaitu di $\Delta^P_2$ ), dan saya ingin memverifikasi klaim Priscilla menggunakan algoritme di $P^{NP}$ . Terima kasih saya kepada MDX untuk cara berpikir tentang hal-hal ini.

Motivasi / aplikasi saya: Saya ingin melakukan verifikasi formal terhadap suatu sistem (mis., Pengecekan model simbolik), dan langkah kunci dalam penalaran melibatkan eliminasi quantifier (yaitu, mulai dari $Q$ , dapatkan $P$ ). Saya berharap ada cara bersih untuk memverifikasi bahwa eliminasi quantifier dilakukan dengan benar.

Jika tidak ada solusi yang berfungsi untuk semua kemungkinan $P,Q$ , jangan ragu untuk menyarankan solusi yang "suara tetapi tidak lengkap", yaitu teknik yang bagi banyak orang $P,Q$ izinkan saya memverifikasi kesetaraan yang diklaim. (Bahkan jika gagal memverifikasi klaim pada beberapa $P,Q$ yang memenuhi klaim, saya masih dapat mencoba ini sebagai heuristik, asalkan tidak pernah secara tidak tepat mengklaim telah memverifikasi klaim palsu. Atas suatu pemberian $P,Q$ , mungkin bekerja, atau mungkin tidak; jika tidak berhasil, saya tidak lebih buruk daripada di mana saya mulai.)

logic satisfiability first-order-logic software-verification model-checking DW
sumber

Jika kita memberi Priscilla a

Q (x, y)

$Q(x,y)$ di mana kamu tidak relevan, apakah kita tidak menyelesaikan secara efektif

TAUT \in coNP

$\text{TAUT}\in \text{coNP}$ ? Jika demikian, maka tidak ada sertifikat yang dapat diberikan Priscilla kepada Anda yang dapat membantu kecuali

NP = coNP

$\text{NP}=\text{coNP}$ .

mdxn

@mdx, hal yang aneh tentang pengaturan ini adalah bahwa saya memiliki pemecah SAT, yang (secara empiris) tampaknya hampir selalu bekerja pada predikat yang saya jalankan dalam praktek. Jadi, jika saya diberikan

P (x), Q (x)

$P(x),Q(x)$ dan ingin memverifikasi

\forall x . P (x) \Leftrightarrow Q (x)

$\forall x . P(x) \Leftrightarrow Q(x)$ , Saya bisa memberi makan

(P (x) \land \neg Q (x)) \lor (\neg P (x) \land Q (x))

$(P(x) \land \neg Q(x)) \lor (\neg P(x) \land Q(x))$ ke pemecah SAT saya; jika ternyata ini tidak memuaskan, saya sudah memverifikasi

\forall x . P (x) \Leftrightarrow Q (x)

$\forall x . P(x) \Leftrightarrow Q(x)$ adalah benar. Jadi, meskipun itu pemecahan yang efektif

TAUT

$\text{TAUT}$ , dalam praktiknya masih OK. Atau apakah saya salah memahami inti dari komentar Anda?

Ah, jadi saya menganggap Anda mengambil peran mesin memutuskan masalah masuk

P^{NP} = Δ_{2}^{P}

$\text{P}^\text{NP}=\Delta^P_2$ (atau setara heuristik dari)?

mdxn

@ mdx, ya, sekarang Anda menyebutkannya, itu cara yang bagus untuk memikirkannya. Terima kasih telah menyarankan perspektif itu!

Saya pikir first-order-logictag tidak bisa dibenarkan. Pertanyaannya adalah semua tentang rumus boolean yang dikuantifikasi.

berlutut

Jawaban:

Berikut adalah dua teknik yang dapat saya identifikasi:

Identifikasi fungsi Skolem eksplisit. Misalkan Priscilla dapat mengidentifikasi fungsi eksplisit $f$ seperti yang

$\forall x . P (x) \Leftrightarrow Q (x, f (x))$ $\forall x . P(x) \Leftrightarrow Q(x,f(x))$
memegang. Maka itu mengikuti bahwa klaim Priscilla benar.

Ini berarti Priscilla dapat membantu kami memverifikasi klaimnya dengan menyediakan fungsi $f$ sehingga proposisi di atas berlaku. Kami dapat mengonfirmasi bahwa proposisi di atas berlaku dengan menguji rumus berikut untuk kepuasan:

$\neg (P (x) \Leftrightarrow Q (x, f (x))) .$ $\neg (P(x) \Leftrightarrow Q(x,f(x))).$
Jika formula ini tidak memuaskan, maka klaim Priscilla telah diverifikasi.

Satu peringatan adalah bahwa Priscilla harus dapat mengidentifikasi fungsi yang sesuai $f$ . Peringatan lebih lanjut adalah yang kita butuhkan $f$ untuk dapat direpresentasikan secara konkret dalam beberapa bentuk singkat, katakanlah, sebagai sirkuit boolean berukuran polinomial. Namun, jika kondisi tersebut terpenuhi, maka teknik ini harus bekerja.
Argumen hibrid. Pertimbangkan kasus khusus masalah ini, di mana kita menghitung variabel satu-bit (daripada a $n$ -bit variabel); ternyata masalahnya mudah diselesaikan dalam kasus ini. Ini menunjukkan bahwa kami mencoba untuk menghubungkan teknik itu $n$ kali, setiap kali menghapus satu bit lagi $y$ . Ternyata ide ini terkadang berhasil, tetapi tidak selalu.

Biarkan saya menjelaskan cara memverifikasi klaim Priscilla dalam kasus di mana $y=(y_1)$ adalah variabel satu-bit. Kemudian $\exists y . Q(x,y)$ setara dengan $Q(x,\text{False}) \lor Q(x,\text{True})$ . Rumus terakhir paling banyak dua kali lebih besar dari $Q$ , jadi masih berukuran polinomial. Sekarang kita bisa menggunakan pemecah SAT kita untuk menguji apakah $Q(x,\text{False}) \lor Q(x,\text{True})$ setara dengan $P(x)$ ; kesetaraan berlaku tepat jika rumus berikut tidak memuaskan:

$\neg (P (x) \Leftrightarrow (Q (x, Salah) \lor Q (x, Benar))) .$ $\neg (P(x) \Leftrightarrow (Q(x,\text{False}) \lor Q(x,\text{True}))).$
Jadi, jika kita mengkuantifikasi lebih dari satu bit, ini memberikan cara untuk memverifikasi bahwa penghapusan quantifier dilakukan dengan benar.

Untuk mengatasi masalah asli, terapkan ini beberapa kali. Tugas Priscilla adalah memberi kita $n+1$ predikat boolean $R_0,R_1,R_2,\dots,R_n$ seperti yang

$R_{saya} (x, (y_{saya + 1}, ..., y_{n})) \equiv \exists y_{1}, y_{2}, ..., y_{saya} . Q (x, y) .$ $R_i(x,(y_{i+1},\dots,y_n)) \equiv \exists y_1,y_2,\dots,y_i . Q(x,y).$
Tugas kami adalah memverifikasi apakah semua predikat boolean ini dihasilkan dengan benar. Kita dapat melakukan ini dengan menguji apakah $Q(x,y) \equiv R_0(x,y)$ , $P(x) \equiv R_n(x)$ ,

$R_{i + 1} (x, (y_{i + 2}, \dots, y_{n})) \equiv \exists y_{i + 1} . R_{i} (x, (y_{i + 1}, \dots, y_{n})) for i = 1, 2, \dots, n - 1 .$ $R_{i+1}(x,(y_{i+2},\dots,y_n)) \equiv \exists y_{i+1} . R_i(x,(y_{i+1},\dots,y_n)) \qquad \text{for $i=1,2,\dots,n-1$}.$
Perhatikan bahwa yang terakhir adalah contoh eliminasi kuantifier dengan bit tunggal, jadi kami telah menjelaskan cara mengujinya dengan menggunakan solver SAT. Kami juga dapat menguji apakah $Q \equiv R_0$ dan $P \equiv R$ menggunakan solver SAT dengan mudah. Jadi, kita dapat memeriksa apakah Priscilla dihasilkan $R_0,\dots,R_n$ benar. Jika dia melakukannya, maka kami telah memverifikasi itu $P$ dihasilkan sesuai.

Satu peringatan adalah bahwa Priscilla harus dapat menghasilkan $R_i$ ini Peringatan yang lebih besar adalah bahwa ukuran semua $R_i$ Harus masuk akal (katakanlah, berukuran polinomial). Jika Priscilla menghasilkan $R_i$ Naif, ukuran mereka mungkin tumbuh secara eksponensial dengan $i$ , yang tidak baik. Jadi, Priscilla akan membutuhkan cara untuk menyederhanakan di setiap tahap; perlu ada beberapa urutan $R_0,\dots,R_n$ yang semuanya berukuran polinomial, dan Priscilla harus dapat menemukan urutan seperti itu. Itu sama sekali tidak dijamin. Yang mengatakan, jika Priscilla dapat melakukan ini, maka teknik ini akan berhasil.

Saya tidak sepenuhnya puas dengan teknik ini - mereka heuristik tidak lengkap, dan mereka mungkin gagal pada beberapa / banyak contoh masalah - jadi saya masih akan tertarik untuk melihat cara-cara lain untuk mendekati masalah ini.

DW
sumber