Přednáška pro odbornou veřejnost v rámci řízení ke jmenování profesorem - doc. RNDr. Jan Strejček, Ph.D.
Jménem předsedy hodnoticí komise prof. Hliněného si Vás dovolujeme pozvat na přednášku pro odbornou veřejnost v rámci řízení ke jmenování profesorem doc. RNDr. Jana Strejčka, PhD.
Název přednášky: Binary decision diagrams for deciding satisfiability of bitvector formulae and DQBF
Abstrakt: 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).
