Libro de recetas para codificaciones SAT?

Los solucionadores de SAT se están volviendo cada vez más eficientes en la resolución de grandes instancias y se están utilizando como back-end en varios contextos. Cada vez que uno quiere usarlos para resolver un problema en un dominio específico, tiene que encontrar una codificación ad-hoc que no solo tenga el conjunto correcto de soluciones, sino que también ponga las restricciones (incluso redundantes) en una forma eso ayuda a la heurística de los solucionadores a encontrar una solución más rápido.

Muchas de estas codificaciones me parecen muy comunes, por ejemplo: afirmar que un conjunto finito de nodos está vinculado como un árbol, o como un DAG, o se ordena una lista ...

¿Existe un repositorio / libro de recetas de codificaciones comunes para problemas comunes con soluciones optimizadas?

Hace unos años leí una encuesta que parece relevante, " Técnicas de codificación SAT exitosas " de Magnus Björk.

Resumen:

Este artículo identifica buenas prácticas para las codificaciones SAT mediante el análisis de entrevistas con varios expertos SAT conocidos. El propósito es tanto determinar la confianza en diferentes estrategias de codificación mediante el análisis de si existe un consenso entre los expertos o no, así como también brindar conocimiento oculto a los usuarios de SAT.

Existe consenso en que las técnicas de codificación generalmente tienen un impacto dramático en la eficiencia del solucionador SAT, que a menudo se necesita mucho trabajo para encontrar una buena codificación, y que el tamaño de una búsqueda se relaciona muy poco con la dureza de encontrar una solución. . Los temas en los que los entrevistados no están de acuerdo incluyen la posibilidad de incluir la aritmética en los problemas del SAT y si se deben formular problemas como cláusulas o circuitos.

El artículo describe una serie de estrategias que son buenas en diferentes situaciones, como diferentes formas de representar números y cómo usar la incrementalidad.

Siempre es una buena idea consultar primero el Manual de satisfacción [1] (supongo que no está disponible de forma gratuita, lo siento). Aquí, el Capítulo 2 se titula "Codificaciones CNF". Por lo menos, el libro proporciona referencias bibliográficas sobre el estado del arte en el momento de la escritura, y puede ampliar su búsqueda a través de ellas.

Además, aquí y aquí hay dos diapositivas recientes sobre el preprocesamiento SAT. Las diapositivas ofrecen una visión general concisa de las técnicas de preprocesamiento y también referencias adicionales. La idea es que en lugar de intentar modelar "manualmente" el problema de una manera eficiente, simplemente modelarlo de la manera más fácil, presionar go, y un software le proporciona una codificación eficiente.

[1] Biere, Armin, Marijn Heule y Hans van Maaren, eds. Manual de satisfacción. Vol. 185. IOS Press, 2009.

no es exactamente una respuesta directa, sino otro ángulo cada vez más estrechamente relacionado: parte de esto está cubierto por un área de investigación relativamente nueva conocida como SMT, Satisfiability Modulo Theories . La idea básica es combinar codificaciones de problemas (por ejemplo, aritmética de enteros, gráficos, etc.) en el solucionador SAT, pero también usar / aprovechar el conocimiento adicional que proviene de este acoplamiento para construir algoritmos de solución más avanzados. Heres una encuesta. Como se señaló, pueden ser mucho más eficientes que combinar un mecanismo de codificación ad-hoc con solucionadores SAT estándar.

• Teorías del módulo de satisfacción: un aperitivo / Leonardo de Moura y Nikolaj Bjørner

  Las Teorías del Módulo de Satisfacción (SMT) se trata de verificar la capacidad de las fórmulas lógicas sobre una o más teorías. El problema se basa en una combinación de algunas de las áreas más fundamentales de la informática. Combina el problema de la satisfacción booleana con dominios, como los estudiados en optimización convexa y sistemas simbólicos de manipulación de términos. También se basa en los problemas más prolíficos en el siglo pasado de la lógica simbólica: el problema de decisión, la integridad y la incompletitud de las teorías lógicas, y finalmente la teoría de la complejidad. El problema de combinar modularmente algoritmos de propósito especial para cada dominio es tan profundo e intrigante como encontrar nuevos algoritmos que funcionen particularmente bien en el contexto de una combinación. SMT también disfruta de un papel muy útil en la ingeniería de software. Software moderno, El análisis de hardware y las herramientas basadas en modelos son sistemas de software cada vez más complejos y multifacéticos. Sin embargo, en su núcleo es invariablemente un componente que utiliza lógica simbólica para describir estados y transformaciones entre ellos. Un solucionador SMT bien sintonizado que tiene en cuenta los avances más avanzados generalmente escala órdenes de magnitud más allá de los solucionadores ad-hoc personalizados.