Twierdzenie o bezpośredniej sumie dla złożoności przestrzeni klauzuli rozdzielczości?

Rozwiązanie to program mający na celu wykazanie niezadowalającej wartości CNF. Dowodem na rozwiązanie jest logiczne odjęcie pustej klauzuli dla klauzul początkowych w CNF. W szczególności każdy punkt początkowy można wywnioskować, i dwóch punktach i klauzula można wywnioskować, jak również. Odrzucenie jest sekwencją dedukcji, która kończy się pustą klauzulą. $A \lor x$ $B \lor \neg{x}$ $A \lor B$

Jeśli takie odrzucenie zostanie wdrożone, możemy rozważyć procedurę, która zachowa niektóre klauzule w pamięci. W przypadku, gdy klauzula nieinicjalna musi zostać użyta ponownie i nie ma jej już w pamięci, algorytm powinien ją ponownie od zera lub z pamięci zapisanych w pamięci.

Niech $Sp(F)$ najmniejszą liczbę klauzul, które należy zachować w pamięci, aby osiągnąć puste klauzule. To się nazywa przestrzeń klauzula złożoność $F$ . Mówimy, że $Sp(F)=\infty$ to $F$ jest zadowalające.

Problem, który sugeruję, jest następujący: rozważmy dwa CNF $A=\bigwedge_{i=1}^m A_i$ i $B=\bigwedge_{j=1}^n B_j$ , i pozwólmy 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$

Jaki jest stosunek do i ? $Sp(A \lor B)$ $Sp(A)$ $Sp(B)$

Oczywista górna granica to . Czy to jest ciasne? $Sp(A \lor B) \leq Sp(A) + Sp(B) -1$

— MassimoLauria
źródło

Dobre pytanie! Czy znasz odpowiedź na wielkość kwoty bezpośredniej? Myślę, że najgorszym przypadkiem jest sytuacja, gdy A i B nie mają wspólnych zmiennych. Ciekawym przypadkiem może być sytuacja, gdy A i B są takie same do zmiany nazwy zmiennej. Przy okazji, nie rozumiem, jak uzyskać tę górną granicę, wydaje się, że może być znacznie gorzej.

— Kaveh

Teraz widzę górnej granicy, można skopiować odrzucenia przez

dla

dostać

pojedynczo dla każdego

, a następnie wykonaj odrzucenia dla

. Rozmiar będzie wynosił około

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,

Masz rację. Zapomniałem o tym wspomnieć, ale oczywiście najciekawszym przypadkiem pod względem dolnej granicy jest to, że A i B nie dzielą zmiennych. To jest właśnie przypadek Jestem rzeczywiście interesują. Biorąc pod uwagę inny A i B jest lepiej indukcyjnie uzyskać wynik dla

gdzie

są rozłączne kopie zmiennych tego samego

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,

Zauważ, że jeśli chodzi o długość obalenia, łatwo masz

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,

Górna granica trywialnej przestrzeni wymaga w rzeczywistości o jedną klauzulę mniejszą. Zredagowałem odpowiednio.

— MassimoLauria,

Chciałem opublikować to jako komentarz, ale ponieważ nie jestem w stanie dokładnie wymyślić, jak to zrobić, wydaje mi się, że będzie to raczej „odpowiedź”.

Zgadzam się, że pytanie jest miłe. Oczywiście to samo pytanie można również zadać o długość odrzucenia rozdzielczości (tj. Liczbę klauzul występujących w odrzuceniu, liczoną z powtórzeniami) i szerokość odrzucenia (tj. Rozmiar lub liczbę literałów występujących w , największa klauzula odrzucenia).

We wszystkich tych przypadkach istnieją „oczywiste” górne granice, ale nie jest dla mnie jasne, czy należy oczekiwać dopasowania dolnych granic, czy nie. Dlatego chciałem dodać jedno pytanie i jeden komentarz.

Pytanie dotyczy długości odrzucenia. Wydaje się rozsądne, aby sądzić, że granica długości określona w komentarzu Massimo jest ścisła, ale czy wiemy o tym?

$A$ $B_i$ $w_A$ $B$ $B$ $w_B$ $\max (w_A, w_B)$

Jest to oczywiście łatwa obserwacja, ale chodzi o to, że może to wskazywać, że pytanie o przestrzeń może być trudne. Jest tak, ponieważ prawie wszystkie dolne granice przestrzeni w obaleniu wiemy, że przechodzą przez dolne granice szerokości. (Oznacza to, że dolne granice przestrzeni zostały wyprowadzone niezależnie, ale z perspektywy czasu wszystkie one są następstwem pięknego artykułu „Kombinatoryjna charakterystyka szerokości rozdzielczości” autorstwa Atseriasa i Dalmau.) Ale jeśli istnieje bezpośrednie twierdzenie o sumie dla klauzuli rozdzielczości przestrzeni, nie będzie wynikać z dolnych granic szerokości, ale trzeba się z nią bezpośrednio spierać, co przynajmniej do tej pory wydawało się znacznie trudniejsze. Ale oczywiście może istnieć jakiś łatwy argument, którego mi brakuje.

— Jakob Nordstrom
źródło

Witaj, Jakob!

— arnab

Komentarze są niestety ograniczone do osób o reputacji co najmniej 50 - jest to osobliwość oprogramowania i dotyczy zapobiegania spamowi. Jestem pewien, że szybko przekroczysz ten próg.

— Suresh Venkat

Cześć Jakob, miło cię tu widzieć. (ps: Myślę, że przekroczyłeś próg).

— Kaveh

Cześć Jakob, zastanawiam się, czy tego rodzaju oświadczenie ma jakieś konsekwencje w odniesieniu do kompromisów. Jako technika o niższych granicach, która nie byłaby bardzo potężnym narzędziem: długość formuły zostaje podniesiona do kwadratu, podczas gdy przestrzeń zwiększa się liniowo. W każdym razie ta właściwość może prowadzić do formuły o małej szerokości i dużej przestrzeni (zwróć uwagę, że szerokość również rośnie, jeśli wykonano nie stałą liczbę powtórzeń).

— MassimoLauria,