Pengkodean batasan 1-dari-n untuk pemecah SAT

Saya menggunakan pemecah SAT untuk menyandikan masalah, dan sebagai bagian dari contoh SAT, saya memiliki variabel boolean $x_1,x_2,\dots,x_n$ mana dimaksudkan bahwa salah satu dari ini harus benar dan sisanya harus salah. (Saya terkadang melihat ini digambarkan sebagai pengkodean "satu-panas".)

Saya ingin menyandikan batasan "tepat satu dari $x_1,\dots,x_n$ harus benar" di SAT. Apa cara terbaik untuk menyandikan batasan ini, untuk membuat pemecah SAT berjalan seefisien mungkin?

Saya dapat melihat banyak cara untuk menyandikan batasan ini:

• Kendala berpasangan. Saya dapat menambahkan batasan berpasangan $\neg x_i \lor \neg x_j$ untuk semua $i,j$ untuk memastikan bahwa paling banyak satu $x_i$ adalah benar, dan kemudian menambahkan $x_1 \lor x_2 \lor \cdots \lor x_n$ untuk memastikan bahwa setidaknya satu benar.

  Ini menambahkan $\Theta(n^2)$ klausa dan tidak ada variabel boolean tambahan.

• Pengkodean biner. Aku bisa memperkenalkan $\lg n$ variabel boolean baru $i_1,i_2,\dots,i_{\lg n}$ untuk mewakili (dalam biner) integer $i$ sehingga $1 \le i \le n$ (menambahkan beberapa kendala boolean untuk memastikan bahwa $i$ berada dalam kisaran yang diinginkan ). Lalu, saya dapat menambahkan kendala menegakkan bahwa $x_i$ adalah pohon dan bahwa semua lainnya $x_j$ 's adalah palsu. Dengan kata lain, untuk setiap $j$ , kami menambahkan klausa yang menyatakan bahwa $i=j \Leftrightarrow x_j$ .

  Ini menambahkan $\Theta(n \lg n)$ klausa dan saya tidak tahu berapa banyak variabel boolean tambahan.

• Hitung jumlah nilai sebenarnya. Saya dapat mengimplementasikan pohon rangkaian boolean adder dan mensyaratkan bahwa $x_1+x_2+\dots+x_n=1$ , memperlakukan masing-masing $x_i$ sebagai 0 atau 1 sebagai ganti false atau true, dan menggunakan transformasi Tseitin untuk mengubah sirkuit ke SAT klausa. Pohon setengah-adders sudah mencukupi: membatasi output carry masing-masing setengah-penambah menjadi 0, dan membatasi output akhir dari setengah-penambah akhir di pohon menjadi 1. Pohon dapat dipilih dari segala bentuk ( pohon biner seimbang, atau tidak seimbang, atau apa pun).

  Ini dapat dilakukan di gerbang dan dengan demikian menambahkan Θ ( n ) klausa dan Θ ( n ) variabel boolean baru.$\Theta(n)$$\Theta(n)$$\Theta(n)$

  Kasus khusus dari pendekatan ini adalah untuk memperkenalkan variabel boolean , dengan gagasan bahwa y i harus berisi nilai x 1 ∨ x 2 ∨ ⋯ ∨ x i . Maksud ini dapat ditegakkan dengan menambahkan klausa y i ∨ ¬ x i , y i ∨ ¬ y i - 1 , dan ¬ y i ∨ x i ∨ y i $y_1,\dots,y_n$$y_i$$x_1 \lor x_2 \lor \cdots \lor x_i$$y_i \lor \neg x_i$$y_i \lor \neg y_{i-1}$ (di mana kami memperlakukan y 0 sebagai sinonim untuk false) untuki=1,…,n. Selanjutnya, kita dapat menambahkan batasan¬ y i ∨¬ x i + 1 untuki=1,2,…,n-1. Ini pada dasarnya setara dengan transformasi Tseitin dari pohon setengah-penambah, di mana pohon tersebut memiliki bentuk yang tidak seimbang secara maksimal.$\neg y_i \lor x_i \lor y_{i-1}$$y_0$$i=1,\dots,n$$\neg y_i \lor \neg x_{i+1}$$i=1,2,\dots,n-1$

