Houve alguma pesquisa sobre -SAT acima do limite de satisfação?

25

Uma característica bem conhecida das instâncias -SAT é a razão do número de cláusulas sobre o número de variáveis , ou seja, o quociente . Para cada , existe um valor limite st \ para , a maioria das instâncias é satisfatória e para maioria das instâncias não é satisfatória. Tem havido uma série de pesquisas feitas para problemas onde , e por problemas com suficientemente pequeno ,kmnρ=m/nkαραραραρk-SAT torna-se solucionável em tempo polinomial. Veja, por exemplo, o artigo de pesquisa de Dimitris Achlioptas do Handbook of Satisfiability ( PDF ).

Gostaria de saber se algum trabalho foi feito na outra direção (onde ), por exemplo, se podemos de alguma forma transformar o problema de CNF para DNF, neste caso, para resolvê-lo rapidamente.ρα

Então, essencialmente, o que se sabe sobre SAT em que ?ρ=m/nα

Matt Groff
fonte
10
Vale a pena notar que é uma função de k . αk
Huck Bennett
poderia haver alguma transformação que mostre algum tipo de simetria entre as duas regiões nos dois "lados" do ponto de transição? parece plausível. de qualquer forma, a questão é bastante amplo no sentido há muito empírica / estudo teórico do ponto de transição que não concentrar tanto em um "lado" ou o outro ...
vzn

Respostas:

26

Sim, houve. Moshe Vardi recentemente deu uma palestra de pesquisa no workshop BIRS Theoretical Foundations of Applied SAT Solving :

(Moshe apresenta o gráfico do experimento um pouco depois do minuto 14:30 em sua palestra acima.)

Seja a razão da cláusula. À medida que o valor de ρ aumenta além do limite, o problema se torna mais fácil para os solucionadores de SAT existentes, mas não tão fácil quanto era antes de atingir o limite. Há um aumento muito acentuado da dificuldade quando nos aproximamos do limiar a partir de baixo. Após o limiar, o problema se torna mais fácil comparado ao limiar, mas a diminuição da dificuldade é muito menos acentuada.ρρ

Seja denotado a dificuldade do problema em relação a n (no experimento T ρ ( n ) é o tempo médio de execução do GRASP em instâncias aleatórias do 3SAT com a razão de cláusulas ρ ). Moshe sugere que T ρ ( n ) muda da seguinte forma:Tρ(n)nTρ(n)ρTρ(n)

  • o limiar: T ρ ( n ) é polinomial em n ,ρTρ(n)n
  • está próximo do limiar: T ρ ( n ) é exponencial em n ,ρTρ(n)n
  • o limiar: T ρ ( n ) permanece exponencial em n, mas o expoente diminui à medida que ρ aumenta.ρTρ(n)nρ
Kaveh
fonte
1
Deve-se notar que os resultados acima são experimentais (a partir de 2000) usando um SAT-solver específico (GRASP). Mas, teoricamente, sabe-se que, para grandes valores (digamos, Ω ( n ) ), até a resolução apresenta pequenas refutações de insatisfação. E, como Jan Johannsem escreveu antes, refutar o 3-SAT já é fácil (no caso médio) quando ρ = Ω ( ρΩ(n). ρ=Ω(n)
Idd Tzameret
19

Existem pelo menos duas linhas de pesquisa relativas a aleatório para fórmulas com uma razão de cláusula / variável maior que o limite de satisfação:k-SAT

  • Para tais fórmulas, foram apresentados limites mais baixos no comprimento das refutações na resolução e sistemas de prova proposicionais mais fortes, começando com o artigo " Muitos exemplos concretos de resolução " de Chvátal e Szemerédi. Esses limites inferiores da resolução implicam limites inferiores no tempo de execução dos solucionadores SAT baseados em DPLL e CDCL. Os limites inferiores mais fortes são para o cálculo polinomial, devido a Ben-Sasson e Impagliazzo .
  • Para essas fórmulas, existem algoritmos determinísticos eficientes para certificar a insatisfação, ou seja, algoritmos que emitem "UNSAT" ou "Não sei", onde a resposta "UNSAT" é necessária para estar correta e deve gerar "UNSAT" em fórmulas insatisfatórias com alta probabilidade. Os resultados mais fortes nessa direção se devem a Feige e Ofek .
Jan Johannsen
fonte
Talvez valha a pena notar que Chvátal / Szemerédi mostra que whp uma fórmula -SAT aleatória com m / n c 1 é insatisfatória. Feige e Ofek dar um algoritmo espectral quando m / n c 2 n 1 / 2 . Portanto, resta um km/nc1m/nc2n1/2 lacuna entrec1nec2n 3 / 2 , onde quase todas as fórmula é insatisfatível, mas não sabemos como decidir que isto é assim. nc1nc2n3/2
András Salamon
2

Aqui está um estudo / ângulo mais antigo, mas relevante, de um especialista líder.

ele mostra o parâmetro estima o número de soluções e mede a "restrição" e correlaciona / tendências aproximadamente com a razão de cláusula para variável. veja p3 fig 4 em particularκ

Na figura 4, plotamos a restrição estimada no ramo heurístico para problemas aleatórios de 3-SAT. Para L / N <4,3, os problemas são sub-restritos e solúveis. À medida que a pesquisa avança, diminui à medida que os problemas se tornam mais restritos e obviamente solúveis. Para L / N> 4.3, os problemas são excessivamente restritos e insolúveis. À medida que a pesquisa avança, κ aumenta à medida que os problemas se tornam mais restritos e obviamente insolúveis.κκ

a pergunta pergunta sobre . mas, a partir da análise empírica, isso é altamente confinado e, portanto, basicamente se aproxima de instâncias do tempo P (um solucionador "descobre" rapidamente que são insolúveis)) e, portanto, não é tão teórico quanto interessante (porque não "eliciam / exercitam" o tempo exponencial comportamento dos solucionadores em média). no entanto, pessoalmente, não vi trabalhos / transformações / teorias que provam isso mais teoricamente / rigorosamente (além deste artigo como um começo disso).m/nα

vzn
fonte
por outro lado, é presumivelmente possível gerar instâncias "rígidas" individuais de qualquer m / n "dimensão", é apenas que elas são menos prováveis ​​estatisticamente fora da transição de fase "P-NP-P".
vzn