#### Backdoor Decomposable Monotone Circuits and their Propagation Complete Encodings

##### Petr Kučera, Petr Savický

We describe a compilation language of backdoor decomposable monotone circuits (BDMCs) which generalizes several concepts appearing in the literature, e.g. DNNFs and backdoor trees. A $\mathcal{C}$-BDMC sentence is a monotone circuit which satisfies decomposability property (such as in DNNF) in which the inputs (or leaves) are associated with CNF encodings from a given base class $\mathcal{C}$. We consider different base classes which consist of encodings with various propagation strength. In particular, we consider encodings which implement consistency checker (CC) or domain consistency (DC) by unit propagation, unit refutation complete (URC) and propagation complete (PC) encodings. We show that a representation of a boolean function with a $\mathcal{C}$-BDMC can be transformed in polynomial time into an encoding from $\mathcal{C}$ for any of the classes of CNF encodings mentioned above.

arrow_drop_up