Quais problemas de SAT são fáceis?

27

O que são "regiões fáceis" para garantir a satisfação? Em outras palavras, condições suficientes para que algum solucionador SAT seja capaz de encontrar uma tarefa satisfatória, assumindo que ela exista.

Um exemplo é quando cada cláusula compartilha variáveis ​​com poucas outras cláusulas, devido à prova construtiva da LLL, outros resultados nesse sentido?

literatura considerável sobre regiões fáceis para a Propagação de Crenças, existe algo nesse sentido para satisfação?

Yaroslav Bulatov
fonte
2
Você também está interessado na transição aleatória da fase SAT?
Suresh Venkat
Como é a condição suficiente? Peter Shor mencionou em outro post que a instância do SAT precisa possuir "estrutura aleatória" para tornar relevantes a proporção de cláusulas e variáveis. Gostaria de saber se isso é algo que pode ser codificado em condições suficientes.
Yaroslav Bulatov

Respostas:

33

Eu acho que você conhece o resultado clássico de Schaefer do STOC'78, mas por precaução.

10.1145 / 800133.804350

Schaefer provou que, se o SAT é parametrizado por um conjunto de relações permitido em qualquer instância, existem apenas 6 casos tratáveis: 2-SAT (ou seja, todas as cláusulas são binárias), Horn-SAT, dual-Horn-SAT, affine-SAT ( soluções para equações lineares em GF (2)), 0-válido (relações satisfeitas pela atribuição all-0) e 1-válido (relações satisfeitas pela atribuição all-1).

Standa Zivny
fonte
3
Há um papel mais recente que refinar este resultado: A complexidade dos problemas satisfiability: "teorema de Refino Schaefer" Eric Allender, Michael Bauland, Neil Immerman, Henning Schnoor e Heribert Vollmer
Vinicius dos Santos
1
Obrigado, aqui está o doi: dx.doi.org/10.1016/j.jcss.2008.11.001
Standa Zivny
Observe que esses são problemas de satisfação com restrições e não SAT (embora possam ser reescritos como instâncias SAT, mas tecnicamente, SAT significa CSP com predicados OU).
MCH
14

Não tenho certeza se é isso que você está procurando, mas há uma literatura considerável sobre a transição de fase 3-SAT.

Monasson, Zecchina, Kirkpatrcik, Selman e Troyansky tiveram um artigo na natureza que fala sobre a transição de fase do k-SAT aleatório. Eles usaram uma parametrização da razão de cláusulas para variáveis. Para o 3-SAT aleatório, eles descobriram numericamente que o ponto de transição está em torno de 4,3. Acima deste ponto, as instâncias aleatórias de 3-SAT são excessivamente restritas e quase certamente insatificáveis ​​e, abaixo deste ponto, os problemas são restritos e satisfatórios (com alta probabilidade). Mertens, Mezard e Zecchina usam procedimentos de método de cavidade para estimar o ponto de transição de fase com maior precisão.

Longe do ponto crítico, os algoritmos "burros" funcionam bem para instâncias satisfatórias (caminhada, etc.). Pelo que entendi, o tempo de execução determinista do solucionador cresce exponencialmente na transição de fase ou próximo a ela (veja aqui mais para uma discussão?).

Braunstein, Mezard e Zecchina, primo próximo da propagação de crenças, introduziram a propagação de pesquisas que são relatadas para resolver instâncias 3-SAT satisfatórias em milhões de variáveis, mesmo extremamente próximas à transição de fase. Mezard fez uma palestra aqui sobre binóculos (cuja teoria ele usou na análise de transições de fase NP-Completas aleatórias) e Maneva fez uma palestra aqui sobre propagação de pesquisas.

Por outra direção, ainda parece que nossos melhores solucionadores levam um tempo exponencial para provar a insatisfação. Veja aqui , aqui e aqui para provas / discussão da natureza exponencial de alguns métodos comuns para provar a insatisfação (procedimentos de Davis-Putnam e métodos de resolução).

