STP řešič pro OpenSMT
| Název práce v češtině: | STP řešič pro OpenSMT |
|---|---|
| Název v anglickém jazyce: | STP solver for OpenSMT |
| Klíčová slova: | SMT, OpenSMT, STP, diferenční logika, DPLL(T) |
| Klíčová slova anglicky: | SMT, OpenSMT, STP, difference logic, DPLL(T) |
| Akademický rok vypsání: | 2019/2020 |
| Typ práce: | bakalářská práce |
| Jazyk práce: | čeština |
| Ústav: | Katedra distribuovaných a spolehlivých systémů (32-KDSS) |
| Vedoucí / školitel: | doc. RNDr. Jan Kofroň, Ph.D. |
| Řešitel: | skrytý - zadáno a potvrzeno stud. odd. |
| Datum přihlášení: | 14.04.2020 |
| Datum zadání: | 23.04.2020 |
| Datum potvrzení stud. oddělením: | 05.05.2020 |
| Datum a čas obhajoby: | 14.09.2020 09:00 |
| Datum odevzdání elektronické podoby: | 30.07.2020 |
| Datum odevzdání tištěné podoby: | 31.07.2020 |
| Datum proběhlé obhajoby: | 14.09.2020 |
| Oponenti: | RNDr. Petr Kučera, Ph.D. |
| Zásady pro vypracování |
| SMT (Satisfiability Modulo Theories) je framework pro efektivní rozhodování splnitelnosti formulí ve fragmentech prvořádové logiky. OpenSMT je SMT řešič, který kombinuje algoritmy pro rozhodovaní splnitelnosti výrokové formule (známé ze SAT řešičů) a specifické algoritmy pro rozhodování konjuktivních fragmentů jednotlivých teorií. V OpenSMT v této chvíli chybí řešič pro teorii známou v SMT prostředí jako "diferenční logika" nebo z plánování jako STP (Simple Temporal Problem) nebo též STN (Simple Temporal Network). Literály tohoto fragmentu jsou omezené na rozdíl dvou proměnných (x - y <= c) a v plánování reprezentují omezující podmínky na čas mezi dvěma událostmi.
Cílem této práce je implementovat STP řešič a integrovat ho do SMT řešiče OpenSMT. Implementovaný řešič tudíž musí implementovat interface, který OpenSMT používá pro komunikaci s jednotlivými řešičemi teorií. Navíc je v kontextu SMT kladen důraz na inkrementalitu, kde pro jednu formuli na vstupu SMT řešiče řeší STP řešič ne jeden STP, ale mnoho podobných dílčích problémů, kde podmínky postupně přibývají ale také ubývají. Mezi další požadavky na STP řešič patří poskytovaní co nejmenšího vysvětlení v případě konfliktu (podmnožiny všech podmínek, které již jsou nesplnitelné) a také poskytování splňujícího ohodnocení, jestliže je daná množina podmínek splnitelná. Implementovaný integrovaný řešič bude otestovaný na příkladech ze SMT knihovny (SMT-LIB projekt). Cílem je dosažení výkonnosti porovnatelné s ostatními používanými SMT řešiči. |
| Seznam odborné literatury |
| 1. SMT-LIB http://smtlib.cs.uiowa.edu
2. OpenSMT http://verify.inf.usi.ch/opensmt2 3. DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic; Robert Nieuwenhuis, Albert Oliveras; https://link.springer.com/chapter/10.1007/11513988_33 |