25 May, 2016

Reconocimiento internacional de la tecnología Barcelogic

La tecnología Barcelogic continúa recibiendo un notable reconocimiento internacional en forma de premios y otras muestras de interés.

La mejor investigación, mundialmente, en confección de horarios

La mejores herramientas software para la confección de horarios compiten periódicamente en la International Timetabling Competition (ITC). Recientemente hemos aplicado la tecnología Barcelogic sobre los problemas utilizados en la última (2008) competición. Usando nuestras herramientas totalmente automáticas, hemos mejorado, en poco tiempo de cálculo, una parte substancial de las mejores soluciones conocidas para estos problemas, lo cual ha sido reconocido en, por ejemplo, la página web de confección de horarios (seleccione la formulación “UD2 International Timetabling Competition, ITC”).

SAT Modulo Theories (SMT)

Uno de los ingredientes esenciales de la tecnología Barcelogic es SMT, una metodología basada en lógica que ha sido extraordinariamente útil para la verificación de hardware y de software. Nuestro enfoque DPLL(T) para SMT ha sido publicado en el Journal of the ACM (Nov. 2006), probablemente la revista más prestigiosa en Informática, y se ha convertido en un estándar de facto. Debido al interés que ha despertado el DPLL(T), Robert Nieuwenhuis ha recibido invitaciones como conferenciante invitado en diversos congresos internacionales.

Barcelogic ha ganado diversas categorías principales en las competiciones internacionales de SMT de 2005200620072008 y 2009, compitiendo contra grupos experimentados de empresas y universidades de Europa y de los Estados Unidos, como Microsoft o SRI International.

 

Satisfacción de fórmulas en lógica proposicional (SAT)

Otra tecnología fundamental para Barcelogic es la Satisfacción de fórmulas en lógica proposicional (SAT), que también es usada extensamente en la verificación de hardware y de programas. Los mejores SAT solvers participan cada dos años en la SAT-Race. La última SAT-Race mundial se celebró en 2008 en Guangzhou, China, donde Barcelogic acabó en tercer lugar. Pero, lo que es más importante, Barcelogic fue el mejor del mundo en problemas insatisfactibles, que es lo que importa más en aplicaciones de optimización.

Había más de 50 participantes, de los cuales 19 se clasificaron para la final. Aproximadamente la mitad de ellos fueron desarrollados en la industria (incluyendo equipos de Intel y de Microsoft) y el resto provenía de centros de investigación y universidades. El ganador, MiniSAT, fue desarrollado por investigadores de Cadence Berkeley, USA, y la universidad de Chalmers de Suecia. Véanse los resultados aquí. Véase también una explicación de prensa sobre la importancia práctica de SAT.