Pengurangan waktu-poli dari ILP ke SAT?

Jadi, seperti diketahui, masalah keputusan 0-1 ILP adalah NP-complete. Menampilkannya dalam NP mudah, dan pengurangan aslinya dari SAT; sejak itu, banyak masalah NP-Lengkap lainnya telah terbukti memiliki formulasi ILP (yang berfungsi sebagai pengurangan dari masalah tersebut ke ILP), karena ILP sangat berguna secara umum.

Pengurangan dari ILP tampaknya jauh lebih sulit untuk dilakukan sendiri atau dilacak.

Jadi, pertanyaan saya adalah, apakah ada yang tahu pengurangan waktu-poli dari ILP ke SAT, yaitu menunjukkan bagaimana menyelesaikan masalah keputusan ILP 0-1 menggunakan SAT?

0-1 ILP diformulasikan sebagai:

Apakah ada vektor , tunduk pada batasan:$\mathbf{x}$

$$\left.\begin{array}{rrrrr|rr} a_{11} x_1 & + &a_{12} x_2 & ... + & a_{1n} x_n\le b_1 \\ a_{21} x_1 & + &a_{22} x_2 & ... + & a_{2n} x_n\le b_2 \\ ...\\ a_{m1} x_1 & + &a_{m2} x_2 & ... + & a_{mn} x_n\le b_m \\ \end{array}\right.$$

Domain x: $\forall_{x_j \in \mathbf{x}} x_j\in \{0,1\}$

Pengurangan ke k-sat:

Perkecil dahulu ke sirkuit sat:

Mulailah dengan baris pertama, membuat variabel boolean untuk mewakili masing-masing bit dalam dan satu variabel boolean untuk x j . Kemudian buat variabel untuk b 1 . Buat sirkuit tambahan (pilih favorit Anda) menambahkan baris ke atas.$a_{1j}$$x_j$$b_1$

Kemudian buat sirkuit perbandingan, nyatakan jumlahnya kurang dari .$b_1$

$a_{1j}$$b_1$

$x_j$

CNF final akan berisi semua kendala.

Ini semacam necro-jawaban untuk pertanyaan yang sudah dijawab dan diterima, tetapi saya ingin mencatat, bahwa ada cara yang lebih mudah.

Pertimbangkan Anda memiliki salah satu ketidaksetaraan seperti ini:

$5*x_1 + 2*x_2 + 3*x_3 \leq 6$

$(1, 1, 1)$$(1, 1, 0)$$(1, 0, 1)$

$(1, 1, 1)$$\neg(x_1 \land x_2 \land x_3)$$(\neg x_1 \lor \neg x_2 \lor \neg x_3)$

$(\neg x_1 \lor \neg x_2 \lor \neg x_3)$$(\neg x_1 \lor \neg x_2 \lor x_3)$$(\neg x_1 \lor x_2 \lor \neg x_3)$

Melintasi semua ketidaksetaraan dan mengumpulkan klausa Anda akan mendapatkan cnf pada akhirnya. Seringkali cnf ini adalah CARA SIMPLER, kemudian satu, yang dihasilkan dari jawaban yang diterima. Biaya lebih sulit pra-pemrosesan.