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