Gliederung

• Aussagenlogik
• CNF-SAT-Constraints
• DPLL-Solver
• PBC, QBF
• Prädikatenlogik
• Finite-Domain-Constraints
• naive Lösungsverfahren, Konsistenzen
• lineare Gleichungen, Ungleichungen, Polynomgleichungen
• Termgleichungen, Unifikation
• Kodierungen nach CNF-SAT (FD, Zahlen)
• SMT, DPLL(T)