variações de SAT

14

Procurei na internet, mas não consegui encontrar nenhuma 'grande lista' de variantes do problema SAT.

Além do (comum)

  • SENTOU,
  • k-SAT,
  • MAX-kSAT,
  • Half-SAT,
  • XOR-SAT,
  • NAE-SAT

o que mais variantes existem?

(também será realmente útil se houver classes de complexidade (quando possível))

Subhayan
fonte
Qual seria o objetivo desta lista?
Tyson Williams
2
Primeiro porque eu queria apresentar uma palestra para alguns estudantes de graduação. Eu estava planejando falar sobre as variações do SAT e mostrar algumas reduções (não triviais) ... elas já tiveram um curso introdutório no TOC, então achei que poderia ser uma boa idéia .. E A SEGUNDA RAZÃO não existe essa lista na internet, essa lista também servirá a qualquer mente curiosa que queira saber sobre as variantes.
precisa saber é o seguinte
11
Não tenho certeza de como esta lista ajudará na sua palestra. Em vez de ler uma lista arbitrariamente longa de variantes do SAT, uma mente curiosa deve ler o teorema da dicotomia de Schaefer e a generalização de Allender et al. isso mostra que todas as variantes possíveis de SAT estão completas para uma das seis classes de complexidade conhecidas.
Tyson Williams
é uma boa sugestão ... obrigado @TysonWilliams ... você também pode responder isso, embora não seja exatamente isso que eu estava procurando, mas certamente isso é útil.
precisa saber é o seguinte

Respostas:

17

(Tornar o comentário uma resposta conforme solicitado e expandir um pouco.)

"Uma mente curiosa" deve ler o teorema da dicotomia de Schaefer e a generalização de Allender et al. mostra que todas as variantes possíveis de SAT são triviais ou em uma das seis classes de complexidade conhecidas:

  1. NP-completo
  2. P-completo
  3. NL-completo
  4. L-complete
  5. CompleteL-completo
  6. co-NLOGTIME
Tyson Williams
fonte
17

Esta lista será muito longa;) Aqui estão algumas das minhas variantes favoritas (completas de NP) do SAT:

  • PLANAR ( 3,3 ) -SAT (cada cláusula contém pelo menos dois e no máximo três literais, cada variável aparece em exatamente três cláusulas; duas vezes em sua forma não-negada, e uma vez em sua forma negada, e o gráfico de incidência bipartido é planar.)

    Veja: Dahlhaus, Johnson, Papadimitriou, Seymour, Yannakakis, A complexidade dos cortes multiterminais, SIAM Journal of Computing 23 (1994) 864-894

  • PLANO PLANAR COM 4 CONEXÕES 3SAT (cada cláusula contém exatamente 3 variáveis ​​distintas, cada variável aparece em no máximo 4 cláusulas, o gráfico de incidentes bipatitos é plano e conectado 3)

    Veja: Kratochvíl, um problema especial de satisfação planar e uma conseqüência de sua completude NP, Matemática Aplicada Discreta. 52 (1994) 233-252

  • MONOTONE CUBIC 1-IN-3SAT (MONOTONE-1-IN-3SAT, em que cada variável aparece exatamente 3 vezes)

    Veja: Moore e Robsen, problema de inclinação difícil com ladrilhos simples, computação discreta. Geom. 26 (2001) 573-590

  • Acho muito interessante que o PLANAR-NAE- SAT esteja em P para cada k .kk

    Veja este post .

user13136
fonte
4
Se você acha o último ponto interessante, também deve estar interessado em saber que # PLANAR-NAE-3SAT (soluções de contagem) também é tratável, enquanto outras variantes aparentemente simples de SAT como PLANAR-MONOTONE-2SAT são tratáveis ​​(ou até triviais) como um problema de decisão, mas difícil de contar. Observe que a redução do último link acima (redução de PLANAR-NAE-kSAT para PLANAR-NAE-3SAT) não é parcimoniosa e que # PLANAR-NAE-4SAT é # P-difícil.
22813 William Whistler #
11

No "lado NP-complete", deparei-me com essas variantes (fiz uma pergunta semelhante no cs.stackexchange também):

Marzio De Biasi
fonte
7

SUMAT(k)SUMATkSUMAT(2)euSUMAT(k)k3

Jan Johannsen
fonte
1

Além da lista acima, também existem:

  • #SAT: contagem de modelos
  • All-SAT: enumeração de modelos
qsp
fonte
1

Existe uma conexão muito clássica entre lógica e álgebra, que remonta à origem da lógica moderna e ao trabalho de George Boole. Uma fórmula na lógica proposicional pode ser interpretada como um elemento de uma álgebra booleana. As constantes lógicas true e false se tornam as noções algébricas dos elementos superior e inferior de uma rede. As operações lógicas de conjunção, disjunção e negação se tornarão as operações algébricas de encontro, união e complementação na álgebra booleana. Essa conexão é menos enfatizada nos tratamentos modernos da lógica, mas é particularmente interessante no contexto da sua pergunta. A álgebra nos permite afastar muitos detalhes específicos do problema e encontrar generalizações de um problema que se aplicará a muitas situações diferentes.

No caso específico de SAT, a pergunta algébrica que se pode perguntar é o que acontece quando interpretamos fórmulas em treliças mais gerais que as álgebras booleanas. No lado lógico, você pode generalizar o problema da satisfação, da lógica proposicional à lógica intuicionista. De maneira mais geral, você pode generalizar o problema de satisfação proposicional para determinar se uma fórmula, quando interpretada sobre uma rede delimitada (uma com top e botto), define o elemento inferior da rede. Essa generalização permite tratar problemas na análise de programas como problemas de satisfação.

Outra generalização é a lógica de primeira ordem sem quantificadores, na qual você obtém a questão do módulo de satisfação de uma teoria. Ou seja, além de ter variáveis ​​booleanas, você também possui variáveis ​​de primeira ordem e símbolos de função e deseja saber se uma fórmula é satisfatória. Nesse ponto, você pode fazer perguntas sobre fórmulas em aritmética, teorias de strings ou matrizes, etc. Portanto, obtemos uma generalização rigorosa e muito útil do SAT, que possui muitas aplicações em sistemas, segurança de computadores, linguagens de programação, verificação de programas, planejamento , inteligência artificial etc.

Vijay D
fonte