ETH: k-SAT vs. SAT?

8

Seja SAT o idioma das instâncias do SAT que contêm variáveis , seja -SAT o idioma das instâncias do SAT nas quais todas as cláusulas têm no máximo k literais, e deixe k -SAT _v ser sua interseção. Seja s_k = \ inf_M \ {\ delta \ mid \ existe c \ forall v \; (M \ text {decide} k \ text {-SAT $ _v $ in} 2 ^ {v \ delta-c}) \ text { time}) \} , onde o mínimo varia sobre todos os algoritmos (máquinas em algum modelo de computação). Deixe s_ \ infty = \ lim_ {k \ to \ infty} s_kv[v]={0 0,1,,v-1}kkkvs = lim k s ksk=infM{δcv(M decide k-SENTOUv no 2vδ-c) Tempo)}s=limksk. Para que isso faça sentido, é necessário assumir que existe um limite razoável para o tamanho da entrada em termos do número de variáveis; caso contrário, pode-se repetir cláusulas para forçar sk e s a serem tão grandes quanto desejado. Portanto, assuma que as cláusulas não são repetidas.

Observe que cada fórmula k -CNF possui tamanho no máximo O(vk) , portanto, o tamanho da fórmula de entrada não é importante quando se considera um expoente linear em v . Segue-se que s3s4s .

A hipótese de tempo exponencial (ETH) é a afirmação de que sk>0 0 para alguns k3 . A sequência (sk) aumenta infinitamente com frequência se ETH for válido. O forte ETH (SETH) é a declaração que s1 ou s=1 , dependendo da referência usada.

Por outro lado, cada instância do SAT v contém até 3v cláusulas distintas (cada variável pode ser positiva, negativa ou ausente em cada cláusula). Portanto, uma entrada pode ter comprimento Ω(2nregistro3) mesmo que nenhuma cláusula seja repetida; portanto, esse é um limite inferior para o tempo de leitura da entrada e também para o tempo total.

Se então permitirmos que , é claro que apenas considerando os tamanhos de entrada. Mesmo se alguém exigir que uma fórmula de entrada não contenha nenhuma cláusula incluída por outra, . Pelo algoritmo trivial, também é o caso de .s ωlog 3 > 1,58 s ω1,5 s ω1 + log 3sω=infM{δcv(M decide SENTOUv no 2vδ-c) Tempo)}sωregistro3>1,58sω1.5sω1+registro3

Por que existe uma lacuna entre e , assumindo SETH?s ωssω

Em certo sentido, é apenas uma maneira diferente de atingir o limite, então parece intrigante que haja uma lacuna.sω

  • Russell Impagliazzo e Ramamohan Paturi, Sobre a complexidade de SATk , JCSS 62 367–375, 2001. doi: 10.1006 / jcss.2000.1727 ( pré-impressão )
  • Evgeny Dantsin e Alexander Wolpert, em tempo moderadamente exponencial para o SAT , SAT 2010, LNCS 6175 313–325. doi: 10.1007 / 978-3-642-14186-7_27 ( pré-impressão )
  • Chris Calabro, Russell Impagliazzo e Ramamohan Paturi, A complexidade da satisfação de pequenos circuitos de profundidade , IWPEC 2009, LNCS 5917 75–85. doi: 10.1007 / 978-3-642-11269-0_6 ( pré-impressão )
  • Marek Cygan, Holger Dell, Daniel Lokshtanov, Dániel Marx, Jesper Nederlof, Yoshio Okamoto, Ramamohan Paturi, Saket Saurabh, Magnus Wahlström, Em problemas tão difíceis quanto CNF-SAT , arXiv: 1112.2275v3 , 27 de março de 2014.
András Salamon
fonte

Respostas:

6

A diferença entre suas definições é que a largura da cláusula em pode crescer com o número de variáveis, enquanto que para é arbitrariamente grande, mas constante.s sωs

É um problema semelhante ao PH vs PSPACE. Se você fizer um número constante arbitrário de alterações no quantificador, obterá a hierarquia polinomial, mas se permitir que a fórmula seja totalmente quantificada, ocorrerá um problema completo no PSPACE.

Stefan Schneider
fonte
4

Uma maneira melhor de definir esses expoentes é se você perguntar sobre o tempo de execução no formato , em que é um polinômio arbitrário do tamanho da entrada. Em seguida, artefatos como o tamanho desaparecem.p o l y ( | F | ) 3 vcnpoeuy(|F|)poeuy(|F|)3v

Hirsch
fonte
Parece uma abordagem sensata, motivada por complexidade parametrizada. No entanto, os trabalhos que tratam da ETH parecem deixá-la bastante vaga ou usam uma definição que é essencialmente a que forneço acima. Você tem um ponteiro?
András Salamon
Quando falamos sobre k-SAT, isso não importa, porque o tamanho da fórmula é polinomial no número de variáveis. Com relação aos ponteiros, veja, por exemplo, como Impagliazzo, Paturi e Zane definem a classe SE em "Quais problemas têm complexidade fortemente exponencial?", Journal of Computer and System Sciences 63, 512-530 (2001).
Hirsch
Obrigado, isso é útil; Anteriormente, apenas me concentrei realmente no lema da Sparsificação desse trabalho.
András Salamon