Pemecah SAT memberikan cara yang ampuh untuk memeriksa validitas rumus boolean dengan satu quantifier.
Misalnya, untuk memeriksa validitas , kita dapat menggunakan pemecah SAT untuk menentukan apakah memuaskan. Untuk memeriksa validitas , kita bisa menggunakan SAT solver untuk menentukan apakah memuaskan. (Di sini adalah vektor variabel boolean, dan adalah rumus boolean.)
Pemecah QBF dirancang untuk memeriksa validitas formula boolean dengan jumlah penjumlah yang berubah-ubah.
Bagaimana jika kita memiliki rumus dengan dua bilangan? Apakah mereka merupakan algoritma yang efisien untuk memeriksa validitas: yang lebih baik daripada hanya menggunakan algoritma generik untuk QBF? Untuk lebih spesifik saya memiliki rumus bentuk (atau ), dan ingin memeriksa validitasnya. Apakah ada algoritma yang bagus untuk ini? Sunting 4/8: Saya mengetahui bahwa kelas formula ini kadang-kadang dikenal sebagai 2QBF, jadi saya mencari algoritma yang bagus untuk 2QBF.
Mengkhususkan lebih lanjut: Dalam kasus khusus saya, saya memiliki rumus bentuk yang validitasnya ingin saya periksa, di mana f , g adalah fungsi yang menghasilkan output k -bit. Apakah ada algoritma untuk memeriksa validitas formula khusus ini, lebih efisien daripada algoritma generik untuk QBF?
PS Saya tidak bertanya tentang kekerasan kasus terburuk, dalam teori kompleksitas. Saya bertanya tentang algoritma yang praktis berguna (seperti pemecah SAT modern praktis berguna pada banyak masalah meskipun SAT adalah NP-lengkap).
Jawaban:
Jika saya dapat, secara terang-terangan, mengiklankan diri saya, kami menulis sebuah artikel tentang Algoritma Berbasis Abstraksi tahun lalu ini untuk 2QBF . Saya punya implementasi untuk qdimacs, yang bisa saya berikan jika Anda mau tetapi dari pengalaman saya, orang bisa mendapat manfaat besar dari spesialisasi algoritma untuk masalah tertentu. Ada juga makalah yang lebih tua, A Comparative Study of 2QBF Algorithms , yang juga menyajikan algoritma yang cukup mudah ditembus.
sumber
Saya telah membaca dua makalah terkait dengan ini, satu khusus terkait dengan 2QBF. Makalah-makalahnya adalah sebagai berikut:
Penentuan Bertambah, Markus N. Rabe dan Sanjit Seshia, Teori dan Aplikasi Pengujian Kepuasan (SAT 2016).
Mereka telah mengimplementasikan algoritme mereka dalam alat bernama CADET . Gagasan dasarnya adalah menambahkan batasan baru secara bertahap ke rumus hingga batasan menggambarkan fungsi Skolem yang unik atau sampai tidak ada yang dikonfirmasi.
Yang kedua adalah Incremental QBF Solving , Florian Lonsing dan Uwe Egly.
Diimplementasikan dalam alat bernama DepQBF . Itu tidak menempatkan kendala atas jumlah pergantian kuantifier. Ini dimulai dengan asumsi bahwa kita memiliki formula qbf yang terkait erat. Ini didasarkan pada pemecahan bertahap dan tidak membuang klausa yang dipelajari selama penyelesaian terakhir. Itu menambahkan klausa dan kubus ke rumus saat ini dan berhenti baik jika klausa atau kubus kosong, mewakili unsat atau sat.
Edit : Hanya untuk perspektif seberapa baik pendekatan ini bekerja untuk tolok ukur 2QBF. Silakan lihat Hasil QBFEVal-2018 untuk hasil kompetisi QBF tahunan QBFEVAL . Pada 2019 tidak ada trek 2QBF.
Jadi kedua pendekatan ini benar-benar bekerja sangat baik dalam praktiknya (setidaknya pada tolok ukur QBFEVAL).
sumber
sumber