Davis y Putman es lineal para Horn-SAT y cuadrático para 2-SAT

  • Gonzalo Escalada Imaz Institute of Scientific Research Spanish Council
  • Nelson Becerra Correa Institute of Scientific Research Spanish Council

Resumen (es_ES)

El esquema de Davis y de Putnam (D&P) se ha estudiado intensivamente durante la última década. Hoy en día, sus buenos resultados empíricos son conocidos. Este artículo se ocupará especialmente de su componente teórico, el cual se ha estudiado relativamente menos hasta este momento. Se propone un algoritmo de D&P que sea lineal para Horn-SAT y cuadrático para 2-SAT; en consecuencia, el algoritmo de D&P diseñado de acuerdo con el problema general SAT corre casi tan rápido (en términos de complejidad) como los algoritmos especializados, diseñados para trabajar exclusivamente con una subclase SAT específica. El algoritmo se ha puesto en ejecución y se ha comparado con solvers muy conocidos para varias subclases de instancias SAT.

Descargas

La descarga de datos todavía no está disponible.

Biografía del autor/a

Gonzalo Escalada Imaz, Institute of Scientific Research Spanish Council
Físico. Ingeniero Informatico. PhD en Ciencias de la Computación. Professor of the Artificial Intelligence Research, Institute of Scientific Research Spanish Council. Barcelona.
Nelson Becerra Correa, Institute of Scientific Research Spanish Council
Ingeniero de sistemas. Magíster en ingeniería de Sistemas. Candidato a doctor en Inteligencia Artificial. Docente de la Universidad Distrital Francisco José de Caldas adscrito a la Facultad Tecnológica. Investigador de Artificial Intelligence Research Institute of Scientific Research Spanish Council CSIC.  Barcelona.
Cómo citar
Escalada Imaz, G., & Becerra Correa, N. (2004). Davis y Putman es lineal para Horn-SAT y cuadrático para 2-SAT. Tecnura, 7(14), 57-67. https://doi.org/10.14483/22487638.6192
Publicado: 2004-01-01