É preciso ter muito cuidado com as alegações de 'facilidade' ou 'dureza' para problemas aleatórios de NP-Complete. A exibição de um problema NP-Complete em uma transição de fase não dá garantia de onde estão os problemas difíceis ou se existem. Por exemplo, o problema do ciclo Hamiltoniain nos gráficos aleatórios Erdos-Renyi é comprovadamente fácil, mesmo no ponto de transição crítico ou próximo a ele. O Problema da Partição Numérica não parece ter algoritmos que o resolvam bem na faixa de probabilidade 1 ou 0, muito menos perto do limite crítico. Pelo que entendi, problemas aleatórios de 3-SAT têm algoritmos que funcionam bem para instâncias satisfatórias quase iguais ou abaixo do limite crítico (propagação da pesquisa, caminhada, etc.), mas nenhum algoritmo eficiente acima do limite crítico para provar a insatisfação.

user834
fonte
Eu me pergunto se aqueles qualquer um desses resultados "aleatório k-SAT" transferir para a vida real exemplos SAT, em outras palavras, se a razão de cláusulas de variáveis ainda é um indicador útil da dureza
Yaroslav Bulatov
1
@Yaroslav, da minha experiência, não. Muitos problemas do mundo real (mesmo reduções) têm (ou introduzem) tanta estrutura para destruir a aleatoriedade para a qual muitos solucionadores foram otimizados. Parece que, em algum momento, poderemos explicar essa estrutura de alguma maneira e concentrar-nos apenas na parte aleatória (ou na "essência" do problema aleatório), mas não vejo nenhuma maneira geral de fazer isso nem Eu realmente conheço alguns exemplos que empregam essa estratégia.
usar o seguinte comando
R(F)Fr[0 0,1]F
5

Existem muitas condições suficientes. Em certo sentido, grande parte do CS teórico foi dedicado à coleta dessas condições - rastreabilidade de parâmetros fixos, 2-SAT, 3-SAT aleatório de diferentes densidades, etc.

Peter Boothe
fonte
2
É verdade, pode-se pegar qualquer problema X que seja fácil de resolver e dizer que "qualquer fórmula que corresponda ao problema X é fácil". Eu acho que eu estou procurando condições suficientes que são mais eficientes no resumindo a região fácil do que "todos os problemas conhecidos para a P", mais parecido com o que o construtivo Lovasz local Lema faz
Yaroslav Bulatov
3

até agora, não há muito reconhecimento amplo desse conceito na literatura, mas o gráfico de cláusulas do problema SAT (o gráfico com um nó por cláusula e os nós estão conectados se as cláusulas compartilharem variáveis), bem como outros gráficos relacionados da representação do SAT, parece ter muitas pistas básicas sobre o quão difícil a instância será, em média.

o gráfico da cláusula pode ser analisado através de todos os tipos de algoritmos teóricos dos grafos, é uma medida aparentemente natural da "estrutura" e com fortes conexões para medir / estimar a dureza, e parece que a pesquisa nessa estrutura e suas implicações ainda é muito precoce estágios. não é inconcebível que a pesquisa de pontos de transição, a maneira tradicional e bem estudada de abordar essa questão, possa eventualmente ser conectada a essa estrutura de gráfico de cláusulas (até certo ponto, ela já possui). em outras palavras, o ponto de transição no SAT pode existir "por causa" da estrutura do gráfico de cláusulas.

aqui está uma excelente referência nesse sentido, uma tese de doutorado de Herwig, e muitas outras.

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

