Logik in der Informatik Prof. Dr. Martin Grohe

Institut für Informatik

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

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.