Os solucionadores SAT são muito importantes em ataques algébricos , por exemplo, walkinsat e minisat .
No entanto, ao resolver os problemas de benchmark disponíveis aqui, há uma enorme diferença de desempenho entre os dois - o Walksat é muito mais rápido que o minisat para esses problemas. Por que é isso?
Essa implementação do walkSat parece ter algumas melhorias de desempenho - existe algum motivo para não ter sido incluído nas competições internacionais do SAT ?
ds.algorithms
sat
ir01
fonte
fonte
Respostas:
Sim, há uma grande diferença entre o MiniSAT e o WalkSAT. Primeiro, vamos esclarecer: MiniSAT é uma implementação específica da classe genérica de algoritmos DPLL / CDCL que usa backtracking e aprendizado de cláusulas, enquanto WalkSAT é o nome geral de um algoritmo que alterna entre etapas gananciosas e etapas aleatórias.
Em geral, o DPLL / CDCL é muito mais rápido nas instâncias SAT estruturadas, enquanto o WalkSAT é mais rápido no k-SAT aleatório . Instâncias SAT industriais e aplicadas tendem a ter muita estrutura; portanto, o DPLL / CDCL é dominante na maioria dos solucionadores SAT modernos. Porém, uma instância de uma técnica pode vencer, e essa é uma das razões pelas quais os solucionadores de portfólio se tornaram populares.
Levo muitos problemas com a sua alegação de que o WalkSAT é muito mais rápido que o MiniSAT nas instâncias dessa página. Por um lado, existem gigabytes de instâncias SAT - em quantos você tentou compará-las? O WalkSAT não é de todo competitivo nas instâncias mais estruturadas, e é por isso que não é visto com frequência nas competições.
Em uma nota lateral - Vijay está certo de que o MiniSAT ainda é relevante. Na verdade, por ser de código aberto e bem escrito, o MiniSAT é o solucionador a ser superado, a fim de mostrar que uma determinada otimização é promissora. Muitas pessoas ajustam o MiniSAT para mostrar suas otimizações - dê uma olhada na categoria "MiniSAT hack" nas recentes competições SAT.
fonte
Um bom artigo para ler sobre esse tópico é este de Nudelman et al . O objetivo principal do artigo é determinar os recursos fáceis de calcular das instâncias SAT que podem lhe dizer quais algoritmos têm provavelmente um bom desempenho e quais não. Usando essa técnica, é possível criar um algoritmo baseado em portfólio que analisará rapidamente uma instância do problema e, em seguida, resolva a instância com o algoritmo mais apropriado. Há uma progressão de trabalhos que seguem essa; pesquisando no Google SATzilla, você encontrará muitos materiais de leitura.
fonte