Qual é a correlação entre a largura da árvore e a dureza da instância para o 3-SAT aleatório?

11

Este artigo recente do FOCS2013, Strong Backdoors to Bounded Treewidth SAT de Gaspers e Szeider, fala sobre o vínculo entre a largura da árvore do gráfico da cláusula SAT e a dureza da instância.

Para instâncias aleatórias de 3-SAT, ou seja, 3-SAT escolhidas aleatoriamente, qual é a correlação entre a largura da árvore do gráfico de cláusulas e a dureza da instância?

A "dureza da instância" pode ser considerada "difícil para um solucionador SAT típico", ou seja, o tempo de execução.

Estou procurando respostas ou referências de estilo teórico ou empírico. Que eu saiba, não parece haver estudos empíricos sobre isso. Estou ciente de que existem maneiras um pouco diferentes de criar gráficos de cláusulas SAT, mas esta questão não está focada na distinção.

Talvez uma questão natural e intimamente relacionada seja como a largura da árvore do gráfico de cláusulas se relaciona com a transição de fase 3-SAT.

vzn
fonte

Respostas:

10

Não é realmente uma resposta, mas as referências mais próximas que conheço. Existem resultados disponíveis para a largura da ramificação. Além disso, há pelo menos um estudo empírico da largura da árvore de instâncias industriais.

Vijay D
fonte
7

Em geral, não se espera que instâncias aleatórias do SAT tenham uma largura de árvore limitada, mesmo que sejam fáceis. Aqui está um exemplo:

Uma instância aleatória do k-SAT em variáveis ​​em que cada variável ocorre em cláusulas será um gráfico de expansão e, portanto, terá uma largura de árvore com alta probabilidade. Isso vale no modelo em que fixamos um n e um m (com 3n = km) e escolhemos uniformemente aleatoriamente uma fórmula com n variáveis ​​e cláusulas m, de modo que todas as variáveis ​​estejam exatamente em 3 cláusulas. Ele também se aplica ao modelo de Erdős – Rényi com conjunto de probabilidades, para que as variáveis ​​tenham grau médio .3 θ ( n ) 3n3θ(n)3

Por outro lado, essa densidade está bem abaixo da transição de fase k-SAT; pelo lema local de Lovasz todas as instâncias regular -SAT são satisfatórias para , ou seja, quandok 4 1dkd2k412kdk1d2k4k

Para a outra parte da sua pergunta, eu esperaria (mas eu não testei isso, então eu realmente não sei) que os solucionadores de SAT sejam capazes de explorar pelo menos algumas das simetrias que ocorrem devido a todos os separadores balanceados em um gráfico de largura de árvore delimitada: em uma instância k-SAT de largura de árvore há um conjunto de variáveis ​​de tamanho para que, após você ramificar essas variáveis, a fórmula se divida em componentes conectados com menos de variáveis ​​em cada uma.t n / 2ttn/2

daniello
fonte
thx para idéias. ofc não esperava que instâncias aleatórias tivessem limitado a largura da árvore; o oposto é presumivelmente comprovável sem muita dificuldade. mas é um parâmetro numérico que pode ser comparado / correlacionado com a dureza de maneira semelhante a muitos outros parâmetros estudados na pesquisa de pontos de transição empíricos do SAT e que alguma relação ou correlação parece ser esperada com base nas pesquisas existentes.
vzn
@vzn Meu argumento é mais do que nos modelos aleatórios mais comuns, a largura da árvore passa pelo telhado antes que as instâncias se tornem computacionalmente difíceis. Por outro lado, as instâncias da `` vida real '' provavelmente têm uma largura de árvore muito menor do que as aleatórias e eu meio que espero que os solucionadores de SAT tirem (algumas) vantagens disso.
Daniello 22/10