Existe um algoritmo às vezes eficiente para resolver #SAT?

24

Seja uma fórmula booleana que consiste nos operadores usuais AND, OR e NOT e em algumas variáveis. Gostaria de contar o número de satisfazer atribuições para B . Ou seja, quero encontrar o número de diferentes atribuições de valores de verdade para as variáveis ​​de B para as quais B assume um valor verdadeiro. Por exemplo, a fórmula a b tem três atribuições satisfatórias; ( a b ) ( c ¬ b ) tem quatro. Este é o problema #SAT .BBBBab(ab)(c¬b)

Obviamente, uma solução eficiente para esse problema implicaria uma solução eficiente para o SAT, o que é improvável e, de fato, esse problema é # P-completo e, portanto, pode ser estritamente mais difícil que o SAT. Portanto, não estou esperando uma solução eficiente garantida.

Mas é sabido que existem relativamente poucas instâncias realmente difíceis do próprio SAT. (Veja, por exemplo, Cheeseman 1991, "Onde estão os problemas realmente difíceis" .) A pesquisa comum podada, embora exponencial no pior dos casos, pode resolver muitas instâncias com eficiência; métodos de resolução, embora exponenciais no pior dos casos, são ainda mais eficientes na prática.

Minha pergunta é:

Existem algoritmos conhecidos que podem contar rapidamente o número de atribuições satisfatórias de uma fórmula booleana típica, mesmo que esses algoritmos exijam tempo exponencial na instância geral? Existe algo visivelmente melhor do que enumerar todas as atribuições possíveis?

Mark Dominus
fonte
1
Tentei adicionar uma tag para # p-completeness, mas o software Stack Exchange não gosta do sinal #.
precisa
Eu teria cuidado ao afirmar que "existem relativamente poucas instâncias realmente difíceis do próprio SAT". Acredito que o artigo que você vincula realmente fale sobre k -SAT aleatório . Além disso, o fenômeno de transição de fase se aplica apenas a instâncias aleatórias. Existem muitas instâncias artesanais, industriais, etc., realmente difíceis de SAT. k
Juho
Obrigado. Você acha que isso tende a deixar minha pergunta menos clara? Você entende o que estou pedindo?
precisa
Está claro para mim. É apenas importante lembrar que casos apresentam a transição de fase :)
Juho

Respostas:

21

Contando no caso geral

2

Os métodos de contagem exata geralmente são baseados em pesquisa exaustiva no estilo DPLL ou em algum tipo de compilação de conhecimento. Os métodos aproximados são geralmente classificados como métodos que fornecem estimativas rápidas, sem garantias e métodos que fornecem limites inferiores ou superiores com uma garantia de correção. Também existem outros métodos que podem não se encaixar nas categorias, como a descoberta de backdoors ou métodos que insistem em certas propriedades estruturais para manter as fórmulas (ou seu gráfico de restrições).

Existem implementações práticas por aí. Alguns contadores exatos de modelos são CDP, Relsat, Cachet, sharpSAT e c2d. O tipo de principais técnicas usadas pelos solucionadores exatos são contagens parciais, análise de componentes (do gráfico de restrição subjacente), cache de fórmula e componente e raciocínio inteligente em cada nó. Outro método baseado na compilação de conhecimento converte a fórmula CNF de entrada em outra forma lógica. Nesse formulário, a contagem do modelo pode ser deduzida facilmente (tempo polinomial no tamanho da fórmula recém-produzida). Por exemplo, pode-se converter a fórmula em um diagrama de decisão binário (BDD). Pode-se atravessar o BDD da folha "1" de volta à raiz. Ou, por outro exemplo, o c2d emprega um compilador que transforma as fórmulas CNF em forma normal de negação decompositável determinística determinística (d-DNNF).

ϕϕ

Gogate e Dechter [3] usam uma técnica de contagem de modelos conhecida como SampleMinisat. Baseia-se na amostragem do espaço de pesquisa livre de retorno de uma fórmula booleana. A técnica baseia-se na idéia de re-amostragem de importância, usando os solucionadores SAT baseados em DPLL para construir o espaço de pesquisa livre de retorno. Isso pode ser feito completamente ou até uma aproximação. A amostragem para estimativas com garantias também é possível. Com base em [2], Gomes et al. [4] mostraram que usando amostragem com uma estratégia aleatória modificada, é possível obter limites inferiores comprováveis ​​na contagem total de modelos com altas garantias probabilísticas de correção.

Há também um trabalho que se baseia na propagação de crenças (PA). Veja Kroc et al. [5] e o BPCount que eles introduzem. No mesmo artigo, os autores fornecem um segundo método chamado MiniCount, para fornecer limites superiores na contagem de modelos. Há também uma estrutura estatística que permite calcular os limites superiores sob certas suposições estatísticas.

Algoritmos para # 2-SAT e # 3-SAT

O(1.3247n)O(1.6894n)O(1.6423n)

Como é da natureza do problema, se você deseja resolver instâncias na prática, muito depende do tamanho e da estrutura de suas instâncias. Quanto mais você souber, mais capaz terá de escolher o método certo.


[1] Vilhelm Dahllöf, Peter Jonsson e Magnus Wahlström. Contando tarefas satisfatórias em 2-SAT e 3-SAT. Em Anais da 8ª Conferência Anual Internacional de Computação e Combinatória (COCOON-2002), 535-543, 2002.

[2] W. Wei e B. Selman. Uma nova abordagem para a contagem de modelos. Em Proceedings of SAT05: 8a Conferência Internacional sobre Teoria e Aplicações de Teste de Satisfação, volume 3569 de Notas de Aula em Ciência da Computação, 324-339, 2005.

[3] R. Gogate e R. Dechter. Contagem aproximada por amostragem do espaço de pesquisa sem retrocesso. Em Anais da AAAI-07: 22ª Conferência Nacional de Inteligência Artificial, 198–203, Vancouver, 2007.

[4] CP Gomes, J. Hoffmann, A. Sabharwal e B. Selman. Da amostragem à contagem de modelos. Em Anais da IJCAI-07: 20ª Conferência Conjunta Internacional sobre Inteligência Artificial, 2293–2299, 2007.

[5] L. Kroc, A. Sabharwal e B. Selman. Alavancando a Propagação de Crenças, a Pesquisa de Retorno e Estatísticas para Contagem de Modelos. No CPAIOR-08: 5ª Conferência Internacional sobre Integração de Técnicas de IA e OR na Programação de Restrições, volume 5015 de Notas de Aula em Ciência da Computação, 127-141, 2008.

[6] K. Kutzkov. Novo limite superior para o problema nº 3-SAT. Cartas de processamento de informações 105 (1), 1-5, 2007.

Juho
fonte
8

Além dos artigos listados por Juho, aqui estão alguns outros que descrevem trabalhos sobre esse tópico, especialmente sobre a aproximação do número de soluções:

DW
fonte