Existe uma classe natural de fórmulas de CNF - de preferência uma que tenha sido previamente estudada na literatura - com as seguintes propriedades:
- é um caso fácil de SAT, como, por exemplo, Horn ou 2-CNF, ou seja, a associação empode ser testada em tempo polinomial e as fórmulaspodem ser testadas quanto à satisfação em tempo polinomial.F ∈ C
- As fórmulas insatisfatórias não são conhecidas por terem refutações de resolução curtas (tamanho polinomial) em árvore. Ainda melhor seria: existem fórmulas insatisfatórias em para as quais é conhecido um limite inferior super-polinomial para resolução semelhante a uma árvore.C
- Por outro lado, as fórmulas insatisfatórias em são conhecidas por terem provas curtas em algum sistema de prova mais forte, por exemplo, em resolução semelhante a dag ou em algum sistema ainda mais forte.
n n ∈ N não deve ser muito esparso, ou seja, conter muitas fórmulas com variáveis, para todos (ou pelo menos para a maioria dos valores de) . Também deve ser não trivial, no sentido de conter fórmulas satisfatórias e também insatisfatórias.
A abordagem a seguir para resolver uma fórmula arbitrária CNF deve ser significativa: encontre uma atribuição parcial na fórmula residual em e aplique o algoritmo de tempo polinomial para fórmulas em a . Portanto, eu gostaria de outras respostas além das restrições totalmente diferentes da resposta atualmente aceita, pois acho raro que uma fórmula arbitrária se torne uma restrição totalmente diferente após a aplicação de uma restrição.α F α C C F α
fonte
Respostas:
Parece que você está interessado em diferentes restrições (e sua última frase está no caminho certo). Essas são instâncias não triviais do princípio do buraco de pombo, em que o número de pombos não é necessariamente maior que o número de buracos e, além disso, alguns pombos podem ser barrados em alguns dos buracos.
Restrições diferentes podem ser decididas combinando em tempo polinomial de ordem baixa.
Quando restrições diferentes são expressas (usando uma das várias codificações) como instâncias SAT, o aprendizado de cláusulas orientadas a conflitos geralmente encontra rapidamente uma solução, se existir. No entanto, a resolução pura para o PHP precisa criar um conjunto de cláusulas superpolinomialmente grandes para mostrar que a instância é insatisfatória. Esse limite claramente se aplica a esse problema mais geral. Por outro lado, lembre-se de que a codificação do PHP por Cook permite a extensão estendida de tamanho polinomial refutações de resolução .
Um trabalho recente nesse sentido é o Capítulo 5 de tese Sergi Oliva , que formou a base de um trabalho com Alberto Atserias no CCC 2013.
Espero que você esteja ciente do resultado clássico de Cook, então talvez você pretenda restringir o poder do sistema de provas em sua terceira condição?
fonte
Não sei por que alguém exigiria também fórmulas sat, mas existem alguns artigos sobre a separação entre a resolução Geral e a Árvore, por exemplo [1]. Parece-me que é isso que você quer.
[1] Ben-Sasson, Eli, Russell Impagliazzo e Avi Wigderson. "Perto da separação ideal entre resolução de árvore e resolução geral". Combinatorica 24.4 (2004): 585-603.
fonte
Você pode estar interessado em fórmulas SAT com pequena "largura de banda" (logarítmica) ou "largura de árvore". Essas fórmulas são particionáveis recursivamente de tal maneira que o limite de comunicação entre partições é pequeno e, portanto, uma abordagem de programação dinâmica enumerativa pode ser usada para resolvê-las. O tópico foi popular nos anos noventa. Certa vez, contei exatamente o número de ciclos hamiltonianos em um pequeno gráfico de largura de árvore de 24.000 vértices; portanto, os problemas de # P com pequena largura de árvore também são solucionáveis. Bodlaender é uma referência importante.
fonte
este artigo a seguir parece próximo ao que é solicitado de algumas maneiras (se não se encaixar, talvez JJ possa esclarecer o porquê). a pergunta quer descartar instâncias PHP (pigeonhole) com base na falta de fórmulas verdadeiras / falsas, mas (conforme citado nas outras respostas) PHP é um dos geradores de casos / instâncias mais bem estudados do lado da teoria e tem sempre foi um gerador de fórmulas satisfatórias / insatisfatórias, embora as fórmulas satisfatórias sejam menos enfatizadas / estudadas.
outra abordagem seria seguir um ângulo mais empírico e apenas gerar instâncias aleatórias (presumivelmente em torno do ponto de transição satisfatório fácil-difícil-fácil 50%) e filtrá-las para atender aos critérios estabelecidos. seria necessário implementar implementações de resolução em árvore / resolução DAG ou "sistemas mais fortes".
fonte