Medindo a dificuldade das instâncias SAT

28

Dada uma instância do SAT, eu gostaria de poder estimar o quão difícil será resolver a instância.

Uma maneira é executar os solucionadores existentes, mas isso acaba com o objetivo de estimar as dificuldades. Uma segunda maneira pode ser procurar a proporção de cláusulas para variáveis, como é feito para transições de fase no SAT aleatório, mas tenho certeza de que existem métodos melhores.

Dada uma instância do SAT, existem algumas heurísticas rápidas para medir a dificuldade? A única condição é que essas heurísticas sejam mais rápidas do que realmente executando os solucionadores SAT existentes na instância.


Pergunta relacionada

Quais problemas de SAT são fáceis? em cstheory.SE. Esta pergunta faz perguntas sobre conjuntos de instâncias tratáveis. Essa é uma pergunta semelhante, mas não exatamente a mesma. Estou realmente interessado em uma heurística que, dada uma única instância, faça algum tipo de palpite semi-inteligente sobre se a instância será difícil de resolver.

Artem Kaznatcheev
fonte
Você pode explicar por que a transição de fase da "densidade" não é o que você precisa?
Raphael
@ Rafael, que é um método muito bom, e eu menciono na minha pergunta. Mas tive a impressão de que existem heurísticas ainda melhores. A transição de fase um me incomoda porque é parece tão fácil de truque (apenas cláusulas anexar facilmente satisfeita ou instância ao o que você está tentando disfarçar)
Artem Kaznatcheev
Desculpe, perdi essa parte da sua pergunta. Certo, como observam os comentaristas, a transição de fase parece ser sensível a fórmulas não aleatórias.
Raphael
2
Você pode representar uma fórmula SAT (no CNF) como um gráfico bipartido, com vértices para todas as fórmulas e cláusulas e arestas representando ocorrências. Se esse gráfico for fácil de particionar, o problema poderá ser decomposto nos subgráficos particionados. Talvez isso possa servir como uma medida útil? Não faço ideia (é por isso que é um comentário e não uma resposta).
Alex-Brink
Você pode achar isso útil: ece.uwaterloo.ca/~vganesh/QPaper/paper.pdf
user

Respostas:

22

Em geral, essa é uma questão de pesquisa muito relevante e interessante. "Uma maneira é executar os solucionadores existentes ..." e o que isso nos diria exatamente? Poderíamos ver empiricamente que uma instância parece difícil para um solucionador específico ou um algoritmo / heurística específico, mas o que isso realmente diz sobre a dureza da instância?

Uma maneira que foi buscada é a identificação de várias propriedades estruturais de instâncias que levam a algoritmos eficientes. De fato, essas propriedades são preferidas por serem "facilmente" identificáveis. Um exemplo é a topologia do gráfico de restrição subjacente, medido usando vários parâmetros de largura do gráfico. Por exemplo, sabe-se que uma instância é solucionável em tempo polinomial se a largura da árvore do gráfico de restrição subjacente estiver limitada por uma constante.

Outra abordagem se concentrou no papel da estrutura oculta das instâncias. Um exemplo é o conjunto de backdoor , significando o conjunto de variáveis ​​que, quando são instanciadas, o problema restante se simplifica para uma classe tratável. Por exemplo, Williams et al., 2003 [1] mostram que, mesmo considerando o custo de pesquisa de variáveis ​​de backdoor, ainda é possível obter uma vantagem computacional geral, concentrando-se em um conjunto de backdoor, desde que o conjunto seja suficientemente pequeno. Além disso, Dilkina et al., 2007 [2] observam que um solucionador chamado Satz-Rand é extraordinariamente bom em encontrar pequenas backdoors fortes em vários domínios experimentais.

Mais recentemente, Ansotegui et al., 2008 [3] propõem o uso da complexidade do espaço em forma de árvore como uma medida para solucionadores baseados em DPLL. Eles provam que também o espaço de contorno constante implica na existência de um algoritmo de decisão de tempo polinomial, com espaço sendo o grau do polinômio (Teorema 6 no artigo). Além disso, eles mostram que o espaço é menor que o tamanho dos conjuntos de ciclos. De fato, sob certas suposições, o espaço também é menor que o tamanho das backdoors.

Eles também formalizam o que eu acho que você procura, ou seja:

Encontre uma medida , e um algoritmo que, dada uma fórmula decida a satisfação no tempo . Quanto menor a medida, melhor ela caracteriza a dureza de uma fórmula .ψΓO(nψ(Γ))


[1] Williams, Ryan, Carla P. Gomes e Bart Selman. "Backdoors para a complexidade típica do caso." Conferência Conjunta Internacional sobre Inteligência Artificial. Vol. 18, 2003.

[2] Dilkina, Bistra, Carla Gomes e Ashish Sabharwal. "Trocas na complexidade da detecção de backdoor". Princípios e Práticas de Programação de Restrições (CP 2007), pp. 256-270, 2007.

