Memahami kinerja pemecah SMT QFBV

Pemecah SMT seperti Z3 atau Boolector menggunakan serangkaian heuristik yang kompleks untuk menyelesaikan masalah. Namun, ini juga membuat memprediksi kinerja pemecah masalah seperti itu sangat sulit. Pertanyaan saya adalah:

Pertanyaan

Apakah ada cara untuk memahami atau mendapatkan wawasan tentang kinerja pemecah SMT untuk spesifik dalam teori bitvektor bebas-kuantifier (QFBV)?

Ini juga termasuk alat visualisasi yang akan membantu untuk memahami di mana pemecah "macet" / tidak membuat kemajuan.

Aplikasi

• Pahami sebelumnya bagaimana pengkodean yang berbeda dari masalah yang sama mempengaruhi kinerja pemecah (keadaan seni di sini tidak bisa "coba saja beberapa pengkodean yang berbeda dan berharap satu cukup cepat", kan?)

• Jika masalah yang diberikan tidak dapat dipecahkan oleh SMT solver karena keterbatasan waktu, temukan cara untuk mengekspresikan masalah secara berbeda sehingga dapat diselesaikan.

• Hindari membuang waktu pada penyederhanaan masalah khusus domain yang tidak akan mempengaruhi kinerja solver sama sekali atau bahkan berdampak negatif pada kinerja solver.

Penelitian yang ada

Saya mencoba mencari penelitian tentang topik ini, tetapi saya belum dapat menemukan banyak. Saya belum memiliki banyak pengalaman di bidang pemecah SAT / SMT, jadi minta maaf jika saya melewatkan sesuatu.

• SATzilla : memprediksi pemecah kinerja terbaik berdasarkan fitur yang diekstraksi dari masalah menggunakan teknik pembelajaran mesin.

  Ini hanya berlaku dengan SAT bukan SMT, dan tidak menjelaskan alasan kinerja pemecah.

• Aksioma profiler Z3 Visualisasi grafik instantiasi Z3 dan analisis loop yang cocok

  Sepertinya ini hanya berfokus pada teori-teori kuantitatif.

Jawaban singkatnya adalah tidak, kami tidak memahaminya. Jawaban panjangnya adalah ya, kami memiliki beberapa batasan, tetapi batasan itu tidak terlalu membantu. Sudah cukup jelas bahwa waktu menjalankan kasus terburuk adalah eksponensial. Itu tidak terlalu membantu, karena kita tahu bahwa dalam beberapa / banyak situasi praktis, tampaknya berjalan cukup cepat - dan kita tidak benar-benar tahu mengapa.

Kami tidak tahu mengapa itu berlaku untuk pemecah SAT, apalagi untuk QFBV. Memahami mengapa pemecah QFBV seringkali cepat tampaknya setidaknya sama sulitnya dengan memahami mengapa pemecah SAT sering cepat, yang sudah di luar tingkat pemahaman kita saat ini. Jika Anda mencari lebih banyak di situs ini, Anda dapat menemukan ringkasan dari upaya saat ini untuk memahami topik yang terakhir.