Evolutionäre Algorithmen für SAT

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

Problem: starke Abhängigkeit von Variablenreihenfolge