Diplomová práce
Získaná ocenění: Cena děkana FI za vynikající závěrečnou práci

Satisfiability of DQBF Using Binary Decision Diagrams

Juraj Síč, učo 433287
Anotace

V tejto diplomovej práci navrhneme a implementujeme nástroj DQBDD, ktorý zisťuje splniteľnosť kvantifikovaných Booleovských formúl so závislosťami. Tie sú rozšírením kvantifikovaných Booleovských formúl, avšak závislosti medzi kvantifikátormi sú explicitne dané. Tento nástroj používa binárne rozhodovacie stromy ako podpornú reprezentáciu Booleovských formúl a techniku eliminácie kvantifikátorov na …více

Abstract

In this thesis, we devise and implement a satisfiability solver DQBDD for dependency quantified Boolean formulas (DQBFs), which are an extension of quantified Boolean formulas (QBFs) where the dependencies between quantifiers are explicitly given. It uses binary decision diagrams (BDDs) as an underlying representation of Boolean formulas with quantifier elimination approach for solving. We show that …více

Klíčová slova
dependency quantified Boolean formula DQBF binary decision diagram BDD satisfiability quantifier elimination quantifier localisation
Zadání práce
The thesis will recall the definition of Dependency Quantified Boolean Formulas (DQBF) and summarize the current algorithms and tools deciding satisfiability of DQBF. The main goal of the thesis is to design and implement a decision procedure for DQBF satisfiability based on Binary Decision Diagrams (BDD). The implementation will be open sourced and the thesis will provide its comparison against the state-of-the-art DQBF solvers using standard benchmarks.
Administrativní informace
Práce zkontrolována:
8. 6. 2020 10:59, prof. RNDr. Jan Strejček, Ph.D., učo 3366
Plný text práce
885,2 KB / soubor PDF
Přílohy (3)
Jazyk práce
angličtina angličtina
Termín obhajoby
17. 6. 2020
Práce byla úspěšně obhájena

Vedoucí

prof. RNDr. Jan Strejček, Ph.D., učo 3366
KTP FI MU

Oponent

doc. RNDr. Vojtěch Řehák, Ph.D., učo 3721
KTP FI MU

Konzultant

RNDr. Martin Jonáš, Ph.D., učo 359542
KTP FI MU
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Informatika
Obor

Práce na příbuzné téma

Seznam prací, které mají shodná klíčová slova.

Podobné práce

  • Přidání souboru

    Soubor nebo složku lze nahrát pomocí tlačítka Přidat.

  • Další operace se soubory

    Podrobnosti lze zjistit označením příslušného řádku.

  • Pohled pro experty

    Pro častou práci je možné zvolit režim Více možností.

  • Vyhledávání souborů

    Vyhledávaný výraz můžete zadat přímo do adresního řádku.

  • Rychlý přístup k souborům

    Pomocí funkce Nedávné je možné se rychle vrátit k právě prohlíženým souborům. Oblíbené soubory je také možné označit Hvězdičkou.