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 e a cláusula 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 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 . Dizemos dizer que é é satisfatório.
O problema que estou sugerindo é o seguinte: considere duas CNFs e , e deixar que o CNF
Qual é a relação de com e ?
O limite superior óbvio é . Isso é apertado?
fonte
Respostas:
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 ) .UMA BEu WUMA B B WB max ( wUMA, 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.
fonte