Logik in der Informatik
Prof. Dr. Martin Grohe

Institut für Informatik

Mitarbeiterseminar Logik in der Informatik

Donnerstag, 20. Juli 2006, 15:15 Uhr
RUD 25, Raum 4.410

Graph decompositions for SAT problems:
Taking polarities of literals into account?!

Oliver Kullmann
University of Wales, Swansea

Given a hard satisfiability problem F (boolean or not), an interesting option is to use some (hyper)graph representation G(F) with the property, that if G(F) splits into connected components, then we can work on the components independently.

It seems that until now only the variable interaction graph (Gaifman graph) and its variations have been considered. In my talk I want to discuss the potential for using other, more refined graph representations, for example the resolution graph, which has clauses as vertices, joined by some edge if they have a non-tautological resolvent.

Our investigations are still at a very preliminary stage, and it is (somehow) clear that (efficient) exploitation of such refined representations is not an easy task, but at least on the theoretical side many interesting (and natural) problems arise.

Zurück zur Vortragsübersicht 

André Hernich