Enumere todas as soluções de um problema SAT

11

Todos os solucionadores #SAT que eu conheço, por exemplo, RelSat, C2D, retornam apenas o número de instâncias satisfatórias. Mas eu quero conhecer cada uma dessas instâncias?

Existe um solucionador de #SAT ou como devo modificar um solucionador de #SAT disponível para fazer isso?

Obrigado.

lo.logic sat software qsp
fonte
7
Isso geralmente é chamado de "solucionador SAT de todas as soluções", mas não parece estar disponível de imediato. As referências que posso encontrar falam sobre modificações no MiniSAT e em outros solucionadores, geralmente adicionando cláusulas de bloqueio para excluir uma solução quando encontrada. Por outro lado, a maioria dos solucionadores de restrições suporta a geração de todas as soluções como padrão.
András Salamon
uma abordagem é uma conversão CNF → DNF para o qual existe uma grande quantidade de literatura
vzn

Respostas:

13

Você está procurando um solucionador ALL-SAT ou todas as soluções SAT. Esse é um problema diferente do #SAT. Você não precisa enumerar todas as soluções para contá-las.

Não conheço uma ferramenta que resolva seu problema porque as pessoas adicionam esses algoritmos aos solucionadores de SAT existentes, mas raramente parecem liberar essas extensões. Dois documentos que devem ajudá-lo a modificar um solucionador de CDCL para implementar o ALL-SAT estão abaixo.

Solucionador SAT de Todas as Soluções com Eficiência de Memória e sua Aplicação à Acessibilidade , O. Grumberg, A. Schuster, A. Yadgar, FMCAD 2004

Aqui está um artigo recente publicado no arXiv.

Ampliando os Solvers SAT modernos para enumerar todos os modelos , Said Jabbour, Lakhdar Sais, Yakoub Salhi, 2013

Você pode tentar entrar em contato com esses autores para a implementação deles.

Vijay D
fonte
Para o segundo artigo, basta clicar na primeira versão v1 para vê-lo.
Tayfun Pay
Este artigo recente parece relacionado: homes.cs.washington.edu/~sudeepa/UAI2013-ModelCounting.pdf
Kaveh:
1
@ Kaveh, acredito que o OP está pedindo um solucionador ALLSAT ou uma maneira de transformar um solucionador #SAT em um solucionador ALLSAT. Este é um documento com limites mais baixos para #SAT. Não sei se isso ajuda o OP.
Vijay D
2

Encontrei um artigo mais recente (2014) sobre o All-SAT em uma conferência VLSI, portanto ele é definitivamente voltado para o lado prático (o que parece estar em sintonia com a pergunta do OP aqui, embora menos com a cstheory.SE em geral):

  • "All-SAT usando cláusulas de bloqueio mínimas" de Yinlei Yu, Pramod Subramanyan, Nestan Tsiskaridze, Sharad Malik, VLSI Design 2014. doi: 10.1109 / VLSID.2014.22 .

Para aqueles sem assinatura do IEEE, há uma cópia gratuita na página da Web de Subramanyan em Princeton . (Ele usa um serviço de compartilhamento de arquivos para armazenar / distribuir cópias de seus documentos e não tenho certeza de quão estáveis ​​são esses URLs, portanto, este link indireto.)

A essência deste artigo parece ser:

Nossa contribuição, o algoritmo Non-Disjoint-Dec, gera cláusulas de bloqueio extremamente curtas que não contêm nenhuma das variáveis ​​implícitas no solucionador. Observe que normalmente a maioria das variáveis ​​em um mintermo satisfatório está implícita. Cláusulas curtas de bloqueio são muito benéficas para o desempenho do solucionador, conforme demonstrado pela avaliação.

Sua implementação se baseia no MiniSat. O código-fonte para sua extensão não parece estar disponível publicamente. Infelizmente, isso parece ser um hábito no campo do All-SAT, portanto, os trabalhos nessa área que contêm resultados experimentais apenas configuram um algoritmo mais ou menos simples e mais simples de superar e raramente podem ser comparados diretamente (em termos de experimentos). resultados) com qualquer outro algoritmo publicado para All-SAT. O artigo de Jabbour et al. mencionado por Vijay D também é desse tipo.

Como não vejo isso mencionado na outra resposta (mas apenas no comentário de András Salamon), a [bastante popular] técnica de cláusulas de bloqueio foi introduzida em:

Efervescer
fonte