Posting blog Scott Aaronson hari ini memberikan daftar masalah / tugas terbuka yang menarik dalam kompleksitas. Seseorang khususnya menarik perhatian saya:

Bangun perpustakaan umum dengan instance 3SAT, dengan sesedikit mungkin variabel dan klausa, yang akan memiliki konsekuensi penting jika diselesaikan. (Misalnya, contoh yang mengkode tantangan anjak piutang RSA.) Selidiki kinerja pemecah SAT terbaik saat ini di perpustakaan ini.

Ini memicu pertanyaan saya: Apa teknik standar untuk mengurangi masalah RSA / anjak menjadi SAT, dan seberapa cepat itu? Apakah ada pengurangan standar seperti itu?

Untuk memperjelas, dengan "cepat", saya tidak bermaksud waktu polinomial. Saya bertanya-tanya apakah kita memiliki batas atas yang lebih ketat pada kompleksitas pengurangan. Misalnya, apakah ada pengurangan kubik yang diketahui?

Salah satu pendekatan untuk mengkodekan Factoring (RSA) ke SAT adalah dengan menggunakan sirkuit multiplikator (Setiap sirkuit dapat dikodekan sebagai CNF).

Mari kita asumsikan kita diberi integer dengan 2 n bit, C = ( c 1 , c 2 , ⋯ , c 2 n ) 2 . Kami tertarik dalam menemukan dua n -bit bilangan bulat A = ( a 1 , ⋯ , sebuah n ) dan A = ( b 1 , ⋯ , b n ) yang produknya adalah C = A $C$$2n$$C=(c_1,c_2,\cdots,c_{2n})_2$$n$$A=(a_1,\cdots,a_n)$$A=(b_1,\cdots,b_n)$ .$C=A*B$

Pengkodean yang paling naif bisa seperti ini: Kita tahu itu

c 2 n - 1 = ( a n ∧ b n - 1 ) x o r ( a n - 1 ∧ b n ) C a r r y : d 2 n - 1 = ( a n ∧ b n - 1 ) ∧ ( a

Kemudian menggunakan transformasi Tseitin, pengkodean di atas dapat diterjemahkan ke dalam CNF.

Pendekatan ini menghasilkan CNF yang relatif kecil. Tetapi pengkodean ini tidak mendukung "Unit Propagation" dan karenanya, kinerja SAT Solver benar-benar buruk.

Ada sirkuit lain untuk perkalian yang dapat digunakan untuk tujuan ini, tetapi mereka menghasilkan CNF yang lebih besar.

Memperluas apa yang ditulis oleh @Amir, saya menemukan halaman web bagus berikut yang meng-host generator CNF untuk sirkuit anjak yang dapat dijalankan misalnya pada beberapa nomor RSA Factoring Challenge (sekarang tidak aktif) . Mesin virtual yang dihasilkan dalam format DIMACS yang dapat langsung diumpankan ke salah satu pesaing saat ini dalam kompetisi pemecah SAT tahunan . Mengenai contoh-contoh SAT yang sulit secara umum, masalah tolok ukur yang diberikan pada situs kompetisi SAT tampaknya cukup berguna, juga klasifikasi ke dalam acak / buatan / industri bagus.

Berikut ini makalah tentang menghasilkan instance SAT dari anjak piutang:

Horie, S. & Watanabe, O. [1997] " Pembuatan instance yang keras untuk SAT " Algoritma dan Komputasi 1350: 22-31 ( pdf )

$n^2$

ToughSat oleh Henry Yuen dan Joseph Bebel adalah alat lain yang mirip dengan yang ditautkan oleh @Martin, yang menghasilkan rumus CNF yang menyandikan contoh anjak piutang dan masalah-masalah sulit lainnya.

Lihat satfactor:

Ubah Integer Factorization menjadi masalah KEPUASAN boolean

Shane Neph

Ikhtisar

Faktor-faktor penentu bilangan bulat besar telah menarik bagi Manusia sejak setidaknya waktu Euclid. Tidak ada algoritma umum yang diketahui untuk masalah ini yang menskala dalam waktu kurang dari eksponensial sehubungan dengan jumlah bit yang diperlukan untuk mewakili integer.

Apa yang dilakukan kode ini

Mengubah masalah faktorisasi bilangan bulat menjadi masalah KEPUASAN boolean. Jika masalah dipecahkan oleh pemecah SAT, itu kemudian mengekstrak faktor integer.

Pemecah kepuasan Boolen meningkat setiap tahun. Setiap 2 tahun, sebuah kompetisi internasional antar pemecah terjadi (lihat http://www.satcompetition.org/ dan http://www.satlive.org/ ). Seberapa baik pemecah yang canggih ini dapat melawan salah satu masalah matematika terbuka tertua yang ada?

Proyek ini memiliki 2 tujuan utama:
1) Konversi masalah dan faktor bilangan bulat minat!
2) Dengan cepat membuat masalah KEPUASAN terpecahkan atau tidak terpecahkan, yang kesulitannya mudah dikendalikan oleh creater.
- Untuk membuat masalah KEPUASAN tidak terpecahkan, cukup enkode bilangan prima.
- Untuk menciptakan masalah yang lebih sulit tetapi bisa dipecahkan, pilih angka komposit yang lebih besar dengan lebih sedikit faktor.

Jumlah bunga mungkin berapa pun jumlahnya!

Ada beberapa pemecah KEPUASAN sumber terbuka. Lihat http://www.satlive.org/ untuk beberapa di antaranya.

Membangun

make -C src /

Bagaimana-Untuk

Masukkan sejumlah minat dalam bentuk binernya:

bin / iencode 10101> composite.21
// selesaikan dengan solver favorit Anda dan masukkan hasilnya di solution.txt
bin / extract-sat composite.21 solution.txt

Outputnya adalah:
00011
00111

yang merupakan representasi biner untuk bilangan bulat desimal 3 dan 7, faktor 21.

Jika integer input memiliki lebih dari 2 faktor, dan masalah SAT diselesaikan, output akan menjadi dua faktor saja. Ini mungkin bukan bilangan prima (Anda bisa menguji dengan mudah di Maxima, Maple, atau Mathematica).

Tidak semua keluaran SAT solver menghasilkan dalam format yang sama. Anda mungkin perlu sedikit memeriksakan hasilnya. ekstrak-sat membutuhkan file solusi yang berisi daftar bilangan bulat (pada sejumlah baris). Sebagai contoh,

1 -2 3 4 -5 ...