Inicio de papeles de solucionador SAT

Quiero hacer un primer solucionador SAT. Conozco la competencia SAT y la conferencia SAT, y hay tantos documentos sobre este tema. Soy un abridor, un abrumador abrumador. ¿Dónde debería comenzar? Finalmente quiero impulsar el estado del arte. Quiero un consejo experto sobre cómo comenzar, para no perder mi tiempo en lo no esencial demasiado pronto. Muchas gracias.

El siguiente artículo de 2009 ofrece una excelente visión general para principiantes.

• Satisfacción booleana: de la dureza teórica al éxito práctico , Sharad Malik, Lintao Zhang, Comunicaciones de la ACM, 2009

Hay varias formas de entrar en los aspectos técnicos. Incluso puede comenzar con el documento original de Davis-Putnam. Es extremadamente claro y tiene ejemplos detallados. Cuando discutimos las optimizaciones SAT en un curso, descubrimos que algunos pueden imaginar que ya están allí. El artículo de Davis-Logeman-Loveland es (creo) menos instructivo, pero es tan breve que es mejor leerlo.

• Un procedimiento de computación para la teoría de cuantificación , Martin Davis, Hilary Putnam, Journal of the ACM, 1960.
• Un programa de máquina para probar teoremas , Martin Davis, George Logemann, Donald Loveland, Comunicaciones de la ACM, 1962.

Hay muchas maneras de ponerse al día con los desarrollos de los próximos 50 años. Recomendaría diapositivas de conferencias. Simplemente buscando 'DPLL' arrojará muchos tutoriales. Si navega por ellos, estoy seguro de que la niebla se despejará, hasta cierto punto. También hay muchas encuestas útiles. El periódico Zhang-Malik es un buen lugar para comenzar. Hay varios artículos en el Manual de Satisfacción que pueden resultarle útiles.

• The Quest for Efficient Boolean Satisfiability Solvers , Lintao Zhang, Sharad Malik, documento conjunto invitado para CAV y CADE 2002.
• Handbook of Satisfiability , editado por Armin Biere, Marijn Heule, Hans van Maaren y Toby Walsh, 2009
• Anatomía y evaluación empírica de solucionadores modernos de SAT , Karem Sakallah, Joao Marques-Silva, Boletín de EATCS, 2011.

Secundo la sugerencia de Mikolaos. El código MiniSAT es limpio y de tamaño manejable. Puedes jugar con eso. Hay varios otros solucionadores que puedes probar. CryptoMiniSat también es bastante limpio. También debe consultar el trabajo de Armin Biere , quien escribe solucionadores SAT y escribe sobre escribir solucionadores SAT.

Sugiero que primero comprenda qué técnicas realmente avanzaron los solucionadores, para lo cual sugeriría la siguiente descripción general y análisis .

Entonces recomendaría descargar el código fuente de minisat y leer su descripción .

Por supuesto, podría ser individual, pero encontré que mirar el código fuente es muy valioso.

Si estás abrumado por todo el trabajo que hay ahí fuera, ¿por qué no empiezas fingiendo que nadie ha trabajado en el problema antes? Si su objetivo es eventualmente construir un solucionador SAT competitivo, será un viaje bastante largo. Al comenzar simplemente jugando sin 'comprobar las soluciones', por así decirlo, tiene más que ganar que perder.

$n$$m$$n$$m$

$n$$m$

Comience con una buena encuesta. Es fácil atacar al sujeto poco a poco y confundirse con diferentes nombres en la literatura para las mismas técnicas y el mismo nombre utilizado para diferentes técnicas. También es fácil volver a representar antiguas batallas algorítmicas (listas de ocurrencia frente a listas de encabezado frente a dos literales vistos para implementaciones de DPLL, por ejemplo) si no sabe cuál es el estado del arte.

Satisfiability Solvers por Gomes, et. Alabama. te dará la tosca disposición de la tierra.

Mejorar los solucionadores SAT utilizando técnicas de vanguardia de Manthey lo acercará al presente.