Por que todos os solucionadores SAT recentes funcionam no CNF em vez do circuito SAT?

18

Após o lançamento da biblioteca da AIGER para manipular gráficos de inversores em 2006 (eu acho), alguns solucionadores de circuito SAT foram lançados em 2006-2008, e em algumas corridas / competições SAT havia faixas da AIG. No entanto, desde então, parece que o foco foi inteiramente no SMT ou na melhoria dos solucionadores de cláusulas SAT.

Intuitivamente, para mim, concentrar-me no circuito SAT parece fazer muito sentido: muitos, se não a maioria dos problemas, são mais naturalmente expressos como circuito SAT do que CNF; os circuitos fornecem informações estruturais que não podem ser projetadas de maneira reversa a partir do CNF, mas os circuitos sempre podem ser transformados em CNF; e pelo menos o campo industrialmente significativo da síntese lógica parece ser particularmente adequado para os AIGs.

Então o que aconteceu? Aconteceu que as informações estruturais extras não ajudam a resolver? O SAT baseado na AIG resolveu um experimento com falha?

Sami Liedes
fonte
É útil ter em mente que, ao otimizar um programa de baixo nível para velocidade e uso de memória, há algo a ser dito por simplicidade, por exemplo, é extremamente fácil representar e manipular uma fórmula CNF em C ou C ++.
Cody
incentivar uma discussão mais aprofundada em Ciência da Computação via Chat
vzn

Respostas:

4

existem muitos ângulos diferentes na sua pergunta. geralmente concordamos com sua premissa de que olhar para "informações estruturais" em uma formulação de SAT deve ser uma excelente área de pesquisa.

  • O SAT codificado no CNF é um padrão há décadas. foi solidificado no início e meados dos anos 90 com o formato / competições DIMACS .

  • o que tecnicamente é "informação estrutural"? pode ser difícil definir formalmente esse conceito e evitar círculos quase tautológicos. não há realmente nenhuma diferença entre uma codificação SAT CNF e outras codificações que preservam uma estrutura de rede. isso está incorporado nos conceitos de "cláusula / gráfico variável" que muitos solucionadores de SAT tendem a utilizar. em outras palavras, em um sentido aproximado, todo solucionador SAT significativo usa "informações estruturais" .

  • sim, as novas direções da pesquisa se concentraram na solução de ASP e SMT, que quase incorporam as "informações estruturais" sobre as quais você pergunta.

  • A transformação de Tseytin converte facilmente um circuito em SAT em P tempo / espaço para entrada em um solucionador SAT padrão. presumivelmente, é amplamente utilizado em muitos contextos, especialmente nos contextos dos circuitos de EE.

  • geralmente, existem algumas pesquisas isoladas ao longo das linhas mencionadas, mas infelizmente (novamente com sua premissa) ela nunca pareceu se desenvolver muito em uma tendência de pesquisa. Não pense que isso se deve à falta de fatores potenciais, mas mais humanos. dois artigos favoritos [1] [2], outro é examinar instâncias particulares de áreas como "instâncias industriais" ou "engenharia elétrica", das quais existe alguma pesquisa especializada.

  • Os puristas de CS às vezes tendem a querer evitar considerações de psicologia / sociologia em todas as abstrações matemáticas, mas razoavelmente ainda é um fator na ciência da computação . você pergunta sobre tendências de pesquisa, baseadas em fatores psicológicos humanos. é possível que haja algum efeito de iluminação pública aqui, conhecido como "frutas baixas". pode-se dizer / considerar que, mesmo agora com algumas décadas, a pesquisa algorítmica SAT está em sua infância, de modo que grandes questões como P vs NP não aparecem à vista, e talvez a pesquisa existente, embora substancial, ainda esteja "arranhando a superfície" .

[1] Decompondo problemas de satisfação ou Usando gráficos para obter uma melhor compreensão dos problemas de satisfação , Herwig 2006 (83pp)

[2] O fio da faca de constrangimento Walsh 1998

vzn
fonte
parece que mais pesquisas sobre a AIG ultimamente foram na direção de MIGs, gráficos de inversor maioritário, por exemplo, otimização de gráficos inversor de maioria com hash funcional / Soeken et al (2016), o ref pode ser extraído para refs adicionais
vzn
outro ângulo: a largura da árvore é uma "propriedade estrutural" significativa do tipo circuito e foi estudada extensivamente na dureza SAT, com trabalho contínuo. esse trabalho tende a ser mais teórico e nunca o ouviu sendo usado diretamente nos solucionadores SAT, mas parece bastante plausível que várias heurísticas do solucionador SAT estejam realmente relacionadas intrinsecamente ou correlacionadas com a largura de árvore.
vzn 17:00