Public talk within a professorship procedure of doc. RNDr. Jan Strejček, Ph.D.
On behalf of the chairman of the evaluation committee, Prof. Hliněný, we would like to invite you to the public talk within a professorship procedure of doc. RNDr. Jan Strejček, Ph.D.
Title of the lecture: Binary decision diagrams for deciding satisfiability of bitvector formulae and DQBF
Abstract: Many efficient methods and tools for analysis or synthesis of computer systems rely on satisfiability solvers for formulae of bitvector theory. We explain basics of this theory and sketch some applications of the corresponding satisfiability solvers. Then we recall the concept of binary decision diagrams (BDDs) and explain how BDDs can be used to decide satisfiability of bitvector formulae. Further, we present some techniques that improve the performance of our BDD-based satisfiability solver Q3B. Finally, we briefly present another BDD-based solver DQBDD, which can solves satisfiability of quantified Boolean formulas with explicit dependencies (DQBF).
