ResearchTrend.AI
  • Papers
  • Communities
  • Events
  • Blog
  • Pricing
Papers
Communities
Social Events
Terms and Conditions
Pricing
Parameter LabParameter LabTwitterGitHubLinkedInBlueskyYoutube

© 2025 ResearchTrend.AI, All rights reserved.

  1. Home
  2. Papers
  3. 1909.06673
12
6
v1v2v3 (latest)

Propagation complete encodings of smooth DNNF theories

14 September 2019
P. Kucera
P. Savický
    AI4CE
ArXiv (abs)PDFHTML
Abstract

We investigate conjunctive normal form (CNF) encodings of a function represented with a smooth 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 from encodings which implement unit refutation completeness or propagation completeness (in both cases implements means by unit propagation). The difference is that in the former case we do not care about properties of the encoding with respect to the auxiliary variables while in the latter case we treat all variables (the input ones and the auxiliary ones) in the same way. The latter case is useful if a DNNF is a part of a problem containing also other constraints and a SAT solver is used to test satisfiability. The currently known encodings of smooth DNNF theories implement domain consistency. Building on this and the result of (Abio et al. 2016) on an encoding of decision diagrams which implements propagation completeness, we present a new encoding of a smooth DNNF which implements propagation completeness. This closes the gap left open in the literature on encodings of DNNFs.

View on arXiv
Comments on this paper