Livro de receitas para codificações SAT?

16

Os solucionadores de SAT estão se tornando cada vez mais eficientes na solução de grandes instâncias e estão sendo usados ​​como back-end em vários contextos. Toda vez que alguém deseja usá-los para resolver um problema em um domínio específico, ele / ela precisa criar uma codificação ad-hoc que não apenas tenha o conjunto certo de soluções, mas também coloque as restrições (mesmo redundantes) em uma forma isso ajuda as heurísticas dos solucionadores a encontrar uma solução mais rapidamente.

Muitas dessas codificações parecem-me muito comuns, por exemplo: afirmar que um conjunto finito de nós está vinculado como uma árvore, ou como um DAG, ou uma lista é classificada ...

Existe um livro de repositório / receita de codificações comuns para problemas comuns com soluções otimizadas?

Bordaigorl
fonte
1. Esta pergunta parece muito útil, mas também potencialmente excessiva. Eu acho que pode ser uma pergunta melhor se você focar em um único domínio (sim, isso pode envolver várias perguntas, uma por domínio - mas certifique-se de fazer uma pesquisa antes de perguntar e nos mostrar o que você fez).
DW
2. Além disso, que pesquisa você fez? Você já viu os front-ends da SAT, como STP, Alloy e Minion? Você já viu cs.stackexchange.com/q/12087/755 , cs.stackexchange.com/q/13188/755 , cs.stackexchange.com/a/6522/755 , cs.stackexchange.com/a/12153/ 755 ? nas perguntas marcadas sat-solvers ou satisfability ?
DW
Sim, a pergunta pode ser um pouco ampla. @DW obrigado pelos links, alguns deles são diretamente relevantes. Eu deveria ter mencionado que não estou interessado em resolver um problema específico, nem em métodos gerais para codificações mais eficientes; a expressão "práticas recomendadas" que usei provavelmente é enganosa, editarei. Estou interessado em um livro de receitas =)
Bordaigorl
Em relação ao domínio eu diria (hiper) teoria dos grafos, mas este é, provavelmente, ainda muito amplo ...
Bordaigorl
Consulte também a pergunta relacionada cs.stackexchange.com/q/12087
András Salamon

Respostas:

9

Eu li um artigo de pesquisa há alguns anos que parece relevante, " Successful SAT Encoding Techniques ", de Magnus Björk.

Abstrato:

Este artigo identifica boas práticas para codificações SAT analisando entrevistas com vários especialistas conhecidos em SAT. O objetivo é determinar a confiança em diferentes estratégias de codificação, analisando se há consenso entre os especialistas ou não, além de trazer conhecimento oculto aos usuários do SAT.

Existe um consenso de que as técnicas de codificação geralmente têm um impacto dramático na eficiência do solucionador SAT, que muitas vezes é preciso muito trabalho para encontrar uma boa codificação e que o tamanho de um encadeamento está apenas vagamente relacionado à dureza de encontrar uma solução . Os tópicos em que os entrevistados discordam incluem a viabilidade de incluir aritmética nos problemas do SAT e formular problemas como cláusulas ou circuitos.

O artigo descreve várias estratégias que são boas em diferentes situações, como maneiras diferentes de representar números e como usar a incrementalidade.

Kyle Jones
fonte
4

É sempre uma boa idéia dar uma olhada no Manual de Satisfação [1] (acho que não está disponível gratuitamente, desculpe). Aqui, o capítulo 2 é intitulado "CNF Encodings". No mínimo, o livro fornece referências de literatura sobre o estado da arte no momento da redação e você pode expandir sua pesquisa por elas.

Além disso, aqui e aqui estão dois slides recentes sobre o pré-processamento SAT. Os slides fornecem uma visão geral concisa das técnicas de pré-processamento e também outras referências. A idéia é que, em vez de tentar modelar "manualmente" o problema de maneira eficiente, você o modele da maneira mais fácil, pressione ir e um software fornecerá uma codificação eficiente.


[1] Biere, Armin, Marijn Heule e Hans van Maaren, orgs. Manual de satisfação. Vol. 185. IOS Press, 2009.

Juho
fonte
3

não exatamente uma resposta direta, mas outro ângulo cada vez mais estreitamente relacionado: parte disso é abordada por uma área de pesquisa relativamente nova, conhecida como SMT, Teorias do Módulo de Satisfação . a idéia básica é combinar codificações de problemas (por exemplo, aritmética inteira, gráficos etc.) no solucionador SAT, mas também usar / alavancar o conhecimento extra que vem desse acoplamento para criar algoritmos de solução mais avançados. aqui está uma pesquisa. como apontado, eles podem ser muito mais eficientes do que combinar um mecanismo de codificação ad-hoc com solucionadores SAT padrão.

  • Teorias do módulo de satisfação: um aperitivo / Leonardo de Moura e Nikolaj Bjørner

    Teorias de módulo de satisfação (SMT) é sobre verificar a satisfação de fórmulas lógicas sobre uma ou mais teorias. O problema baseia-se na combinação de algumas das áreas mais fundamentais da ciência da computação. Ele combina o problema da satisfação booleana com domínios, como os estudados em otimização convexa e manipulação de sistemas simbólicos. Também se baseia nos problemas mais prolíficos do século passado da lógica simbólica: o problema de decisão, a completude e a incompletude das teorias lógicas e, finalmente, a teoria da complexidade. O problema de combinar modularmente algoritmos de finalidade especial para cada domínio é tão profundo e intrigante quanto encontrar novos algoritmos que funcionam particularmente bem no contexto de uma combinação. O SMT também possui um papel muito útil na engenharia de software. Software moderno, análise de hardware e ferramentas baseadas em modelo são sistemas de software cada vez mais complexos e multifacetados. No entanto, seu núcleo é invariavelmente um componente que usa lógica simbólica para descrever estados e transformações entre eles. Um solucionador SMT bem ajustado que leva em consideração as inovações de ponta geralmente escala ordens de magnitude além dos solucionadores ad-hoc personalizados.

vzn
fonte
Este é um ponto muito bom. Mas mesmo quando você usa um solucionador de SMT, há uma parte puramente baseado SAT da busca que podem se beneficiar de "receitas" de sucesso ...
Bordaigorl
não é inteiramente exato dizer que há uma "parte puramente baseada em SAT da pesquisa", porque (como afirmado / pelo meu entendimento) usa a estrutura conhecida / construída especial das instâncias geradas em suas heurísticas que um solucionador de "baunilha" não usaria "reconhecer". em outras palavras, (isto é, a combinação ) não é "redutível / separável" para partes constituintes (isto é, codificador mais solucionador) ou apenas outro sistema de codificação padronizado.
vzn
Entendo. Vou ler mais sobre isso obrigado!
Bordaigorl 10/10
certo. Observe também que a programação do conjunto de respostas é um pouco semelhante.
vzn