Propagation complete encodings of smooth DNNF theories

TL;DR

This paper develops propagation complete CNF encodings for smooth DNNF theories, enhancing the understanding of how to represent complex logical functions efficiently for SAT solving.

Contribution

It introduces a propagation complete encoding for smooth DNNF theories and generalizes existing encodings for decision diagrams and finite domain variables.

Findings

Provides a propagation complete encoding of DNNF theories.

Generalizes encoding techniques to variables with finite domains.

Builds on previous work to improve propagation completeness.

Abstract

We investigate conjunctive normal form (CNF) encodings of a function represented with a decomposable negation normal form (DNNF). Several encodings of DNNFs and decision diagrams were considered by (Abio et al. 2016). The authors differentiate between encodings which implement consistency or domain consistency by unit propagation from encodings which are unit refutation complete or propagation complete. The difference is that in the former case we do not care about propagation strength of the encoding with respect to the auxiliary variables while in the latter case we treat all variables (the main and the auxiliary ones) in the same way. The currently known encodings of DNNF theories implement domain consistency. Building on these encodings we generalize the result of (Abio et al. 2016) on a propagation complete encoding of decision diagrams and present a propagation complete encoding of a DNNF and its generalization for variables with finite domains.