Vorverarbeitung

Niklas Eén, Armin Biere: Effective Preprocessing in SAT Through Variable and Clause Elimination. SAT 2005: 61-75 http://dx.doi.org/10.1007/11499107_5http://minisat.se/downloads/SatELite.pdf

• clause distribution:

  Elimination einer Variablen y durch vollständige Resolution (Fourier-Motzkin-Verfahren):

  jede Klausel C∋y resolvieren gegen jede Klausel C'∋$\overline{{y}}$,

  Originale löschen

• self-subsumption resolution (evtl. Übung)

Implementierung muß Subsumption von Klauseln sehr schnell feststellen (wenn C₁⊆C₂, kann C₂ entfernt werden)