25 May, 2016

International recognition of the Barcelogic technology

The Barcelogic technology is receiving significant international interest, in the form of awards and other recognition.

World’s best research on timetabling

Many state-of-the-art tools participate in the International Timetabling Competitions (ITC). We recently tried Barcelogic on some challenging problems used in the last (2008) competition. Using our fully automatic tools, we improved in short computing time several of the best known solutions for these problems, which has been recognized, e.g., in the Course timetabling website (select formulation UD2 International Timetabling Competition, ITC).

SAT Modulo Theories (SMT)

SMT is one of the essential underlying ingredients of the Barcelogic technology. It has been extremely successful in software and hardware verification. Our DPLL(T) approach to SMT was published in the Journal of the ACM, (Nov. 2006), probably the most prestigious Journal in Computer Science, and has since then become a de facto standard. Due to its interest, Robert Nieuwenhuis has been an invited speaker at several international conferences.

Barcelogic has won main divisions in the international SMT Competitions of 2005200620072008, and  2009, competing against experienced groups of companies and universities from Europe and the USA, such as Microsoft or SRI International.

Propositional Satisfiability

Another main technology for Barcelogic is Propositional Satisfiability (or simply, SAT), another crucial ingredient for software and hardware verification. The world’s best industrial solvers compete every two years in the SAT-Race. The last one was held in 2008 in Guangzhou, China, where Barcelogic ranked third. But, more importantly, Barcelogic was world’s best on unsatisfiable problems, which is what matters most for optimisation applications.

There were around 50 participants, of which 19 qualified for the final. About half of them were from industry (including Intel and Microsoft teams) and the rest from universities and research centres. The winner, MiniSAT, was developed by researchers from Cadence Berkeley, USA, and Chalmers University in Sweden. See the results here. See also here a larger press explanation about the practical importance of SAT.