• Home
  • People
  • Teaching
  • Theses
  • Research
  • Highschool Activities
  • Press
  • Contact
  • MOVES
  • Browsing: »
  • Home
  • »Teaching
  • »ARC Teaching Materials RWTH Aachen University

ARC Teaching Materials RWTH Aachen University

Papers

  • Erika Ábrahám, Gereon Lukas Kremer. SMT Solving for Arithmetic Theories: Theory and Tool Support, 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2017), pages 1-8, IEEE, 2017.
  • Erika Ábrahám. Symbolic Computation Techniques in Satisfiability Checking, 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), pages 3-10, IEEE, 2016.

Tutorials

  • SAT solving in a nutshell
  • SMT solving in a nutshell

Satisfiability Checking Lecture

  • OVERVIEW

    PART I: SAT solving and eager SMT solving
  • Propositional logic
    Examples
  • SAT Solving
    Example 1
    Example 2
  • First-order logic
    Historical notes on decidability results
  • Eager SMT solving for equalities and uninterpreted functions
  • SUMMARY 1

    PART II: Lazy SMT solving
  • Lazy SMT solving
  • Lazy SMT solving for equalities and uninterpreted functions
  • Lazy SMT solving for linear real arithmetic
    Fourier-Motzkin variable elimination
    Simplex, Simplex in SMT
  • Lazy SMT solving for integer arithmetic
    Branch-and-bound
    Gomory cuts
    The Omega test
    , Omega test example
  • SUMMARY 2
  • Lazy SMT solving for (nonlinear) real arithmetic
    Interval constraint propagation
    Subtropical satisfiability
    Virtual substitution
    Cylindrical algebraic decomposition

    Groebner bases
  • SUMMARY 3

  • Exams
  • Summer Term 2023
  • Winter Term 2022/2023
  • Summer Term 2022
  • Winter Term 2021/2022
  • Summer Term 2021
  • ARC Teaching Materials RWTH Aachen University
  • Winter Term 2020/2021
  • Summer Term 2020
  • Winter Term 2019/2020
  • Summer Term 2019
  • Winter Term 2018/2019
  • Summer Term 2018
  • Winter Term 2017/2018
  • Summer Term 2017
  • Winter Term 2016/2017
  • Summer Term 2016
  • Winter Term 2015/2016
  • Summer Term 2015
  • Winter Term 2014/2015
  • Summer Term 2014
  • Winter Term 2013/2014
  • Summer Term 2013
  • Winter Term 2012/2013
  • Previous Terms

Links

  • RWTH Aachen
  • Fachgruppe Informatik