Tools of the ICCL have received first prizes in several international competitions

News from the research group Knowledge Representation and Reasoning of October 9, 2015

Tools of the ICCL have received first prizes in several international competitions

In the era of Industry 4.0 and automation more and more combinatorial tasks have to be solved automatically, and hence actual systems become more complex as well.

Hence, research focusses on efficient decision procedures - here so called SAT solvers - that can be used to show that correctness and reliability of the use programs and machines. SAT solvers can be used for example to check circuits for faulty states, to create good rail ways schedules, to optimize the workflow in manufactories or to find bugs in software systems. For these tasks, a SAT solvers is given a huge specification for which it either states that the system works correctly, or it points out a specific case of misbehavior.

The SAT solver "Riss" is developped by Norbert Manthey in the knowledge representation and reasoning group for 5 years now, where student projects are also integrated into the system or related software packages. In three SAT related international competitions, which cover major application areas of SAT solver, the group showed that it is quite competitive on an international level. The good results live up to the success of the previous years.

In the hardware model checking competition model checkers have to prove correctness of a circuit or have show a counter example for this correctness. For circuits that are to difficult to be proven, there is another track: showing that a faulty state cannot be reached as long as possible. This track has been won by the model checker "ShiftBMC" of the group.

In the SAT Race, this years version of the bi-yearly SAT competition with moderate timeouts and a focus on industrial problems. An important feature of a succesful system is to be able to adapt to the given problem, as the number of applications for SAT solvers increases every years. In this competition, the SAT solver "Riss" achieved a third place.

The MaxSAT competition searches for optimal solutions for discrete optimization problems with two different categories: either, withing a rather long timeout the optimality of the solution has to be proven by showing that no better solution exists, or, within a small timeout of 10 minutes a very good solution has to be reported without the optimality proof.

For industrial problems in the latter category the MaxSAT solver "Optiriss" has been awarded first, second and third, depending on the actual kind of the optimization problem.