• Jaringan kupu-kupu. Saya dapat membangun jaringan kupu - kupu pada bit, membatasi input n- bit menjadi 000 ⋯ 01 , membatasi output n- bit menjadi x 1 x 2 ⋯ x n , dan memperlakukan setiap gerbang kupu-kupu 2-bit sebagai gerbang independen yang bertukar atau tidak menukar inputnya dengan keputusan yang harus dilakukan berdasarkan variabel boolean baru yang dibiarkan tidak dibatasi. Lalu, saya bisa menerapkan transformasi Tseitin untuk mengubah rangkaian ke klausa SAT.$n$$n$$000\cdots 01$$n$$x_1 x_2 \cdots x_n$

  Ini membutuhkan gerbang dan dengan demikian menambahkan Θ ( n lg n ) klausa dan Θ ( n lg n ) variabel boolean baru.$\Theta(n \lg n)$$\Theta(n \lg n)$$\Theta(n \lg n)$

Apakah ada metode lain yang saya abaikan? Yang mana yang harus saya gunakan? Adakah yang menguji ini atau mencobanya secara eksperimental, atau adakah yang punya pengalaman dengan semua ini? Apakah jumlah klausa dan / atau jumlah variabel boolean baru metrik stand-in yang baik untuk memperkirakan dampak ini pada kinerja pemecah SAT, atau jika tidak, metrik apa yang akan Anda gunakan?

Saya hanya melihat bahwa jawaban ini memiliki beberapa referensi tentang menegakkan kendala kardinalitas untuk SAT, yaitu, menegakkan kendala yang tepat keluar dari n variabel adalah benar. Jadi, pertanyaan saya sampai pada kasus khusus di mana k = 1 . Mungkin literatur tentang batasan kardinalitas akan membantu menjelaskan pertanyaan saya.$k$$n$$k=1$

Untuk kasus khusus k dari n variabel true di mana k = 1, ada pengkodean variabel komandan seperti yang dijelaskan dalam Pengkodean CNF yang Efisien untuk Memilih Objek 1 ke N oleh Klieber dan Kwon. Sederhana: Bagilah variabel menjadi kelompok-kelompok kecil dan tambahkan klausa yang menyebabkan status variabel komandan menyiratkan bahwa sekelompok variabel semuanya salah atau semuanya salah. Kemudian secara rekursif menerapkan algoritma yang sama untuk variabel komandan. Pada akhir proses, tuntutan bahwa salah satu dari segelintir variabel komandan akhir benar. Hasilnya adalah O (n) klausa baru dan O (n) variabel baru.

Mengingat keberadaan dua literal yang ditonton dalam pemecah berbasis DPLL, saya pikir pertumbuhan klausa O (n) adalah keuntungan yang menentukan atas skema pengkodean yang akan menambah lebih banyak klausa.

Sebuah makalah karya Magnus Björk menjelaskan dua teknik yang layak untuk dicoba.

Untuk 1-out-of- , seseorang dapat menggunakan pengkodean satu-panas dan biner secara bersamaan. Jadi, kita memiliki x 1 , ... , x n sebagai pengkodean satu-panas, dan y 1 , ... , y b sebagai pengkodean biner, di mana b = lg n . Kita dapat mengkodekan batasan "setidaknya satu" dengan mudah, dalam satu klausa tunggal: ( x 1$n$$x_1,\dots,x_n$$y_1,\dots,y_b$$b = \lg n$ . Kita juga bisa memaksa dua pengkodean agar konsisten dengan 2 lg $(x_1 \lor \dots \lor x_n)$$2 \lg n$klausa: kita hanya menambahkan atau x $x_i \implies \neg y_j$ , berdasarkan apakahbit j dari pengkodean biner dari i adalah 0 atau 1. Akhirnya, batasan "paling banyak" mengikuti secara otomatis. Ini juga memungkinkan sisa instance SAT untuk menggunakan pengkodean mana pun yang lebih nyaman.$x_i \implies y_j$$j$$i$

$k$$n$$x_1,\dots,x_n$$y_1,\dots,y_n$$y_k$$y_{k+1}$$O(n \lg^2 n)$$O(n \lg^2 n)$

Kertas itu

Magnus Björk. Teknik Penyandian SAT yang Berhasil . 25 Juli 2009.

$n$$k$$n$

Alan M. Frisch, Paul A. Giannaros. Pengodean SAT dari At-Most-k Constraint: Some Old, Some New, Some Fast, Some Slow . ModRef 2010.