Evolutionäre Algorithmen für SAT

• Genotyp: Bitfolge [x₁,…, x_n] mathend000# fester Länge
• Phänotyp: Belegung b = {(v₁, x₁),…,(v_n, x_n)} mathend000#
• Fitness: z. B. Anzahl der von b mathend000# erfüllten Klauseln
• Operatoren:
  • Mutation: einige Bits ändern
  • Kreuzung: one/two-point crossover?

Problem: starke Abhängigkeit von Variablenreihenfolge