Los algoritmos centrales como DPLL y sus refinamientos como CDCL son completamente deterministas.
Tenga en cuenta que el no determinismo no necesariamente significa que un algoritmo puede conducir a un resultado incorrecto. Por ejemplo podemos distinguir entre
Algoritmos de Monte Carlo , que son algoritmos aleatorios cuya salida puede ser incorrecta con cierta probabilidad.
Los algoritmos de Las Vegas , que son algoritmos aleatorios cuya salida siempre es correcta , pero los algoritmos 'juegan' con los recursos utilizados en el cálculo, por ejemplo, el tiempo de ejecución en entradas idénticas puede variar.
En el otro extremo están los algoritmos probabilísticos para resolver -SAT como el de Schöning [1], que es Monte-Carlo, y notablemente eficaz en la práctica dada su total simplicidad. Curiosamente, el algoritmo de Schöning puede ser completamente aleatorizado sin perder (gran parte) de su efectividad [2].k
En la práctica, los solucionadores de SAT industriales siempre emplean cierto grado de aleatoriedad, para "escapar" del mal comportamiento (= exponencial) en el peor de los casos de los algoritmos basados en DPLL. MiniSat es una pieza de software altamente configurable y en evolución. Dicho esto, MiniSat no es completamente determinista: la elección de la variable de ramificación a veces es aleatoria, dependiendo de las opciones de la línea de comandos. (El valor predeterminado es que el 2% de las variables de ramificación se eligen al azar IIRC.) Asimismo, MiniSAT tiene la opción de inicializar los puntajes VSIDS al azar. (VSIDS es una heurística para 'medir' la influencia que tiene una variable).
¿El algoritmo de Monte-Carlo puede decir que un problema es SAT cuando no lo es, sin una solución satisfactoria o es solo en el caso de unSAT, que el problema podría ser SAT?
Xavier Combelle
@XavierCombelle Eso dependería del algoritmo específico, aunque tengo dificultades para pensar en un algoritmo que podría equivocarse SAT. Schöning solo se equivoca unSAT.
Martin Berger
Una extensión menor: mientras MiniSat usa la aleatoriedad, no es una aleatoriedad "verdadera". Cada ejecución de MiniSat producirá la misma respuesta, en el mismo período de tiempo (si no reconfigura ninguna opción), ya que se eligen las mismas opciones "aleatorias" cada vez que se ejecuta el solucionador.
Chris Jefferson
@ChrisJefferson ¿MiniSAT no tiene una forma de especificar una semilla aleatoria?
Martin Berger
6
Eso es correcto. DPLL explora exhaustivamente el espacio. Si devuelve 'unsat', ciertamente no existe una tarea satisfactoria.
Más recientemente, los investigadores han desarrollado solucionadores de SAT de certificación que además devuelven una prueba (insatisfactoriamente corta) de insatisfacción, cuando devuelven 'insat'. Cualquier otra persona puede verificar esta prueba, lo que proporciona una forma para que otros verifiquen que la fórmula no es satisfactoria sin que tengan que volver a ejecutar el algoritmo SAT. Esto puede ser útil en algunos contextos.
MiniSAT es una implementación, más que un algoritmo. Su comportamiento depende de su código. No puedo hablar de lo que hace el código.
Todos los solucionadores DPLL / CDCL pueden ser "aumentados" para producir una prueba de insatisfacción.
Yuval Filmus
5
Una palabra clave que puede faltar es integridad . En general, se dice que un algoritmo de búsqueda está completo si encuentra una solución dado que existe (con tiempo suficiente). En particular, DPLL es un ejemplo de un método de búsqueda determinista y completo.
Los solucionadores SAT pueden ser deterministas o no dependiendo de cómo se implementen. ¡Tenga en cuenta que el no determinismo aquí solo puede afectar el modelo generado, no la respuesta (SAT o UNSAT) del solucionador! Para fines de diversificación y otros, el solucionador SAT generalmente introduce aleatoriedad en cierto punto: por ejemplo, para inicializar actividades variables o para tomar decisiones aleatorias. En minisat, por ejemplo, las decisiones aleatorias se toman llamando a una función que siempre devuelve el mismo número aleatorio cuando se usa la misma semilla aleatoria. Entonces, en este punto, cuando no cambie ninguna configuración del solucionador, siempre tendrá la misma respuesta y el mismo modelo. Cambiar la semilla aleatoria, por ejemplo, no afectará la respuesta (SAT o UNSAT) pero puede cambiar el modelo y el tiempo de ejecución.
Eso es correcto. DPLL explora exhaustivamente el espacio. Si devuelve 'unsat', ciertamente no existe una tarea satisfactoria.
Más recientemente, los investigadores han desarrollado solucionadores de SAT de certificación que además devuelven una prueba (insatisfactoriamente corta) de insatisfacción, cuando devuelven 'insat'. Cualquier otra persona puede verificar esta prueba, lo que proporciona una forma para que otros verifiquen que la fórmula no es satisfactoria sin que tengan que volver a ejecutar el algoritmo SAT. Esto puede ser útil en algunos contextos.
MiniSAT es una implementación, más que un algoritmo. Su comportamiento depende de su código. No puedo hablar de lo que hace el código.
fuente
Una palabra clave que puede faltar es integridad . En general, se dice que un algoritmo de búsqueda está completo si encuentra una solución dado que existe (con tiempo suficiente). En particular, DPLL es un ejemplo de un método de búsqueda determinista y completo.
fuente
Los solucionadores SAT pueden ser deterministas o no dependiendo de cómo se implementen. ¡Tenga en cuenta que el no determinismo aquí solo puede afectar el modelo generado, no la respuesta (SAT o UNSAT) del solucionador! Para fines de diversificación y otros, el solucionador SAT generalmente introduce aleatoriedad en cierto punto: por ejemplo, para inicializar actividades variables o para tomar decisiones aleatorias. En minisat, por ejemplo, las decisiones aleatorias se toman llamando a una función que siempre devuelve el mismo número aleatorio cuando se usa la misma semilla aleatoria. Entonces, en este punto, cuando no cambie ninguna configuración del solucionador, siempre tendrá la misma respuesta y el mismo modelo. Cambiar la semilla aleatoria, por ejemplo, no afectará la respuesta (SAT o UNSAT) pero puede cambiar el modelo y el tiempo de ejecución.
fuente