The HydraSAT solver
Max Seelemann and Friedrich Grater (Technische Universitat Dresden)
NICTA LC SEMINARDATE: 2008-09-03
TIME: 14:30:00 - 15:30:00
LOCATION: NICTA - 7 London Circuit
CONTACT: JavaScript must be enabled to display this email address.
ABSTRACT:
In 2007 the KRR (Knowledge Representation and Reasoning) group of the TU Dresden started a reading group about the foundations of satisfiability problems. As a first step to get more familiar with the subject, a modular and parallelized solver - HydraSAT - was developed, which also took part in the 2008 SAT race in the parallel track. It is based on a CDCL search and a SATelite-like preprocessor, as well as some experimental concepts. Unfortunately, only 10 out of 50 instances were solved in time. This talk will provide an overview of the design and implementation of HydraSAT and about ideas on future improvements. As mostly novices in the wide field of SAT, there is a high amount of interest in feedback and criticism on the presented solution in the discussion afterward.
BIO:
Max Seelemann was born in Leipzig, Germany in 1986. Friedrich Grater was born in Nuremberg, Germany in 1985. Both are studying computer sciences at Technische Universitat Dresden since 2006. They are currently working as student assistants for the knowledge representation and reasoning group of the artificial intelligence ?institute in Dresden since 2007. Their work is focused on satisfiability problems and SAT solvers.
