Um teorema de soma direta para a complexidade do espaço da cláusula Resolution?

10

A resolução é um esquema para provar a insatisfação dos CNFs. Uma prova na resolução é uma dedução lógica da cláusula vazia para as cláusulas iniciais do CNF. Em particular qualquer cláusula inicial pode ser inferida, e a partir de dois cláusulas Ax e B¬x a cláusula AB pode ser deduzida como bem. Uma refutação é uma sequência de deduções que termina com uma cláusula vazia.

Se essa refutação for implementada, podemos considerar um procedimento que mantém algumas cláusulas na memória. Caso uma cláusula não inicial precise ser usada novamente e não esteja mais na memória, o algoritmo deve fazê-lo novamente do zero ou daqueles na memória.

Deixe Sp(F) o menor número de cláusulas a serem mantidas na memória para alcançar as cláusulas vazias. Isto é chamado o espaço cláusula complexidade da F . Dizemos dizer que Sp(F)= é F é satisfatório.

O problema que estou sugerindo é o seguinte: considere duas CNFs A=i=1mAi e B=j=1nBj , e deixar que o CNF

AB=i=1mj=1nAiBj

Qual é a relação de Sp(AB) com Sp(A) e Sp(B) ?

O limite superior óbvio é Sp(AB)Sp(A)+Sp(B)1 . Isso é apertado?

MassimoLauria
fonte
Boa pergunta! Você sabe a resposta para o tamanho da soma direta? Eu acho que o pior caso é quando o A e o B não possuem variáveis ​​compartilhadas. Um caso interessante pode ser quando A e B são iguais até a renomeação da variável. Aliás, não vejo como você consegue esse limite superior, parece que pode ser muito pior.
Kaveh
Agora vejo o limite superior, você pode copiar a refutação de para A iB j para 1 j n para obter um i , um por um para cada 1 i m e depois fazer a refutação para A . O tamanho será em torno de m . ( S i z e ( B ) + O ( 1 ) ) + S i z e ( A )BAiBj1jnAi1imAm.(Size(B)+O(1))+Size(A).
Kaveh
Você está certo. Esqueci de mencionar isso, mas é claro que o caso mais interessante em termos de limite inferior é quando A e B não compartilham variáveis. Isso é exatamente o caso, eu estou realmente interessado. Considerando diferentes A e B é melhor indutivamente obter um resultado para onde F i são disjuntos cópias variáveis da mesma F . F1F2FkFiF
MassimoLauria
11
Note-se que em relação comprimento refutação você facilmente ter
Length(AB)Length(B)|A|+Length(A)
MassimoLauria
O limite superior do espaço trivial, na verdade, requer menos uma cláusula na memória. Eu editei de acordo.
MassimoLauria

Respostas:

7

Eu queria postar isso como um comentário, mas como não consigo descobrir o caminho, acho que terá que ser uma "resposta".

Eu concordo que a pergunta é boa. Obviamente, a mesma pergunta também pode ser feita sobre a duração das refutações de resolução (ou seja, o número de cláusulas que ocorrem na refutação, contadas com repetições) e a largura da refutação (ou seja, o tamanho ou o número de literais que ocorrem em , a maior cláusula da refutação).

Em todos esses casos, existem limites superiores "óbvios", mas não está claro para mim se é de esperar que os limites inferiores sejam iguais ou não. Portanto, eu queria adicionar uma pergunta e um comentário.

A questão diz respeito ao comprimento da refutação. Parece razoável acreditar que o limite de duração declarado no comentário de Massimo seja rígido, mas sabemos disso?

E o comentário diz respeito à largura. Observe que, para esta medida, um momento de reflexão revela que um limite inferior de soma direta não se mantém. Para largura, uma vez refuta toda a -Fórmula para cada cláusula B i , de largura w A , digamos, mais a largura do B -Fórmula, e depois um refuta a B -Fórmula de largura w B . Supondo que ambas as fórmulas tenham largura inicial constante, a largura da refutação da soma direta será essencialmente máxima ( w A , w B ) .ABiwABBwBmax(wA,wB)

É claro que é uma observação fácil, mas o ponto é que isso pode indicar que a questão do espaço pode ser complicada. Isso ocorre porque quase todos os limites inferiores no espaço em refutação que conhecemos passam por limites inferiores de largura. (Ou seja, os limites inferiores do espaço foram derivados independentemente, mas em retrospectiva todos eles seguem como corolário do belo artigo "Uma caracterização combinatória da largura da resolução" de Atserias e Dalmau.) Mas se existe um teorema da soma direta para a cláusula de resolução espaço, ele não segue da largura limites inferiores, mas deve ser discutido diretamente, o que pelo menos até agora parece ser muito mais difícil. Mas é claro que pode haver algum argumento fácil que estou perdendo.

Jakob Nordstrom
fonte
2
Bem-vindo, Jakob!
Arnab
11
Infelizmente, os comentários são limitados a pessoas com uma reputação de pelo menos 50 - isso é uma singularidade do software e está relacionado à prevenção de spam. Tenho certeza de que você cruzará esse limiar rapidamente.
precisa saber é o seguinte
Olá Jakob, é um prazer vê-lo aqui. (ps: Eu acho que você passou do limite.)
Kaveh
Olá Jakob, gostaria de saber se esse tipo de declaração tem algumas conseqüências em relação às compensações. Como uma técnica de limite inferior que não seria uma ferramenta muito poderosa: o comprimento da fórmula quadratura enquanto o espaço aumenta linearmente. De qualquer forma, essa propriedade pode levar à fórmula com largura pequena e espaço grande (observe que também a largura aumenta se um número não constante de repetição for feito).
MassimoLauria 17/01