RA2010: Investigación en lógica computacional

PorJosé A. Alonso

Las clases de esta semana del curso de Razonamiento automático se han sustituido por las conferencias de las Jornadas de Lógica, Computación e Inteligencia Artificial

En dichas Jornadas, he presentado las investigaciones en Lógica
computacional realizadas por el Grupo de Lógica Computacional de la Universidad de Sevilla.

El título de la presentación fue Lógica Computacional en Sevilla (30 años en una hora).
Read More “RA2010: Investigación en lógica computacional”

Extending Clause Learning of SAT Solvers with Boolean Gröbner Bases

PorJosé A. Alonso

Se ha publicado recientemente el artículo Extending Clause Learning of SAT Solvers with Boolean Gröbner Bases.

En el artículo se presenta una forma de combinar sistemas SAT (basados en el algoritmo DPLL) y bases de Gröbner de forma que cuando se encuentran conflictos, el aprendizaje de las nuevas cláusulas se realice mediante bases de Gröbner en lugar de hacerlo por resolución.

Para experimentar la propuesta, han creado el sistema MiniSat+GB en el que integran el sistema MiniSat con la librería para el cálculo de bases de Gröbner del sistema de cálculo simbólico Reduce.

En los resultados de los experimentos se observa cómo MiniSat+GB supera en eficiencia a MiniSat en los casos en los que se requiere más tiempo de cómputo.

Los autores del artículo son Christoph Zengler y Wolfgang Küchlin que son miembros del Grupo de cálculo simbólico de la Universidad de Tubinga (Tübingen en alemán), Alemania.

El artículo se ha publicado en el LNCS 6244: Computer Algebra in Scientific Computing. (12th International Workshop, CASC 2010)