[3] Ansótegui, Carlos, Maria Luisa Bonet, Jordi Levy e Felip Manya. "Medindo a dureza de instâncias SAT." Em Anais da 23ª Conferência Nacional de Inteligência Artificial (AAAI'08), pp. 222-228, 2008.

Juho
fonte
Eu gosto da formalização que você cita. Também seria bom refinar para declarar explicitamente que é eficientemente computável. Obrigado pela resposta! Você conhece alguma medida menos formal que as pessoas possam usar "na prática"? ψ(Γ)
Artem Kaznatcheev 01/04/12
@ArtemKaznatcheev Acho que o backdoor set é provavelmente o único realmente usado. Ao executar um solucionador, não nos importamos com a dureza da fórmula; a instância tem que ser resolvida, no entanto. A medida deve nos dar uma vantagem computacional, ou talvez possamos usá-la para escolher uma heurística adequada. Fora isso, acho que as medidas de dureza ainda são bastante experimentais.
Juho2
1

Como você conhece a transição de fase, permita-me mencionar algumas outras verificações simples que eu conheço (que provavelmente são incluídas na análise do gráfico de restrição):

  • Alguns geradores aleatórios do SAT criaram inadvertidamente fórmulas fáceis, porque usavam "densidade constante", o que significa uma proporção aproximadamente igual de todos os comprimentos de cláusula. Estes eram na maioria fáceis, porque duas cláusulas e unidades simplificam significativamente o problema, como seria de esperar, e cláusulas muito longas não acrescentam muita ramificação ou facilitam ainda mais a hiper-resolução. Portanto, parece melhor seguir as cláusulas de comprimento fixo e variar outros parâmetros.
  • Da mesma forma, uma poderosa regra de simplificação é a eliminação literal pura. Obviamente, uma fórmula é realmente tão difícil quanto o número de literais impuros que possui. Como o Resolution cria novas cláusulas numeradas(ou seja, o produto das ocorrências de e sua negação), o número de resolvidos é maximizado quando há um número igual de literais positivos e negativos para cada variável. Portanto, geradores SAT balanceados.|x||¬x|x
  • Existe também uma técnica chamada "No Triangle SAT", que parece bem nova [1], que é um tipo de gerador de instância difícil que proíbe "triângulos". Um triângulo é um conjunto de cláusulas contendo 3 variáveis que ocorrem aos pares em todas as combinações em algum conjunto de cláusulas (por exemplo, ). Aparentemente, triângulos tendem a facilitar uma fórmula para solucionadores conhecidos.v1,v2,v3{v1,v2,...},{v2,v3,...},{v1,v3,...}

[1] https://arxiv.org/pdf/1903.03592.pdf.

Homem cortador de grama
fonte
0

Além da excelente resposta do Juho, aqui está outra abordagem:

Ercsey-Ravasz & Toroczkai, Dureza da otimização como caos transitório em uma abordagem analógica à satisfação de restrições , Nature Physics volume 7, páginas 966–970 (2011).

Essa abordagem é reescrever o problema SAT em um sistema dinâmico, em que qualquer atrator do sistema é uma solução para o problema SAT. As bacias de atração do sistema são mais fractais à medida que o problema se torna mais difícil e, portanto, a "dificuldade" da instância do SAT pode ser medida examinando o quão caótico são os transitórios antes da convergência do sistema.

Na prática, isso significa iniciar um grupo de solucionadores a partir de diferentes posições iniciais e examinar a taxa na qual os solucionadores escapam dos transitórios caóticos antes de chegarem a um atrator.

Não é difícil criar um sistema dinâmico para o qual as "soluções" sejam soluções para um determinado problema de SAT, mas é um pouco mais difícil garantir que as soluções sejam todas atrativas e não repelentes. A solução deles é introduzir variáveis ​​de energia (semelhantes aos multiplicadores de Lagrange) para representar o grau de violação de uma restrição e tentar fazer com que o sistema minimize a energia do sistema.

Curiosamente, usando seu sistema dinâmico, você pode resolver problemas de SAT em tempo polinomial em um computador analógico, o que por si só é um resultado notável. Há um problema; pode exigir tensões exponencialmente grandes para representar as variáveis ​​de energia; portanto, infelizmente você não pode perceber isso no hardware físico.

Pseudônimo
fonte
11
"usando seu sistema dinâmico, você pode resolver problemas de SAT em tempo polinomial em um computador analógico, o que por si só é um resultado notável". Eu discordo que isso é notável. Como você observa: requer precisão exponencial. Este é realmente um truque padrão que se vincula diretamente à definição de NP. Se você pudesse medir a precisão exponencialmente, tente estimar o número de caminhos aceitos (ou veja como dyn sys de passeio aleatório) e veja se é exatamente zero ou poucos (é claro, isso exigiria uma medição exponencialmente precisa, igual ao sistema dinâmico).
Artem Kaznatcheev
Obrigado por isso. Não conheço muitos resultados teóricos sobre computação analógica.
Pseudônimo