Algoritmos básicos como DPLL e seus refinamentos como CDCL são completamente determinísticos.
Observe que o não determinismo não significa necessariamente que um algoritmo pode levar a um resultado errado. Por exemplo, podemos distinguir entre
Algoritmos de Monte Carlo , que são algoritmos aleatórios cuja saída pode estar incorreta com alguma probabilidade.
Os algoritmos de Las Vegas , que são algoritmos aleatórios cuja saída está sempre correta , mas os algoritmos 'jogam' com os recursos usados na computação, por exemplo, o tempo de execução em entradas idênticas pode variar.
No outro extremo estão os algoritmos probabilísticos para resolver o SAT, como o de Schöning [1], que é Monte-Carlo, e notavelmente eficaz na prática, devido à sua total simplicidade. O interessante é que o algoritmo de Schöning pode ser completamente des randomizado sem perder (grande parte) sua eficácia [2].k
Na prática, os solucionadores de SAT industriais sempre empregam algum grau de aleatoriedade, de modo a "escapar" do mau comportamento (= exponencial) do pior caso dos algoritmos baseados em DPLL. O MiniSat é um software altamente configurável e em evolução. Dito isto, o MiniSat não é completamente determinístico: a escolha da variável de ramificação às vezes é aleatória, dependendo das opções da linha de comando. (O padrão é que 2% das variáveis de ramificação sejam escolhidas aleatoriamente IIRC.) Da mesma forma, o MiniSAT tem a opção de inicializar as pontuações do VSIDS aleatoriamente. (O VSIDS é uma heurística para 'medir' a influência que uma variável tem.)
o algoritmo de monte-carlo pode dizer que um problema é SAT quando não é, sem solução de satisfação ou é apenas no caso da unSAT, que o problema pode ser SAT?
Xavier Combelle
@XavierCombelle Isso dependeria do algoritmo específico, embora eu tenha dificuldade em pensar em um algoritmo que possa dar errado no SAT. A Schöning's errou apenas o UNSAT.
Martin Berger
Uma extensão menor - enquanto o MiniSat usa aleatoriedade, não é uma aleatoriedade "verdadeira". Cada execução do MiniSat produzirá a mesma resposta, na mesma quantidade de tempo (se você não reconfigurar nenhuma opção), pois as mesmas opções "aleatórias" serão escolhidas toda vez que o solucionador for executado.
Chris Jefferson
@ChrisJefferson O MiniSAT não tem como especificar uma semente aleatória?
18717 Martin-Berger
6
Está correto. A DPLL explora exaustivamente o espaço. Se retornar 'unsat', certamente não existe uma tarefa satisfatória.
Mais recentemente, os pesquisadores desenvolveram solucionadores de certificação SAT que, além disso, retornam uma (esperançosamente curta) prova de insatisfação, quando retornam 'insat'. Essa prova pode ser verificada por qualquer outra pessoa, o que fornece uma maneira de outras pessoas verificarem se a fórmula é insatisfatória sem que elas precisem executar novamente o algoritmo SAT. Isso pode ser útil em alguns contextos.
MiniSAT é uma implementação, e não um algoritmo. Seu comportamento depende do seu código. Não posso falar com o que o código faz.
Todos os solucionadores DPLL / CDCL podem ser "aumentados" para produzir uma prova de insatisfação.
Yuval Filmus
5
Uma palavra-chave que você pode estar perdendo é a integridade . Em geral, um algoritmo de busca é considerado completo se encontrar uma solução, desde que exista (com tempo suficiente). Em particular, DPLL é um exemplo de um método de pesquisa completo e determinístico.
Os solucionadores de SAT podem ser determinísticos ou não, dependendo de como eles são implementados. Observe que o não determinismo aqui pode afetar apenas o modelo gerado e não a resposta (SAT ou UNSAT) do solucionador! Para fins de diversificação e outros, o solucionador SAT geralmente introduz a aleatoriedade em determinado ponto: por exemplo, para inicializar atividades variáveis ou para tomar decisões aleatórias. No minisat, por exemplo, decisões aleatórias são tomadas chamando uma função que sempre retorna o mesmo número aleatório ao usar a mesma semente aleatória. Portanto, nesse ponto, quando você não altera nenhuma configuração do solucionador, sempre terá a mesma resposta e o mesmo modelo. Alterar a semente aleatória, por exemplo, não afetará a resposta (SAT ou UNSAT), mas poderá alterar o modelo e o tempo de execução.
Está correto. A DPLL explora exaustivamente o espaço. Se retornar 'unsat', certamente não existe uma tarefa satisfatória.
Mais recentemente, os pesquisadores desenvolveram solucionadores de certificação SAT que, além disso, retornam uma (esperançosamente curta) prova de insatisfação, quando retornam 'insat'. Essa prova pode ser verificada por qualquer outra pessoa, o que fornece uma maneira de outras pessoas verificarem se a fórmula é insatisfatória sem que elas precisem executar novamente o algoritmo SAT. Isso pode ser útil em alguns contextos.
MiniSAT é uma implementação, e não um algoritmo. Seu comportamento depende do seu código. Não posso falar com o que o código faz.
fonte
Uma palavra-chave que você pode estar perdendo é a integridade . Em geral, um algoritmo de busca é considerado completo se encontrar uma solução, desde que exista (com tempo suficiente). Em particular, DPLL é um exemplo de um método de pesquisa completo e determinístico.
fonte
Os solucionadores de SAT podem ser determinísticos ou não, dependendo de como eles são implementados. Observe que o não determinismo aqui pode afetar apenas o modelo gerado e não a resposta (SAT ou UNSAT) do solucionador! Para fins de diversificação e outros, o solucionador SAT geralmente introduz a aleatoriedade em determinado ponto: por exemplo, para inicializar atividades variáveis ou para tomar decisões aleatórias. No minisat, por exemplo, decisões aleatórias são tomadas chamando uma função que sempre retorna o mesmo número aleatório ao usar a mesma semente aleatória. Portanto, nesse ponto, quando você não altera nenhuma configuração do solucionador, sempre terá a mesma resposta e o mesmo modelo. Alterar a semente aleatória, por exemplo, não afetará a resposta (SAT ou UNSAT), mas poderá alterar o modelo e o tempo de execução.
fonte