# 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.