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 mathend000# durch vollständige Resolution (Fourier-Motzkin-Verfahren):

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

  Originale löschen

• self-subsumption resolution (evtl. Übung)

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