Em outro tópico , Joe Fitzsimons perguntou sobre "os melhores limites inferiores atuais no 3SAT".
Eu gostaria de seguir o outro caminho: qual é o melhor limite superior atual no 3SAT? Em outras palavras, qual é a complexidade de tempo do solucionador SAT mais eficiente?
Em particular, é concebível encontrar um algoritmo subexponencial (ainda super polinomial) para o SAT?
cc.complexity-theory
ds.algorithms
sat
upper-bounds
MS Dousti
fonte
fonte
Respostas:
Existem dois tipos de "melhores" solucionadores de SAT, um para teoria e outro para prática.
Teoria
Prática
Verifique a conferência SAT para obter resultados da competição para cada ano.
fonte
Eu não conheço nenhum algoritmo aleatório com erro zero (ou algoritmos coNE / Eadvice ,
para esse assunto) para SAT que tenham limites melhores que os algoritmos determinísticos conhecidos,
independentemente de prometer ou não haver no máximo uma tarefa satisfatória.
reivindica um resultado que pode ser resumido da seguinte forma:
fonte
O algoritmo de Schoening é um algoritmo probabilístico para k-SAT com tempo de execução , em que . Isso resulta em um algoritmo para 3SAT, um algoritmo para 4SAT, etc.O(an) a=2(k−1)/k O(1.33334n) O(1.5n)
O algoritmo também foi (quase completamente) des randomizado por Moser e Scheder, que fornecem um algoritmo determinístico para resolver o tempo de execução do kSAT que é a mesma constante de antes e pode ser arbitrariamente pequeno.O((a+ϵ)n) a ϵ>0
Nota: Nesta resposta, a grande notação Oh oculta fatores pol (n). Eu queria usar a notação , mas ela não está sendo renderizada corretamente.O∗
fonte
Como já foi mencionado, se você estiver interessado em garantias teóricas de tempo de execução, essa pergunta é uma duplicata.
Mas gostaria de ressaltar que, se você realmente deseja resolver um problema concreto (como o problema de cores mencionado), acho que não faz absolutamente nenhum sentido estudar os limites teóricos superiores.
Mesmo que você queira evitar aspectos de "engenharia", sugiro que você faça alguns solucionadores SAT populares, experimente-os e veja o que acontece (a maioria deles pode ler o mesmo formato de arquivo DIMACS, por isso é fácil tentar diferentes solucionadores). Você pode ter surpresas positivas e negativas. Recentemente, tive uma família de instâncias do SAT; um monte de instâncias com dezenas de milhares de variáveis e mais de um milhão de cláusulas acabou sendo fácil de resolver, enquanto instâncias aparentemente mais simples com apenas centenas de variáveis e milhares de cláusulas eram difíceis demais para qualquer solucionador que eu tentasse.
fonte
fonte
É impossível para o 3SAT ter algoritmos subexponenciais, a menos que a hipótese do tempo exponencial seja falsa.
fonte
Este post lida com os limites superiores no SAT. Este um lida com melhores limites inferiores. Este link fornece detalhes da competição anual comparando as implementações do SAT Solver, todas disponíveis para download. Para simplificar, você pode começar com o SAT4J , uma biblioteca baseada em Java para solução de SAT.
fonte
O melhor algoritmo determinístico para o 3-SAT agora tem o limite superior 1.32793 ^ n, consulte https://arxiv.org/abs/1804.07901 por Sixue Liu. Basicamente, os limites superiores para todo o k-SAT foram aprimorados neste documento.
fonte