Return to search

Kompilace KNF do backdoor decomposable monotone circuit / Compilation of a CNF into a backdoor decomposable monotone circuit

An 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

Identiferoai:union.ndltd.org:nusl.cz/oai:invenio.nusl.cz:451073
Date January 2021
CreatorsIllner, Petr
ContributorsKučera, Petr, Čepek, Ondřej
Source SetsCzech ETDs
LanguageCzech
Detected LanguageEnglish
Typeinfo:eu-repo/semantics/masterThesis
Rightsinfo:eu-repo/semantics/restrictedAccess

Page generated in 0.002 seconds