Satisfiability checking (Erfüllbarkeitsüberprüfung)

Satisfiability is a metalinguistical predicate in logic and mathematics for the property of predicates and Boolean-valued
formulae, that they can be true.  With other words, a formula is satisfiable, iff there exists an assignment (assigning values to the formula's variables), such that the value of the formula becomes true.The problem of determining if a formula is satisfiable is called the satisfiability problem.

In this lecture we deal with the automatic check of satisfiability for different logics. Formulae of predicate logic can be checked for satisfiability using SAT-solvers (SAT=''satisfiability'') and QBF-solvers (QBF=''quantified Boolean formula''). Extending the logic with different theories leads us to SMT-solvers (SMT=''satisfiability modulo theories''). We will discuss the basic methods of theorem proving. To show up practical relevance, we employ the above methods in the context of bounded model checking.

 

Content:

• Propositional logic, the satisfiability problem, adding background theories

• Satisfiability checking for propositional logic without quantification: SAT-solving algorithms

• First-order propositional logic: QBF-solving (Quantified Boolean Formula)

• Satisfiability checking modulo theories: SMT-solving

• Some theorem proving basics

• Application: Bounded model checking (introducing some transition system classes, expressing their bounded reachability,

expressing safety and lifeness properties)

 

Prerequisites:

• Mathematical Logic

• Algorithms and Data Structures

 

Literature:

Script and slides of the lecture and for example the following books:

• Daniel Kroening, Ofer Strichman: Decision Procedures: An Algorithmic Point of View. Springer Berlin, 2008

• Aaron R. Bradley, Zohar Manna: The Calculus of Computation: Decision Procedures with Applications to Verification. Springer, Berlin. 2007