O SAT de largura limitada é decidível no espaço de logs?

10

Elberfeld, Jakoby e Tantau 2010 ( ECCC TR10-062 ) provaram ser uma versão com eficiência de espaço do teorema de Bodlaender. Eles mostraram que para gráficos com largura de árvore no máximo , pode-se encontrar uma decomposição em árvore da largura usando espaço logarítmico. O fator constante no espaço limitado depende de . (O teorema de Bodlaender mostra um limite linear no tempo, com uma dependência exponencial de no fator constante.)k k kkkkk

O SAT se torna fácil quando o conjunto de cláusulas tem baixa largura. Especificamente, Fischer, Makowsky e Ravve 2008 mostraram que a satisfação das fórmulas de CNF com a largura da árvore do gráfico de incidência delimitada por pode ser decidida com no máximo operações aritméticas quando a decomposição da árvore é dada. Pelo teorema de Bodlaender, o cálculo da decomposição em árvore do gráfico de incidência para fixo pode ser feito em tempo linear e, portanto, o SAT pode ser decidido para fórmulas limitadas de largura de árvore no tempo que é um polinômio de baixo grau no número de variáveis .2 O ( k ) n k nk2O(k)nkn

Pode-se então esperar que o SAT seja realmente decidível usando espaço logarítmico, para fórmulas com largura de árvore limitada do gráfico de incidência. Não está claro como modificar Fischer et al. abordagem para decidir SAT em algo eficiente em termos de espaço. O algoritmo funciona computando uma expressão para o número de soluções, via inclusão-exclusão e avaliando recursivamente o número de soluções de fórmulas menores. Embora a largura da árvore delimitada ajude, as subfórmulas parecem ser muito grandes para serem computadas no espaço logarítmico.

Isso me leva a perguntar:

Sabe-se que SAT para fórmulas de largura de árvore limitada está em ou ?N LLNL

András Salamon
fonte
5
O fato de que SAT em L para instâncias limitadas de largura de árvore não se segue diretamente dos resultados no artigo que você citou? O conjunto de fórmulas satisfatórias é definível pelo MSO. Portanto, a satisfação pode ser resolvida em tempo linear em gráficos de largura de árvore limitada via teoremas de Bodlaender + Courcelle. Elberfeld-Jakoby-Tantau-2010, mostra que as propriedades do MSO podem ser decididas no espaço logarítmico em gráficos de largura de árvore limitada, fornecendo versões espaciais logarítmicas dos teoremas de Bodlaender + Courcelle. Portanto, o SAT pode ser decidido no espaço de logs em gráficos de largura de árvore limitada.
Mateus de Oliveira Oliveira
@MateusdeOliveiraOliveira, os detalhes não me parecem claros. O SAT é definível pelo MSO por meio de uma estrutura com duas relações de arestas direcionadas (Exemplo 2.18 de Immerman), cuja união leva às arestas do gráfico de incidência quando a direção é esquecida. No entanto, não está claro para mim que é possível usar o gráfico de incidência como está para definir a satisfação do MSO (por meio da cobertura do conjunto, por exemplo), de modo a poder aplicar o Bodlaender / Courcelle / EJT.
András Salamon 27/03
@ AndrásSalomon O teorema de Courcelle pode ser indicado para gráficos com vértices e arestas coloridas. A largura da árvore desses gráficos coloridos é igual à largura das versões sem cor. Existem muitas maneiras de modelar estruturas relacionais arbitrárias como gráficos coloridos.
Mateus de Oliveira Oliveira
11
No caso de Fórmulas, você deseja definir uma estrutura relacional que codifique ao mesmo tempo a fórmula e o gráfico de incidência. (caso contrário, como você definiria a satisfação em primeiro lugar?) Então, usando uma noção apropriada de largura de árvore para essa estrutura, temos que a largura de árvore da estrutura (gráfico de Fórmula + Incidência) é no máximo uma constante aditiva maior que a largura de árvore de o gráfico de incidência sozinho. Observe que existem muitas maneiras de definir tais estruturas relacionais combinadas e, essencialmente, cada autor usa a que é mais adequada ao seu contexto.
Mateus de Oliveira Oliveira
@Mateus, obrigado! Esse é um comentário bastante útil; Eu não estava ciente da natureza da "caixa de ferramentas" da largura da árvore em complexidade descritiva. Gostaria de transformar isso em uma resposta?
András Salamon 28/03

Respostas:

10

De fato, usando os resultados de Elberfeld-Jakoby-Tantau-2010, pode-se mostrar que o SAT pode ser decidido no espaço de log em fórmulas cujo gráfico de incidência delimitou a largura da árvore. Aqui está um esboço de como vão as principais etapas da prova desta reivindicação.

  1. As noções de decomposição de árvores e largura de árvore podem ser generalizadas para estruturas relacionais arbitrárias. Veja, por exemplo, as seções 2 e 3 deste artigo de Dalmau, Kolaitis e Vardi.
  2. O teorema de Courcelle afirma que a lógica do MSO pode ser decidida em tempo linear em estruturas relacionais de largura de árvore constante.
  3. Um teorema de Bodlaender implica que, se uma estrutura relacional tem uma largura , então uma decomposição em árvore dessa estrutura pode ser encontrada no tempo . Em outras palavras, essa decomposição pode ser encontrada em tempo linear em gráficos de largura de árvore constante.f ( t ) ntf(t)n
  4. Pode-se definir a estrutura relacional adequado que pode ser usado para codificar uma fórmula em conjunto com o gráfico de incidência . O treewidth de é no máximo uma constante mais o treewidth de .F I ττFIτI
  5. O conjunto de estruturas relacionais que codificam fórmulas satisfatórias + seus gráficos de incidência é definível pelo MSO.τ
  6. Portanto, pelo teorema de Bodlander + Courcelle, pode-se decidir se uma fórmula de largura de árvore constante é satisfatória em tempo linear.
  7. Elberfeld-Jakoby-Tantau-2010 mostra que "tempo linear" pode ser substituído por "espaço logarítmico" no teorema de Bodlaender e de Courcelle.
  8. Portanto, para cada fórmula MSO e cada estrutura relacional , é possível determinar no espaço logarítmico se satisfeito .τ τ φφττφ
  9. Em particular, o SAT pode ser determinado no espaço de log em gráficos de largura de árvore constante.
Mateus de Oliveira Oliveira
fonte