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))
cc.complexity-theory
sat
big-list
Subhayan
fonte
fonte
Respostas:
(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:
fonte
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 .k k
Veja este post .
fonte
No "lado NP-complete", deparei-me com essas variantes (fiz uma pergunta semelhante no cs.stackexchange também):
fonte
fonte
Além da lista acima, também existem:
fonte
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.
fonte