Název:
Kompilace KNF do backdoor decomposable monotone circuit
Překlad názvu:
Compilation of a CNF into a backdoor decomposable monotone circuit
Autoři:
Illner, Petr ; Kučera, Petr (vedoucí práce) ; Čepek, Ondřej (oponent) Typ dokumentu: Diplomové práce
Rok:
2021
Jazyk:
cze
Abstrakt: [cze][eng] NNF obvod je zakořeněný orientovaný acyklický graf (DAG), který v listech obsahuje true/false nebo literály a má dva typy vnitřních uzlů, a to konjunkci (∧) a disjunkci (∨). Decomposable NNF (DNNF) je NNF, který navíc splňuje podmínku decomposa- bility pro všechny konjunktivní uzly. C-BDMC je jazyk, který zobecňuje DNNF jazyk. V C-BDMC mohou listy obsahovat i výrokové formule v CNF z nějaké třídy C. V této práci se zaměříme pouze na skrytě hornovské výrokové formule. Experimentálně porov- náme velikosti reprezentací d-BDMC a d-DNNF obvodů. Představíme nový experimen- tální kompilátor CaraCompiler, který kompiluje výrokové formule v CNF do d-BDMC nebo (c)d-DNNF obvodu. CaraCompiler je založený na nejmodernějším kompilátoru D4. Také zmíníme rozšíření pro kompilátor D4 jako například kešování řezů hypergrafů, které vede k rychlejším kompilacím. 1An NNF circuit is a directed acyclic graph (DAG), where each leaf is labelled with either true/false or a literal, and each inner node represents either a conjunction (∧) or a disjunction (∨). A decomposable NNF (DNNF) is an NNF satisfying the decomposabi- lity property for each conjunction node. The C-BDMC language generalizes the DNNF language. In a C-BDMC, the leaves can contain CNF formulae from a given base class C. In this paper, we focus only on renamable Horn formulae. We experimentally compare the sizes of d-BDMC and d-DNNF representations. We describe a new compilation langu- age, called cara DNNF (c-DNNF), that generalizes the DNNF language. A c-DNNF circuit can be considered as a compressed representation of a DNNF circuit. We present a new experimental knowledge compiler, called CaraCompiler, for converting a CNF formula into a d-BDMC or a (c)d-DNNF circuit. CaraCompiler is based on the state-of-the-art compiler D4. Also, we mention some extensions for the compiler D4, such as caching hypergraph cuts that can reduce the compilation times. 1
Klíčová slova:
kompilace znalostí|konjunktivní normální forma|backdoor decomposable monotone circuit|decomposable negation normal form; knowledge compilation|conjunctive normal form|backdoor decomposable monotone circuit|decomposable negation normal form