Home En què som bons? Analitzem el seu cas gratis Qui som? Contacte

Reconeixement internacional de la tecnologia Barcelogic

La tecnologia Barcelogic continua rebent un notable reconeixement internacional en forma de premis i altres mostres d'interès.

La millor investigació, a nivell mundial, en confecció d'horaris

Les millores eines software per a la confecció d'horaris competeixen periòdicament a la International Timetabling Competition (ITC). Recentment hem aplicat la tecnologia Barcelogic sobre els problemes utilitzats a l'última (2008) competició. Utilitzant les nostres eines, totalment automàtiques, hem millorat, en poc temps de càlcul, una part substancial de les millors solucions conegudes per aquests problemes, fet que ha estat reconegut, per exemple, a la pàgina web de confecció d'horaris (seleccioni la formulació "UD2 International Timetabling Competition, ITC").

SAT Mòdul Teories (SMT)

Un dels ingredients essencials de la tecnologia Barcelogic és SMT, una metodologia basada en lògica que ha estat extraordinàriament útil per a la verificació de hardware i de software. El nostre enfocament DPLL(T) per a SMT ha estat publicat en el Journal of the ACM, probablement la revista més prestigiosa en Informàtica, i s'ha convertit en un estàndard de facto. Degut a l'interès que ha despertat DPLL(T), Robert Nieuwenhuis ha rebut invitacions com a conferenciant convidat de diversos congressos internacionals.

Barcelogic ha guanyat diverses categories principals en les competicions internacionals de SMT de 2005, 2006, 2007, 2008, i 2009, competint contra grups experimentats d'empreses i universitats d'Europa i dels Estats Units, com Microsoft o SRI International.

Satisfacció de fórmules en lògica proposicional (SAT)

Una altra tecnologia fonamental per a Barcelogic és la Satisfacció de fórmules en lògica proposicional (SAT), que també és usada extensament en la verificació de màquines i de programes. Els millors SAT solvers participen cada dos anys a la competició internacional SAT-Race. L'última SAT-Race es va celebrar el 2008 a Guangzhou, Xina, on Barcelogic va acabar en tercer lloc. Però, el més important, Barcelogic va ser el millor del món en problemes insatisfactibles, que és el que importa més en aplicacions d'optimització.

Hi havia més de 50 participants, dels quals 19 es van classificar per a la final. Aproximadament la meitat d'ells van ser desenvolupats per companyies privades (incloent alguns equips de Microsoft i Intel), i els altres provenien de centres d'investigació i universitats. El guanyador, MiniSAT, va ser desenvolupat per investigadors de Cadence Berkeley, Estats Units, i la universitat de Chalmers de Suècia. El resultats es poden veure aquí. Vegin-se també una nota de premsa sobre la importància pràctica de SAT.

A UPC spinoff
Home En què som bons? Analitzem el seu cas gratis Qui som? Contacte	Reconeixement internacional de la tecnologia Barcelogic La tecnologia Barcelogic continua rebent un notable reconeixement internacional en forma de premis i altres mostres d'interès. La millor investigació, a nivell mundial, en confecció d'horaris Les millores eines software per a la confecció d'horaris competeixen periòdicament a la International Timetabling Competition (ITC). Recentment hem aplicat la tecnologia Barcelogic sobre els problemes utilitzats a l'última (2008) competició. Utilitzant les nostres eines, totalment automàtiques, hem millorat, en poc temps de càlcul, una part substancial de les millors solucions conegudes per aquests problemes, fet que ha estat reconegut, per exemple, a la pàgina web de confecció d'horaris (seleccioni la formulació "UD2 International Timetabling Competition, ITC"). SAT Mòdul Teories (SMT) Un dels ingredients essencials de la tecnologia Barcelogic és SMT, una metodologia basada en lògica que ha estat extraordinàriament útil per a la verificació de hardware i de software. El nostre enfocament DPLL(T) per a SMT ha estat publicat en el Journal of the ACM, probablement la revista més prestigiosa en Informàtica, i s'ha convertit en un estàndard de facto. Degut a l'interès que ha despertat DPLL(T), Robert Nieuwenhuis ha rebut invitacions com a conferenciant convidat de diversos congressos internacionals. Barcelogic ha guanyat diverses categories principals en les competicions internacionals de SMT de 2005, 2006, 2007, 2008, i 2009, competint contra grups experimentats d'empreses i universitats d'Europa i dels Estats Units, com Microsoft o SRI International. Satisfacció de fórmules en lògica proposicional (SAT) Una altra tecnologia fonamental per a Barcelogic és la Satisfacció de fórmules en lògica proposicional (SAT), que també és usada extensament en la verificació de màquines i de programes. Els millors SAT solvers participen cada dos anys a la competició internacional SAT-Race. L'última SAT-Race es va celebrar el 2008 a Guangzhou, Xina, on Barcelogic va acabar en tercer lloc. Però, el més important, Barcelogic va ser el millor del món en problemes insatisfactibles, que és el que importa més en aplicacions d'optimització. Hi havia més de 50 participants, dels quals 19 es van classificar per a la final. Aproximadament la meitat d'ells van ser desenvolupats per companyies privades (incloent alguns equips de Microsoft i Intel), i els altres provenien de centres d'investigació i universitats. El guanyador, MiniSAT, va ser desenvolupat per investigadors de Cadence Berkeley, Estats Units, i la universitat de Chalmers de Suècia. El resultats es poden veure aquí. Vegin-se també una nota de premsa sobre la importància pràctica de SAT.