material sobre SAT (Boolean satisfacibilidad Problema) el aprendizaje [cerrado]

Question

¿Cuáles son buenos para leer documentos en SAT (booleano) satisfacibilidad problemas que resuelven. No he sido capaz de encontrar un buen material a través de Google. Los documentos que encontré eran o vista de pájaro, los archivos PDF corruptos demasiado avanzado o ...

¿Qué papeles / documentos recomiendas para aprender acerca de los algoritmos en modernas prácticas solucionadores SAT?

Answer 1

El página de Davis-Putnam-Logemann-Loveland Wikipedia tiene una buena visión general.

A continuación, debería ser capaz de seguir el papel MINISAT "Un extensible SAT-solucionador" .

También debe leer "GRASP - Un nuevo algoritmo de búsqueda para satisfacibilidad " para entender el algoritmo de aprendizaje conflicto impulsado utilizado en MINISAT.

yo era capaz de escribir un solucionador SAT en Python usando con bastante facilidad esos recursos. Mi sat.py código está disponible (LGPL 2.1 actualmente), pero es tan reciente todavía pueden contener errores. Carece de un par de optimizaciones del diseño MINISAT; si quieres utilización velocidad pura del código MINISAT; -)

Actualización: También he hecho una versión OCaml, sat.ml , lo que podría hacer que sea más fácil ver los tipos.

Answer 2

Un buen libro es: Uwe Schöning-; Jacobo Torán - El Problema satisfacibilidad