Gliederung der Vorlesung

• Aussagenlogik
  • CNF-SAT-Constraints (Normalf., Tseitin-Transformation)
  • DPLL-Solver, Backtracking und Lernen
  • ROBDDs (Entscheidungsdiagramme)
• Prädikatenlogik (konjunktive Constraints)
  • Finite-Domain-Constraints
  • naive Lösungsverfahren, Konsistenzbegriffe
  • lineare Gleichungen, Ungleichungen, Polynomgleichungen
  • Termgleichungen, Unifikation
• Kombinationen
  • Kodierungen nach CNF-SAT (FD, Zahlen)
  • SMT, DPLL(T)