Medindo a dificuldade das instâncias SAT

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.

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 .$\psi$$\Gamma$$O(n^{\psi ( \Gamma )})$

[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.

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|*|\lnot 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.$v_1, v_2, v_3$$\{v_1, v_2, ...\}, \{v_2, v_3, ...\}, \{v_1, v_3, ...\}$

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

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.