minisat
Solucionador SAT rápido y ligero. A pesar de la completitud NP del problema de satisfacibilidad de fórmulas booleanas (SAT), los solucionadores SAT suelen ser capaces de resolver este problema en un plazo razonable. Un solucionador es un programa o algoritmo que, dado un problema específico, busca encontrar una solución que cumpla ciertas condiciones. En el contexto de la informática y la lógica, un solucionador toma una fórmula o conjunto de restricciones y determina si existe una asignación de valores o variables booleanas que hagan verdadera una fórmula lógica. Un ejemplo de uso:
$ nano formula.cnf
p cnf 3 2
1 -2 0
2 3 0
p cnf 3 2 --> indica que hay 3 variables y 2 cláusulas.
La primera cláusula --> 1 -2 0 (x1 OR NOT x2)
La segunda cláusula --> 2 3 0` (x2 OR x3)
$ minisat formula.cnf resultado.out
La pantalla mostrar un salida amplia pero el archivo resultado.out:
SAT
1 -2 3 0