Classes bem conhecidas de fórmulas booleanas que exigem provas de resolução exponencialmente longas

Muitas vezes, é possível encontrar métodos de plano de corte, propagação variável, ramificação e encadernação, aprendizado de cláusulas, retrocesso inteligente ou até heurísticas humanas tecidas à mão nos solucionadores SAT. No entanto, há décadas os melhores solucionadores de SAT contam com técnicas de prova de resolução e usam uma combinação de outras coisas simplesmente para obter ajuda e direcionar a pesquisa no estilo de resolução. Obviamente, suspeita-se que QUALQUER algoritmo falhará ao decidir a questão da satisfação no tempo polinomial em pelo menos alguns casos.

Em 1985, Haken provou em seu artigo "A intratabilidade da resolução" que o princípio do buraco do pombo codificado na CNF não admite provas de resolução de tamanho polinomial. Embora isso prove algo sobre a intratabilidade de algoritmos baseados em resolução, também fornece critérios pelos quais os solucionadores de ponta podem ser julgados - e, de fato, uma das muitas considerações que são necessárias para projetar um solucionador SAT hoje é como é provável que ele tenha desempenho em casos conhecidos 'difíceis'.

Ter uma lista de classes de fórmulas booleanas que admitem comprovadamente provas de resolução de tamanho exponencial é útil no sentido em que fornece fórmulas "difíceis" para testar novos solucionadores de SAT. Que trabalho foi feito na compilação de tais classes? Alguém tem uma referência que contenha essa lista e suas provas relevantes? Por favor, liste uma classe de fórmula booleana por resposta.

Instâncias rígidas para resolução :

1. Fórmulas de Tseitin (sobre gráficos expansores).

2. Princípio fraco ( a n ) do pombo (exponencial em n limites inferiores, para qualquer m > n ).$m$$n$$n$$m>n$

3. Aleatória de 3CNF com variáveis e S ( N de 1,5 - ε ) cláusulas, para 0 < ε < 1 / 2 .$n$$O(n^{1.5-\epsilon})$$0<\epsilon<1/2$

Pesquisa técnica boa e relativamente atualizada para os limites inferiores da complexidade da prova, consulte:

Nathan Segerlind: A complexidade das provas proposicionais. Boletim de Lógica Simbólica 13 (4): 417-481 (2007) disponível em: http://www.math.ucla.edu/~asl/bsl/1304/1304-001.ps

Existem várias pesquisas e livros bons sobre a complexidade da prova proposicional que contêm essas listas. Muitos sistemas de prova simulam p-resolução, portanto, qualquer fórmula que seja difícil para eles será difícil para resolução.

Livros:
1. Jan Krajicek, "Aritmética limitada, lógica proposicional e teoria da complexidade", 1995
2. Stephen A. Cook e Phoung The Neguyen, "Fundamentos lógicos da complexidade da prova", 2010

Pesquisas:
1. Paul Beame e Toniann Pitassi, "Complexidade da prova proposicional: passado, presente e futuro", 2001
2. Samuel R. Buss, "Complexidade aritmética e de prova proposicional limitada", 1997
3. Alasdair Urquhart, "A complexidade da provas proposicionais ", 1995

Veja também os listados aqui e aqui .

$2n \times 2n$$2\times 1$

Michael Alekhnovich. O problema do tabuleiro de xadrez mutilado é exponencialmente difícil de resolver. Teórico Compututer Science 310 (1-3): 513-525 (2004). http://dx.doi.org/10.1016/S0304-3975(03)00395-5

$n\to (k)^2_2$$k=\lfloor \frac12 \log n \rfloor$$\bigvee_{i,j\in K} x_{i,j}$$\bigvee_{i,j\in K} \neg x_{i,j}$$K\subseteq \{ 1 , \ldots , n \}$$|K| = k$

Há uma construção na página 9 deste artigo de Groote e Zantema .

O DIMACS não mantém conjuntos de amostras de instâncias SAT rígidas? Eu não consegui encontrá-lo lá apenas com um olhar superficial, mas se você digitar "SAT" na caixa de pesquisa dele, serão exibidos muitos hits, incluindo vários artigos / palestras sobre instâncias difíceis do SAT.