Bakalářská práce

Rekonstrukce modelů zjednodušovaných formulí

Model Reconstruction of Formulas Before Simplification

Olga Krumlová
Anotace

Cílem této práce je navázat na projekt SMT solveru Q3B, který byl vytvořený na Fakultě informatiky Masarykovy univerzity. Původní solver Q3B přichází s novými způsoby, jak zjednodušovat formule bit-vektorové logiky, a tím urychlit výpočet modelu této formule. Zjednodušené formule sice urychlí výpočet, ovšem nemusí být ekvivalentní s původními, a tedy jejich modely nemusí být stejné jako modely původních …více

Abstract

The aim of this work is to follow up on the Q3B SMT solver project, which was created at the Faculty of Informatics of Masaryk University. The original Q3B solver comes with new ways to simplify bit vector logic formulas and thereby speed up the calculation of the model of this formula. Although simplified formulas speed up the calculation, they may not be equivalent to the original ones, and thus …více

Klíčová slova
splnitelnost SMT bit-vektory Q3B modely
Zadání práce
Jednou ze součástí SMT solveru Q3B je zjednodušování formulí bitvektorové logiky s využitím tzv. neomezených proměnných, které se ve vstupní formuli objevují právě jednou. Toto zjednodušování zachovává splnitelnost vstupní formule, nicméně zjednodušená formule nemusí být ekvivalentní původní formuli. Cílem práce je navrhnout a implementovat rozšíření nástroje Q3B, které z modelu takto zjednodušené formule dokáže rekonstruovat model formule původní. Práce také bude obsahovat experimentální vyhodnocení implementace na vhodné sadě formulí, které ukáže časovou náročnost implementované rekonstrukce modelů.
Administrativní informace
Práce zkontrolována:
27. 5. 2024 13:00, RNDr. Martin Jonáš, Ph.D., učo 359542
Plný text práce
562,1 KB / soubor PDF
Přílohy (1)
Jazyk práce
čeština čeština
Termín obhajoby
24. 6. 2024
Práce byla úspěšně obhájena

Vedoucí

RNDr. Martin Jonáš, Ph.D., učo 359542
KTP FI MU

Oponent

RNDr. Petr Ročkai, Ph.D., učo 139761
KPSK FI MU

Konzultant

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

Literatura

  • JONÁŠ, Martin a Jan STREJČEK. On Simplification of Formulas with Unconstrained Variables and Quantifiers. In Serge Gaspers, Toby Walsh. Theory and Applications of Satisfiability Testing – SAT 2017. Cham (Switzerland): Springer, 2017, s. 364-379. ISBN 978-3-319-66262-6. Dostupné z: https://doi.org/10.1007/978-3-319-66263-3_23.
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Plán
Informatika

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.