gophersat
1.0.0
Este es Gophersat, un solucionador SAT y pseudobooleano escrito exclusivamente en Go. Gophersat fue desarrollado por el CRIL (Centre de Recherche en Informatique de Lens) de la Universidad de Artois y el CNRS. Se publica bajo la licencia MIT. Gophersat es bastante eficiente, es decir, en las pruebas típicas del SAT funciona entre 2 y 5 veces más lento que los solucionadores de alto nivel (es decir, glucosa o minisat) en los que está fuertemente inspirado. También puede resolver problemas de MAXSAT y problemas de optimización y decisión pseudobooleanos.
La última versión estable de Gophersat es la versión 1.4. Incluye la estrategia opcional de resolución de planos de corte.
Algunos problemas, como el famoso problema del casillero, requieren mucho tiempo para resolverse mediante razonamiento lógico puro.
El problema de los casilleros se puede expresar de esta manera: ¿es posible poner n palomas en m casilleros, donde m = n-1, sin poner varias palomas en el mismo hoyo y poner todas las palomas en un hoyo? La respuesta es obvia: si tienes 4 palomas en 3 hoyos, no puedes ponerlas todas en un hoyo diferente. ¿Pero cómo se prueba esto? Un solucionador SAT o PB lo demostrará probando todas las combinaciones posibles, y el número de combinaciones posibles crece exponencialmente. Por lo tanto, intentar resolver el problema con n=20 no es factible en la práctica, a pesar de que el problema tiene una respuesta obvia.
Algunos solucionadores de PB implementan una estrategia alternativa: la estrategia de planos de corte. No se describirá en detalle en este documento, pero esta estrategia puede ser extremadamente eficiente en algunos problemas, como el problema del casillero, que no se puede resolver de manera eficiente mediante razonamiento lógico puro, pero será más lento en la mayoría de los problemas.
Ahora es posible utilizar los planos de corte con Gophersat. Simplemente use la opción de línea de comando -cp . Entonces, en lugar de llamar:
gophersat problem.opb
Sólo llama:
gophersat -cp problem.opb
La última versión estable de Gophersat es la 1.3. Es una actualización menor, que agrega la capacidad de acceder al solucionador subyacente cuando se trata de problemas de MAXSAT.
La versión 1.2 de Gophersat incluye una forma de comprender las instancias UNSAT, proporcionando certificados RUP cuando un problema es UNSAT y brindando la capacidad de extraer subconjuntos insatisfactorios de la fórmula. También se corrigieron algunos errores y se mejoró el soporte para la resolución incremental de SAT.
Para conocer más sobre estas funcionalidades, puedes consultar el tutorial sobre certificados UNSAT y MUS.
Para generar un certificado con el ejecutable de gophersat, simplemente llame:
gophersat -certified problem.cnf
Luego, el certificado se imprimirá en la salida estándar, utilizando la notación RUP. El certificado se genera sobre la marcha, así que tenga en cuenta que se generará un certificado parcial e inútil incluso si el problema es realmente satisfactorio. Esta es una práctica común en la comunidad, y aunque las cláusulas generadas son ruido inútil, en la práctica esto no es un problema.
Para extraer un MUS de una instancia UNSAT, simplemente llame:
gophersat -mus problem.cnf
El MUS se imprimirá en la salida estándar. Si el problema no es UNSAT, se mostrará un mensaje de error.
Por el momento, estas funciones sólo están disponibles para problemas puros del SAT (es decir, no para problemas pseudobooleanos).
Desde su versión 1.1, Gophersat incluye un solucionador central nuevo y más eficiente para problemas puros de SAT y un paquete que trata problemas de MAXSAT. También incluye una nueva API para optimización y recuento de modelos, donde se escriben nuevos modelos en los canales tan pronto como se encuentran.
Desde la versión 1.0, la API de Gophersat se considera estable, lo que significa que se garantiza que la API seguirá siendo compatible con versiones anteriores hasta un cambio importante de versión. En otras palabras, si su programa funciona con la versión 1.0 de gophersat, seguirá funcionando con la versión 1.1 o superior, pero no necesariamente con las versiones superiores a la 2.0.
Tenga en cuenta que, por "seguir funcionando", solo queremos decir "compilará y producirá el mismo resultado", no "tendrá el mismo rendimiento en cuanto a memoria o tiempo". Esta es una distinción importante: durante las actualizaciones de versiones menores, se pueden introducir nuevas heurísticas o tipos de datos, lo que significa que algunos problemas determinados podrían resolverse más rápido o más lento que antes.
go get github.com/crillab/gophersat && go install github.com/crillab/gophersat
Gophersat se puede utilizar como solucionador independiente (leyendo archivos DIMACS CNF) o como biblioteca en cualquier programa go.
Para resolver un archivo DIMACS, puedes llamar a gophersat con la siguiente sintaxis:
gophersat --verbose file.cnf
donde --verbose es un parámetro opcional que hace que el solucionador muestre información durante el proceso de resolución.
Gophersat también es capaz de leer y resolver fórmulas booleanas más generales, no sólo problemas representados en el formato DIMACS, poco amigable para el usuario. También trata de forma nativa con restricciones de cardinalidad, es decir, cláusulas que deben tener al menos n literales verdaderos, con n > 1.
Gophersat se puede utilizar como solucionador independiente (leyendo archivos OPB) o como biblioteca en cualquier programa go.
Para resolver un problema pseudobooleano (ya sea de decisión o de optimización), puede llamar a gophersat con la siguiente sintaxis:
gophersat --verbose file.opb
donde --verbose es un parámetro opcional que hace que el solucionador muestre información durante el proceso de resolución.
Por el momento, sólo puede resolver los llamados problemas DEC-SMALLINT-LIN y OPT-SMALLINT-LIN, es decir, problemas de decisión (hay solución o no), para restricciones lineales (una suma de literales ponderados) sobre números enteros pequeños. (n < 2^30), o problemas de optimización (cuál es la mejor solución, minimizando una función de costo dada), para restricciones lineales en números enteros pequeños.
Gracias al paquete maxsat , Gophersat ahora puede resolver problemas de MAXSAT.
Para resolver un problema MAXSAT ponderado, puede llamar a gophersat con la siguiente sintaxis:
gophersat --verbose file.wcnf
donde --verbose es un parámetro opcional que hace que el solucionador muestre información durante el proceso de resolución. Se supone que el archivo está representado en (el formato WCNF) [http://www.maxsat.udl.cat/08/index.php?disp=requirements].
SAT, que significa problema booleano de satisfacción , es el problema canónico NP-completo, es decir, un problema para el que no existe una solución conocida que no requiera un tiempo exponencial en el peor de los casos. En pocas palabras, un solucionador SAT intenta encontrar, para una fórmula proposicional dada, una asignación para todas sus variables que la haga verdadera, si tal asignación existe.
Si bien es trivial implementar un solucionador SAT utilizando un algoritmo ingenuo, dicha implementación sería muy ineficiente en la práctica. Gophersat implementa funciones de última generación y, por lo tanto, es bastante eficiente, lo que lo hace utilizable en la práctica en programas Go que necesitan un motor de inferencia eficiente.
Aunque esta no siempre es la mejor decisión por razones prácticas, cualquier problema NP completo puede traducirse como un problema SAT y resolverse con Gophersat. Dichos problemas incluyen el problema del viajante, la programación de restricciones, el problema de la mochila, la planificación, la verificación del modelo, la verificación de la corrección del software, etc.
Puede encontrar más información sobre el problema del SAT en el artículo de Wikipedia sobre el SAT.
También puedes encontrar información sobre cómo representar tus propias fórmulas booleanas para que gophersat pueda usarlas en el tutorial "SAT para noobs".
MAXSAT es el equivalente de optimización del problema de decisión SAT. Mientras que un solucionador SAT puro devolverá un modelo que satisfaga todas las cláusulas o UNSAT si no existe dicho modelo, un solucionador MAXSAT devolverá un modelo que satisfaga tantas cláusulas como sea posible.
Hay extensiones para MAXSAT.
MAXSAT parcial significa que, aunque queremos satisfacer tantas cláusulas como sea posible, algunas cláusulas (llamadas cláusulas duras ) deben cumplirse, pase lo que pase. Por tanto, un problema MAXSAT parcial puede declararse insatisfactorio.
Por ejemplo, generar un horario para una escuela es un problema parcial de MAXSAT: los hay tanto blandos (queremos tener la menor cantidad posible de clases que comiencen después de las 4 de la tarde, por ejemplo) como difíciles (dos profesores no pueden estar en dos lugares diferentes al mismo tiempo). al mismo tiempo) restricciones.
MAXSAT ponderado significa que las cláusulas están asociadas a un coste: aunque son opcionales, algunas cláusulas se consideran más importantes que otras. Por ejemplo, si la cláusula C1 tiene un costo de 3 y las cláusulas C2 y C3 tienen un costo de 1, una solución que satisfaga C1 pero ni C2 ni C3 se considerará mejor que una solución que satisfaga C2 y C3 pero no C1, todas las demás. en igualdad de condiciones.
MAXSAT ponderado parcialmente significa que hay cláusulas blandas y duras en el problema, y las cláusulas blandas están ponderadas. En este sentido, MAXSAT "puro" es un caso particular del MAXSAT ponderado parcial más genérico: un problema MAXSAT "puro" es un problema MAXSAT ponderado parcial donde todas las cláusulas son cláusulas blandas asociadas con un peso de 1.
Los problemas pseudobooleanos son, en cierto modo, una generalización de los problemas SAT: cualquier cláusula proposicional se puede escribir como una única restricción pseudobooleana, pero representar una restricción pseudobooleana puede requerir un número exponencial de cláusulas proposicionales.
Una expresión pseudobooleana (lineal) es una expresión como:
w1 l1 + w2 x2 + ... + wn xn ≥ y
donde y y todos wi son constantes enteras y todos li son literales booleanos.
Por ejemplo, para que la siguiente expresión sea verdadera
2 ¬x1 + x2 + x3 ≥ 3
la variable booleana x1 debe ser falsa y al menos uno de x2 y x3 debe ser verdadero. Esto es equivalente a la fórmula proposicional.
¬x1 ∧ (x2 ∨ x3)
Las expresiones pseudobooleanas son una generalización de cláusulas proposicionales: cualquier cláusula
x1 ∨ x2 ∨ ... ∨ xn
se puede reescribir como
x1 + x2 + ... + xn ≥ 1
La descripción de un problema pseudobooleano puede ser exponencialmente más pequeña que su contraparte proposicional, pero la resolución de un problema psudobooleano sigue siendo NP-completa.
Gophersat resuelve tanto problemas de decisión (¿existe alguna solución para el problema) como problemas de optimización? Un problema de optimización es un problema pseudobooleano asociado con una función de costos, es decir, una suma de términos que deben minimizarse. En lugar de simplemente intentar encontrar un modelo que satisfaga las restricciones dadas, gophersat intentará encontrar un modelo que garantice satisfacer las restricciones y minimizar la función de costos.
Durante la búsqueda de soluciones óptimas, gophersat proporcionará soluciones subóptimas (es decir, soluciones que resuelven todas las restricciones pero aún no se garantiza que sean óptimas) tan pronto como las encuentre, de modo que el usuario pueda obtener una solución subóptima en un tiempo determinado límite o esperar más tiempo para obtener la solución óptima garantizada.
Sí y no. Es mucho más rápido que las implementaciones ingenuas, lo suficientemente rápido como para usarse en problemas del mundo real, pero más lento que los solucionadores de última generación, altamente optimizados y de alto nivel.
Gophersat no pretende ser el solucionador SAT/PB más rápido disponible. El objetivo es dar acceso a las tecnologías SAT y PB a los gophers, sin recurrir a interfaces para solucionadores escritos en otros lenguajes (normalmente C/C++).
Sin embargo, en algunos casos, interactuar con un solucionador escrito en otro idioma es la mejor opción para su aplicación. Si tiene muchos pequeños problemas que resolver, Gophersat será la alternativa más rápida. Para problemas mayores, si desea tener la menor cantidad de dependencias posible a expensas del tiempo de resolución, Gophersat también es bueno. Si necesita resolver problemas difíciles y no le importa usar cgo o utilizar un programa externo, Gophersat probablemente no sea la mejor opción.
Hay algunos otros solucionadores de SAT en Go, principalmente go-sat y gini. El rendimiento de Gini está bastante a la par del Gophersat, aunque un poco más lento en promedio, según las pruebas que realizamos.
Gophersat también proporciona características interesantes que no siempre están disponibles con otros solucionadores (un formato de entrada fácil de usar, por ejemplo), por lo que puede usarse como una herramienta para describir y resolver problemas NP-difíciles que pueden reducirse fácilmente a un SAT/PB. problema.
No. El paquete bf (para "fórmula booleana") proporciona funciones para traducir cualquier fórmula booleana a CNF.
Esto se conoce como recuento de modelos y sí, existe una función para eso: solver.Solver.CountModels .
También puedes contar modelos desde la línea de comando, con
gophersat --count filename
donde nombre de archivo puede ser un archivo .opb o .cnf.
