- es gibt nicht erfüllbare F
mathend000# mit (exponentiell)
großen Resolutionsbeweisen
(sonst wäre NP =
mathend000# co-NP, das glaubt niemand)
- vollständige Resolution einer Variablen y
mathend000#
als Preprocessing-Schritt
- Unit Propagation kann man als Resolution auffassen
- moderne SAT-Solver
können Resolutions-Beweise
für Unerfüllbarkeit ausgeben
- komprimiertes Format für solche Beweise
(RUP--reverse unit propagation)
wird bei ``certified unsat track'' der
SAT-competitions verwendet (evtl. Übung)
2014-03-31