vzn
fonte
este é o gráfico de dependência ao aplicar o lema local e as variantes do lovasz à satisfação. nesse sentido, o gráfico de cláusulas foi analisado bastante . Shearer caracteriza os gráficos para os quais o lema local é válido, e Kolipaka e Szegedy tornaram o resultado de Schaefer construtivo. Quando você não sabe muito, por favor, não deduza que ninguém sabe!
Sasho Nikolov
A decomposição de shaefers em algumas classes tratáveis ​​é mencionada na resposta por Zivny, mas essa análise de gráfico de cláusulas é relativamente mais nova, mais profunda e mais sutil, e mais com um sabor empírico. como para as citações que você menciona, não parecem ser mencionado muitas vezes em SAT papéis de dureza / pesquisa ... existem vários / paralelo linhas entrelaçadas de inquérito ...
vzn
Schaefer foi um erro de digitação, eu quis dizer Shearer. O LLL e suas variantes são a principal ferramenta para delimitar as instâncias difíceis do k-SAT; uma pesquisa no Google revelará toneladas de referências. O teorema de Shearer mostra quais gráficos de cláusulas garantem que qualquer instância SAT com esse gráfico seja necessariamente satisfatória. Olhe para esta pesquisa para conexões detalhado para limiares de dureza, dificuldade de construir situações difíceis, algoritmos, etc. disco.ethz.ch/lectures/fs11/seminar/paper/barbara-3.pdf
Sasho Nikolov
1
um pensamento geral: cada vez que você diz que algo é terra incógnita, há uma forte possibilidade de que seja terra incógnita para você . de qualquer forma, esse tipo de comentário é inútil, a menos que você seja um especialista estabelecido e publicado na área. seria melhor se você restringisse suas respostas ao que sabe e deixasse comentários sobre o que acha que ninguém sabe.
Sasho Nikolov
1
A LLL é uma ferramenta para analisar o SAT, inventada em 1975 com talvez alguns aprimoramentos desde então. é uma receita para instâncias fáceis ou difíceis suficientes, mas não é necessário . existem outras abordagens desde então que preenchem cada vez mais a lacuna de maneiras novas, ou seja, aumentam e ultrapassam. você deve confundir esta resposta com outra coisa, não há uso do termo "terra incognita" na pergunta acima. E sugerem que você limitar-se às respostas reais escritos e não especular sobre o que os outros sabem ou não sabe =)
vzn
1

É fácil mover todas as instâncias perto do ponto de "transição" para o mais longe possível do ponto de "transição". O movimento envolve um esforço polinomial de tempo / espaço.

Se instâncias distantes do ponto de "transição" são mais fáceis de resolver, as que estão próximas ao ponto de transição devem ser igualmente fáceis de resolver. (Transformações polinomiais e tudo.)

GHR
fonte
você pode elaborar, ou você tem um juiz para isso?
vzn
1

κ

ele encontra uma aparente estrutura de auto-similaridade fractal de instâncias difíceis com o parâmetro de restrição, de modo que, como um solucionador de DP (LL) durante a pesquisa, tende a encontrar subproblemas com a mesma restrição crítica, independentemente da variável escolhida ao lado da ramificação. há algumas análises adicionais da estrutura fractal em instâncias SAT (como a dimensão Hausdorff das fórmulas SAT e a conexão à dureza) em, por exemplo, [2,3]

Outra linha de investigação um tanto inter-relacionada aqui é a relação de pequenos gráficos mundiais com a estrutura SAT (rígida), por exemplo [4,5]

=?

[1] O fio da faca de constrangimento de Toby Walsh 1998

[2] AUTO-SIMILARIDADE DE EXPRESSÕES BOOLEANAS SATISFEITÁVEIS DECIFERIDAS EM TERMOS DE SISTEMAS DE FUNÇÕES ITERADAS DIRECIONADAS POR GRÁFICO, por Ni e Wen.

[3] Visualização da estrutura interna das instâncias SAT (relatório preliminar) Sinz

[4] Pesquisa em um mundo pequeno por Walsh 1999

[5] Modelando problemas SAT mais realistas por Slater 2002

vzn
fonte
3
É DPLL, não DP (LL), a propósito. Além disso, há trabalhos significativamente mais recentes sobre a transição de fases no SAT (veja o trabalho de Achlioptas, por exemplo).
Vijay D
existe um algoritmo DP que precede a DPLL que possui um comportamento semelhante. a outra resposta por user834 pesquisa ponto de transição SAT mencionado principalmente com muitos refs mas esta resposta enfatiza um ângulo diferente (mas interrelacionados)
vzn
1
Estou ciente desses algoritmos. Eu estava apenas apontando a convenção tipográfica padrão, que é escrever DP, ou DPLL, ou DPLL (T) ou DPLL (Join), para o caso de primeira ordem sem quantificador. Ninguém escreve DP (LL) e acrescenta confusão com DPLL (T) e DPLL (Join)
Vijay D
DP (LL) é o que se entende como DP + DPLL
vzn