Tugasnya adalah menulis kode yang dapat menemukan formula logis kecil untuk jumlah bit.
Tantangan keseluruhan adalah untuk kode Anda untuk menemukan formula logis proposisional sekecil mungkin untuk memeriksa apakah jumlah variabel biner 0/1 sama dengan beberapa nilai x. Biarkan kami memanggil variabel x1, x2, x3, x4 dll. Ekspresi Anda harus sama dengan jumlah. Artinya, rumus logis harus benar jika dan hanya jika jumlahnya sama dengan x.
Ini adalah cara naif untuk melakukannya sejak awal. Katakan y = 15 dan x = 5. Pilih semua 3003 cara yang berbeda untuk memilih 5 variabel dan untuk masing-masing membuat klausa baru dengan DAN dari variabel-variabel tersebut DAN dan dari negasi dari variabel yang tersisa. Anda berakhir dengan 3003 klausa yang masing-masing panjangnya tepat 15 dengan total biaya 45054.
Jawaban Anda harus berupa ekspresi logis dari jenis yang hanya dapat disisipkan ke python, katakanlah, jadi saya bisa mengujinya. Jika dua orang mendapatkan ekspresi ukuran yang sama, kode yang menjalankan kemenangan tercepat.
Anda diizinkan untuk memperkenalkan variabel baru ke dalam solusi Anda. Jadi dalam hal ini rumus logis Anda terdiri dari variabel biner y, x dan beberapa variabel baru. Seluruh rumus akan memuaskan jika dan hanya jika jumlah variabel y sama dengan x.
Sebagai latihan awal beberapa orang mungkin ingin memulai dengan y = 5 variabel menambahkan ke x = 2. Metode naif kemudian akan memberikan biaya 50.
Kode harus mengambil dua nilai y dan x sebagai input dan output rumus dan ukurannya sebagai output. Biaya solusi hanyalah hitungan mentah variabel dalam outputnya. Jadi (a or b) and (!a or c)
diperhitungkan sebagai 4. Satu-satunya operator yang diizinkan adalah and
, or
dan not
.
Pembaruan Ternyata ada metode pintar untuk menyelesaikan masalah ini ketika x = 1, setidaknya secara teori.
sumber
z[0] = y[0] and y[1]
, bagaimana Anda ingin ini ditunjukkan?z[0]
mewakiliy[0] or y[1]
maka saya hanya perlu memperkenalkan klausa yang terlihat seperti(y[0] or y[1]) or not z[0]
(atau pernyataan yang setara menggunakan 3 operator diperbolehkan).Jawaban:
Python, 644
Generator persamaan rekursif sederhana.
S
menghasilkan persamaan yang puas jika daftarvars
tambah hinggatotal
.Ada beberapa perbaikan nyata yang harus dilakukan. Misalnya, ada banyak subekspresi umum yang muncul di keluaran 15/5.
Menghasilkan:
sumber
not x[0] and not x[1] and not x[2]
muncul 5 kali dalam ekspresi 15/5.Saya ingin berkomentar, tapi saya tidak punya reputasi. Saya ingin berkomentar bahwa hasil pengkodean Kwon & Klieber (dikenal sebagai "Komandan") untuk k = 1 telah digeneralisasi untuk k> = 2 oleh Frisch et al. "SAT Encodings dari At-Most-k Constraint." Apa yang Anda tanyakan adalah kasus khusus dari batasan AM-k, dengan klausa tambahan untuk menjamin At-Least-k, yang sepele, hanya keterputusan semua variabel dengan batasan AM-k. Frisch adalah peneliti terkemuka dalam pemodelan kendala, jadi saya akan merasa nyaman menyarankan bahwa [(2k + 2 Ck + 1) + (2k + 2 C k-1)] * n / 2 adalah batas terbaik yang diketahui pada jumlah klausa diperlukan, dan k * n / 2 untuk jumlah variabel baru yang akan diperkenalkan. Detailnya ada dalam makalah yang dikutip, bersama dengan instruksi bagaimana pengkodean ini dibuat. Itu' Cukup mudah untuk menulis sebuah program untuk menghasilkan formula ini, dan saya pikir solusi seperti itu akan bersaing dengan solusi lain yang mungkin Anda temukan untuk saat ini. HTH.
sumber