Teorema jumlah langsung untuk Resolusi ruang klausa kompleksitas?

Resolusi adalah skema untuk membuktikan ketidakpuasan CNF. Bukti dalam resolusi adalah deduksi logis dari klausa kosong untuk klausa awal CNF. Khususnya setiap klausa awal dapat disimpulkan, dan dari dua klausa dan klausa dapat disimpulkan juga. Sangkalan adalah urutan pemotongan yang diakhiri dengan klausa kosong. $A \lor x$ $B \lor \neg{x}$ $A \lor B$

Jika penolakan semacam itu diterapkan, kami dapat mempertimbangkan prosedur yang menyimpan beberapa klausa dalam memori. Dalam hal klausa non-awal harus digunakan lagi dan tidak ada dalam memori lagi, algoritma harus harus lagi dari awal atau dari yang ada di memori.

Biarkan $Sp(F)$ jumlah klausa terkecil untuk disimpan dalam memori untuk mencapai klausa kosong. Ini disebut ruang klausul kompleksitas $F$ . Kami mengatakan bahwa $Sp(F)=\infty$ is $F$ adalah memuaskan.

Masalah yang saya sarankan adalah ini: pertimbangkan dua CNF $A=\bigwedge_{i=1}^m A_i$ dan $B=\bigwedge_{j=1}^n B_j$ , dan biarkan CNF

A \lor B = ⋀_{i = 1}^{m} ⋀_{j = 1}^{n} A_{i} \lor B_{j}

$A \lor B = \bigwedge_{i=1}^m \bigwedge_{j=1}^n A_i \lor B_j$

Apa hubungan $Sp(A \lor B)$ dengan $Sp(A)$ dan $Sp(B)$ ?

Batas atas yang jelas adalah $Sp(A \lor B) \leq Sp(A) + Sp(B) -1$ . Apakah ini ketat?

cc.complexity-theory lo.logic proof-complexity proof-search MassimoLauria
sumber

Pertanyaan bagus! Apakah Anda tahu jawaban untuk ukuran dari jumlah langsung? Saya kira kasus terburuk adalah ketika A dan B tidak memiliki variabel bersama. Kasus yang menarik mungkin ketika A dan B sama dengan mengubah nama variabel. Btw, saya tidak melihat bagaimana Anda mendapatkan batas atas itu, rasanya seperti itu bisa jauh lebih buruk.

Kaveh

Sekarang saya melihat batas atas, Anda dapat menyalin sanggahan untuk untuk untuk untuk mendapatkan satu per satu untuk setiap dan kemudian melakukan sanggahan untuk . Ukurannya akan sekitar .

B

$B$

A_{i} \lor B_{j}

$A_i \lor B_j$

1 \leq j \leq n

$1 \leq j \leq n$

A_{i}

$A_i$

1 \leq i \leq m

$1 \leq i \leq m$

A

$A$

m . (S i z e (B) + O (1)) + S i z e (A)

$m.(Size(B)+O(1))+Size(A)$

Kaveh

Kamu benar. Saya lupa menyebutkan itu, tapi tentu saja kasus yang paling menarik dalam hal batas bawah adalah ketika A dan B tidak berbagi variabel. Itulah kasus Saya benar-benar tertarik. Mengingat yang berbeda A dan B lebih baik induktif mendapatkan hasil untuk mana adalah variabel menguraikan salinan yang sama .

F_{1} \lor F_{2} \lor \dots F_{k}

$F_1 \lor F_2 \lor \ldots F_k$

F_{i}

$F_i$

F

$F$

MassimoLauria

Perhatikan bahwa mengenai panjang sanggahan Anda dengan mudah memiliki

L e n g t h (A \lor B) \leq L e n g t h (B) | A | + L e n g t h (A)

$Length(A \lor B) \leq Length(B)|A|+Length(A)$

MassimoLauria

Batas atas ruang sepele sebenarnya membutuhkan satu klausa yang lebih sedikit dalam memori. Saya mengedit sesuai.

MassimoLauria

Jawaban:

Saya ingin memposting ini sebagai komentar, tetapi karena saya tidak tahu cara melakukannya, saya kira itu harus menjadi "jawaban".

Saya setuju bahwa pertanyaannya bagus. Tentu saja, pertanyaan yang sama juga dapat ditanyakan tentang panjang sanggahan resolusi (yaitu, jumlah klausa yang terjadi dalam sanggahan, dihitung dengan pengulangan) dan lebar sanggahan (yaitu, ukuran, atau jumlah literal yang terjadi dalam , klausa terbesar dalam sanggahan).

Dalam semua kasus ini ada batas atas "jelas", tetapi tidak jelas bagi saya apakah seseorang harus mengharapkan pencocokan batas bawah atau tidak. Karena itu, saya ingin menambahkan satu pertanyaan dan satu komentar.

Pertanyaannya menyangkut panjang sangkalan. Tampaknya masuk akal untuk percaya bahwa ikatan panjang yang dinyatakan dalam komentar oleh Massimo itu ketat, tetapi apakah kita tahu ini?

Dan komentar itu menyangkut lebar. Perhatikan bahwa untuk ukuran ini, saat pemikiran mengungkapkan bahwa jumlah batas bawah langsung tidak berlaku. Untuk lebar, satu malah menolak seluruh formula untuk setiap klausa , dengan lebar , katakanlah, ditambah lebar dari -formula, dan kemudian satu membantah lebar . Dengan asumsi bahwa kedua rumus memiliki lebar awal konstan, lebar sanggahan jumlah langsung akan pada dasarnya . $A$ $B_i$ $w_A$ $B$ $B$ $w_B$ $\max (w_A, w_B)$

Ini tentu saja pengamatan yang mudah, tetapi intinya adalah bahwa itu mungkin menunjukkan bahwa pertanyaan untuk ruang bisa rumit. Ini terjadi karena hampir semua batas bawah pada ruang dalam sangkalan kita tahu tentang pergi melalui batas bawah lebar. (Yaitu, batas bawah ruang diturunkan secara independen, tetapi dengan melihat ke belakang mereka semua mengikuti sebagai akibat wajar dari kertas indah "Karakterisasi Kombinasi Resolusi Lebar" oleh Atserias dan Dalmau.) Tetapi jika ada teorema jumlah langsung untuk klausul resolusi ruang, itu tidak akan mengikuti dari batas bawah lebar tetapi harus diperdebatkan secara langsung, yang setidaknya sejauh ini tampaknya jauh lebih sulit. Tapi tentu saja mungkin ada beberapa argumen mudah yang saya lewatkan.

Jakob Nordstrom
sumber

Selamat datang, Jakob!

arnab

Sayangnya, komentar terbatas pada orang dengan reputasi minimal 50 - ini adalah keanehan dari perangkat lunak dan berkaitan dengan pencegahan spam. Saya yakin Anda akan melewati ambang itu dengan cepat.

Suresh Venkat

Hai Jakob, senang melihatmu di sini. (ps: Saya pikir Anda telah melewati ambang pintu.)

Kaveh

Hai Jakob, saya ingin tahu apakah pernyataan seperti ini memiliki beberapa konsekuensi terkait pertukaran. Sebagai teknik batas bawah yang tidak akan menjadi alat yang sangat kuat: rumus panjang kotak sementara ruang meningkat secara linear. Pokoknya properti ini dapat menyebabkan rumus dengan lebar kecil dan ruang besar (perhatikan bahwa lebar juga tumbuh jika jumlah pengulangan tidak konstan dilakukan).

MassimoLauria