Como mencionó Pasquale, los solucionadores de las Teorías del módulo de satisfacción (SMT) son
Un buen ejemplo. Son extensiones de solucionadores de SAT a otras cosas que no sean lógica booleana pura (llamadas “teorías”). Como ejemplos particulares, podemos tener teorías para cosas como vectores de bits, enteros (sin límites), matrices o incluso números algebraicos. Esto significa que los solucionadores SMT pueden trabajar con fórmulas y restricciones sobre todos estos tipos diferentes: puede resolver variables en fórmulas que involucran cosas como números, etc.
A diferencia de los solucionadores SAT, los solucionadores SMT tienen una amplia gama de capacidades. Casi todos los solucionadores SMT pueden usar un conjunto diferente de primitivas y operaciones, lo que le permite resolver diferentes tipos de problemas. Los solucionadores particularmente populares son Z3 de Microsoft y Yices de SRI (de hecho, ¡ambos fueron escritos en gran parte por la misma persona!).
También hay solucionadores SMT que son muy especializados. Por ejemplo, Boolector solo funciona con bitvectors. Por un lado, esto significa que es mucho menos capaz que algo como Z3; Por otro lado, es realmente rápido para los vectores de bits. Otro ejemplo es el solucionador de croquis de Berkeley, que está muy ajustado para trabajar con lenguajes de programación, especialmente para la síntesis de programas.
- ¿Hay alguna forma metódica (algoritmo) de crear un autómata que acepte un idioma dado, dado el idioma como un conjunto ({w | condición (w)})?
- Cómo encontrar un puente en un gráfico
- ¿Cuáles son algunas de las cosas que la mayoría de las personas que usan Linux desconocen?
- En India; ¿Cuál es la mejor GPU portátil Nvidia o AMD?
- ¿Hay una plataforma para registrarse para obtener información sobre el aprendizaje automático, conferencias, talleres, trabajos y otras actividades?
Otra tecnología relacionada son los solucionadores para la programación lineal entera (ILP) y Programación lineal de enteros mixtos (MILP). En lugar de resolver problemas lógicos, estos problemas implican resolver grandes sistemas de ecuaciones donde todas (ILP) o algunas (MILP) de las variables están restringidas a ser enteros.
Este tipo de solucionadores son útiles para todo tipo de problemas de optimización y para cosas como el diseño de hardware. Sin embargo, no son adecuados para modelar la semántica del lenguaje de programación, por lo que no estoy muy familiarizado con ellos.
Si desea una mayor generalidad a cambio de velocidad, puede consultar los lenguajes de programación lógica . La programación lógica es realmente su propio paradigma: estos lenguajes son completos de Turing y podrían usarse para programación de propósito general. Sin embargo, en mi experiencia, son relativamente inconvenientes para las tareas de programación más comunes. Sin embargo, por las cosas en las que son buenos, son realmente buenos, por lo que definitivamente vale la pena aprender. Algunos lenguajes de programación lógica populares son Prolog y Mercury, de tipo estático.
Además, algunos lenguajes pueden incluir sub-lenguajes de programación lógica (DSL integrados, realmente) como bibliotecas. Buenos ejemplos son la mónada de programación lógica de retroceso de Haskell. y Clojures core.logic. Estos le permiten utilizar la programación lógica para pequeñas partes de su programa, donde sea que tengan sentido, mientras usa un estilo funcional mucho más agradable para todo lo demás.
