Instâncias solucionáveis ​​em tempo polinomial do Max-Sat

18

O problema Max-Sat pede que você encontre uma atribuição de uma fórmula CNF que atenda ao máximo de cláusulas possível.

Para o problema mais simples SAT, existem muitos casos especiais conhecidos que podem ser resolvidos em tempo polinomial, por exemplo, podemos resolver 2-SAT em tempo polinomial.

Para Max-Sat, a situação é diferente, pois Max-Sat é NP-difícil, mesmo para fórmulas 2-CNF (cada cláusula contém apenas 2 variáveis).

Existem entradas especiais interessantes para as quais o Max-Sat é polinomial?

Em particular, eu estaria interessado em uma referência padrão para resolver o Max-Sat quando o gráfico de incedência limitar a largura da árvore.

sat treewidth max2sat Martin Vatshelle
fonte
3
Max-cut planar é um caso especial de max-cut, que é (em certo sentido) um caso especial de max-2-sat.
Jukka Suomela 31/01

Respostas:

6

Isso não responde diretamente ao seu problema Max-SAT, mas as referências podem orientá-lo para a resposta completa.

Szeider mostrou que a satisfação é tratável por parâmetros fixos quando parametrizada pela largura da árvore do gráfico de incidência. Samer e Szeider deram um algoritmo de programação dinâmica eficiente.

Referências

S. Szeider. Em parametrizações tratáveis ​​de parâmetros fixos do SAT. Em Proc. 6ª Conferência Internacional sobre Teoria e Aplicações da Satisfação (SAT'03), Artigos Selecionados e Revisados, vol. 2919 do LNCS, páginas 188–202. Springer-Verlag, 2004.

M. Samer e S. Szeider. Algoritmos para contagem de modelos proposicionais. Em Proc. 14ª Conferência Internacional de Lógica para Programação, Inteligência Artificial e Raciocínio (LPAR'07), vol. 4790 do LNCS, páginas 484–498. Springer-Verlag, 2007.

Samer e Szeider, rastreabilidade de parâmetros fixos. Em A. Biere, M. Heule, H. van Maaren e T. Walsh, editores, Handbook of Satis fi ability, parte 1, capítulo 13. IOS Press

Mohammad Al-Turkistany
fonte
Eu sei que alguns dos trabalhos de Stefan Szeiders, um artigo mais recente mostra que #SAT é polinomial quando o gráfico de incidência tem largura de clique limitada, o que também implica largura de árvore limitada (embora aqui tenhamos o tempo de execução do XP em vez do FPT). Friedrich Slivovsky e Stefan Szeider, Modelo de Contagem para Fórmulas de Largura de Clique Limitada, Algoritmos e Computação, vol. 8283, p. 677-687, LNCS, 2013 Eu sei que esse tipo de resultado geralmente se traduz em MAX-SAT, mas seria muito mais fácil ter uma referência onde isso já é feito, em vez de fazer sozinho.
Martin Vatshelle 31/01
0

Encontramos um tipo de propriedade:

FFxCxCCCxx

veja: http://arxiv.org/abs/1402.6485

Existem outras propriedades conhecidas?

Martin Vatshelle
fonte