Si tuviera un algoritmo muy rápido y distribuido para resolver el problema 3-SAT, ¿cuáles son los mercados relevantes para este algoritmo? ¿Para qué industrias sería relevante?

Como dice Mark, debido a que 3-SAT es NP-complete, puede codificar cualquiera de una gran variedad de problemas como una instancia de 3-SAT y luego aplicar su algoritmo. Los clientes finales pagan por esta codificación y presentación. Necesitará desarrollar estas habilidades o asociarse con OEM (“fabricantes de codificación original”) que puedan empaquetar su tecnología para industrias específicas. No subestimes el tiempo que tomará hacer esta pieza correctamente.

Tampoco eres el único solucionador rápido que existe. Hay concursos activos para solucionadores SAT y para solucionadores de “teoría del módulo de satisfacción”, vea por ejemplo esta página para SMT-COMP
http://www.smtcomp.org/2010/

Los puntos de referencia SMT-COMP dan una idea de cómo se ven las diferentes instancias de problemas en diferentes aplicaciones. Puede resultarle útil ver dónde venció a la competencia en velocidad y en qué medida. Eso a su vez puede ayudar a enfocar la elección de las industrias donde primero va al mercado.

Otra cuestión clave es si vence a los demás, ¿por cuánto los vence, y es eso sostenible? Debido a que puede cambiar un solucionador por otro en una aplicación, siempre puede ser comparado directamente con sus competidores. Esto puede sugerir hacer su propia integración y codificación para su industria objetivo, porque de lo contrario un OEM tiene un bajo costo para cambiar de usted al siguiente solucionador.

Un mercado relevante viene en el desarrollo de herramientas de modelado de software, particularmente para su uso en industrias donde la corrección del software es crítica y los errores pueden costar vidas. Por ejemplo, el Grupo de Diseño de Software del MIT [1] ha creado una herramienta llamada Alloy que se basa en simuladores y verificadores basados ​​en SAT para validar invariantes o refutar afirmaciones especificadas en un sistema descrito por un lenguaje declarativo y relacional. Un solucionador SAT más rápido permitiría que dicho software de modelado ejecute análisis y simulaciones sobre modelos más grandes y también reduciría el tiempo de iteración para alguien que desarrolle un modelo. El grupo de investigación del MIT ha utilizado Alloy para modelar la exactitud del software de control de la terapia de protones en el Hospital General de Massachusetts, los sistemas de control de tráfico aéreo construidos por la NASA y el software del teléfono celular Nokia. Que yo sepa, el grupo solo ha estado usando Alloy en una capacidad de investigación, pero es probable que estos clientes estén dispuestos a gastar un porcentaje de sus presupuestos para mejorar la confianza en la corrección del software.

[1] http://sdg.csail.mit.edu/index.html
[2] http://alloy.mit.edu/

Debido a que 3-SAT es NP-Complete, ahora tiene la capacidad de resolver presumiblemente cualquier NP-Complete de una “manera muy rápida y distribuida”. Cualquiera de los otros problemas de zillion NP-Complete tendrá una transformación de tiempo polinomial a 3-SAT, lo que significa que resolverlos puede aprovechar su bondad.

Así que comience a buscar grandes empresas que gasten mucho dinero en cosas como programar recursos de transporte, diseñar placas de circuitos, administrar rutas de red. Muchas buenas aplicaciones, y de hecho este podría ser un caso en el que el mundo realmente abriría el camino a su puerta.

– Marca