Diplomová práce

Algorithms for Counting of Maximal Satisfiable Subsets

Algorithms for Counting of Maximal Satisfiable Subsets.

Bc. Natália Jankaničová
Anotace

Ak je zadaný nesplniteľný systém obmedzení v podobe Booleovskej formule v konjunktívnej normálnej forme je možné ďalej podrobnejšie skúmať splniteľnosť množín obmedzení. Pre lepšie vyjadrenie splniteľnosti takýchto množín boli zadefinované rôzne pojmy. V tejto práci sú bližšie skúmané maximálne splniteľné podmnožiny. Maximálne splniteľné podmnožiny (skrátene MSS) sú množiny obmedzení, v tomto konktrétnom …více

Abstract

Given an infeasible constraint system, which is specified as a Boolean formula in conjunctive normal form, the satisfiability of sets of clauses can be explored in more detail. To better express, the satisfiability of such sets few concepts were defined. In this thesis, maximal satisfiable subsets are closely examined. Maximal satisfiable subsets (MSS) are sets of constraints, represented as clauses …více

Klíčová slova
satisfiability Boolean formula conjunctive normal form (CNF) maximal satisfiable subsets (MSS) minimal unsatisfiable subset (MUS) minimal corection subset (MCS)
Zadání práce
V situacích, kdy máme danou nesplnitelnou Booleovskou formuli v CNF, tedy množinu klauzulí, je často naším cílem onu nesplnitelnost diagnostikovat. Jako vhodným diagnostickým nástrojem se ukázala identifikace tzv. Maximálních Splnitelných Podmnožin (MSP) dané formule, tzn. splnitelných podmnožin, které se stanou nesplnitelné, když do nich přidáme další klauzuli. Čím více MSP je identifikováno, tím lepší vhled do oné nesplnitelnost získáme. Bohužel však, kompletní enumerace MSP je často prakticky neproveditelná, jelikož zde obecně může být až exponenciálně mnoho MSP vzhledem k počtu klauzulí vstupní formule. V případech, kdy je kompletní enumerace MSP prakticky neproveditelná, je tak otázkou, zda můžeme všechny MSP alespoň v rozumném čase spočítat. Cílem diplomové práce je prozkoumat, zda je možné, pro danou nesplnitelnou CNF formuli, spočítat všechny maximální splnitelné podmnožiny bez jejich kompletní explicitní enumerace. Konkrétně, diplomantka navrhne techniku, která toto počítání umožní. Dále pak diplomantka navrženou techniku naimplementuje (s využitím vhodných, již existujících, nástrojů a knihoven) a experimentálně vyhodnotí na vhodné sadě CNF formulí. Primárním experimentálním kritériem bude poměr mezi počtem explicitně identifikovaných MSP a celkovým počtem MSP. Sekundárním kritériem pak bude srovnání časové efektivity navržené techniky s existujícími nástroji pro kompletní enumeraci MSP.
Administrativní informace
Práce zkontrolována:
19. 5. 2021 08:36, prof. RNDr. Ivana Černá, CSc., učo 1419
Plný text práce
1014,5 KB / soubor PDF
Přílohy (1)
Jazyk práce
angličtina angličtina
Termín obhajoby
21. 6. 2021
Práce byla úspěšně obhájena

Vedoucí

prof. RNDr. Ivana Černá, CSc., učo 1419
KTP FI MU

Oponent

doc. Mgr. Jan Obdržálek, PhD., učo 1552
KTP FI MU

Konzultant

RNDr. Jaroslav Bendík, Ph.D.
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.

  • 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.