Download do #SAT Solver

21

Alguém poderia apontar para um ou mais sites onde é possível fazer o download de uma implementação de trabalho de um solucionador #SAT? Estou interessado em retornar a contagem exata da solução, não em uma aproximação.

ds.algorithms sat software Giorgio Camerani
fonte
2
Olá Walter, sua pergunta está próxima à fronteira do que seria oficialmente "tópico" para este site. No entanto, se você não tiver nenhum outro lugar para fazer essa pergunta e pudermos respondê-la, talvez não seja tão ruim ... (Como o site ainda está em desenvolvimento, acho que estamos sendo mais abertos do que outros sites). que o objetivo deste comentário não é "repreender" ou "avisar", é apenas um aviso amigável.
Ryan Williams
Olá Ryan, obrigado pelo seu aviso. Sinto muito se esta pergunta está perto da fronteira. Pesquisei na web e não encontrei nada: apenas alguns solucionadores SAT, mas não #SAT. Por isso perguntei aqui. É claro que sei que posso escrever meu próprio código que usa um solucionador SAT como um mecanismo para contar soluções, mas estava procurando por algo já feito e pronto para uso.
Giorgio Camerani
12
Eu gostaria de discordar. Eu acho que essas questões estão dentro do escopo, e deveriam estar!
Suresh Venkat
concordar com seu escopo. fyi / imho não é muito prático construir um solucionador #SAT a partir de um solucionador SAT, a menos que se tenha o código fonte e, mesmo nesse caso, não seja tão prático, exceto por fórmulas muito pequenas, por causa de uma explosão exponencial muito ruim. técnicas normalmente especiais únicos para #SAT e não SAT seria necessário ...
vzn

Respostas:

16

Você pode fazer isso com o SAT4J , simplesmente repetindo todos os modelos: http://www.sat4j.org/howto.php#models . Eu imagino que a maioria dos solucionadores de SAT tem essa capacidade.

Dave Clarke
fonte
Oi supercooldave, obrigado pelo seu ponteiro. Eu não sabia que o SAT4J tinha essa capacidade.
Giorgio Camerani
16

Você também pode tentar o resolvedor #SAT "sharpSAT" ( site , github ) para contar o número de atribuições satisfatórias de fórmulas CNF.

Holger
fonte
11

Uma opção é usar uma biblioteca BDD, como JavaBDD . Todas essas bibliotecas têm uma função que conta as soluções rapidamente ou, pelo menos, facilitam a gravação dessa função. A desvantagem, no entanto, é que a construção do BDD será lenta em muitos casos e poderá exigir muita memória.

Caso sua entrada seja na CNF, uma heurística simples que acelera a construção do BDD é a seguinte. Primeiro, crie um pequeno BDD para cada cláusula e coloque-os em uma fila prioritária cuja raiz seja o menor BDD. Segundo, coloque dois BDDs, calcule AND entre eles e empurre o resultado para a fila de prioridade. Aqui está a idéia: como a computação AND entre BDDs de tamanho e leva na teoria, mas na prática, minimizar o tempo de execução é o mesmo que encontrar um código de Huffman.n O ( m n ) ∼ m + nmnO(mn)∼m+n

Radu GRIGore
fonte
7

Tópico relacionado: Melhor SAT Solver .

MS Dousti
fonte
11
Obrigado Sadeq. O tópico que você indicou parece ser teórico. Ele lista vários trabalhos sobre a redução do limite superior. É muito interessante, mas eu estava procurando uma implementação de trabalho pronta para uso.
Giorgio Camerani
2
Você é muito bem-vindo. Entre os links citados, havia um que era puramente prático: satcompetition.org . Eu acho que você pode encontrar implementações muito boas lá.
MS Dousti
7

O melhor que encontrei é o "compilador c2d". http://reasoning.cs.ucla.edu/c2d/

Ele usa d-DNNF e você precisa da opção -count .

Leon Leon
fonte
O c2d resolve muito mais CNFs do que o sharpsat. Para fins de brinquedo , o solucionador sat "relsat" também funciona.
Leon Leon
7

O MBound Solver fornecido aqui http://www.cs.cornell.edu/~sabhar/ pode fornecer contagens de modelos com garantias probabilísticas. É muito mais rápido do que enumerar todas as soluções.

Optar
fonte
5

Escrevi um modelo pequeno / enumerador implicante principal . Isso já pode ser usado para a contagem de modelos com a enumeração de modelos, mas isso não é muito prático. Se alguém estiver interessado, eu posso estendê-lo para que ele conte modelos dos principais implicantes.

Mikolas
fonte
2

O site BeyondNP contém um bom inventário das ferramentas existentes para resolver o #SAT (e outros problemas complexos relacionados às fórmulas CNF). Você também pode encontrar uma lista de ferramentas para contagem aproximada de modelos e compilação de conhecimento (a tarefa de transformar o CNF em uma estrutura de dados esperançosamente sucinta que geralmente oferece suporte à contagem polinomial de modelos de tempo).

Você também pode encontrar uma lista de ferramentas para o pré-processamento de fórmulas CNF que podem ser úteis para melhorar o desempenho dos contadores de modelos e vários benchmarks .

holf
fonte