Top-Down Knowledge Compilation for Counting Modulo Theories

Vincent Derkinderen, Pedro Zuidberg Dos Martires, Samuel Kolb, Paolo Morettin
6/7/2023
cs.AI

No confident code implementation found for this paper.

Abstract

Propositional model counting (#SAT) can be solved efficiently when the input formula is in deterministic decomposable negation normal form (d-DNNF). Translating an arbitrary formula into a representation that allows inference tasks, such as counting, to be performed efficiently, is called knowledge compilation. Top-down knowledge compilation is a state-of-the-art technique for solving #SAT problems that leverages the traces of exhaustive DPLL search to obtain d-DNNF representations. While knowledge compilation is well studied for propositional approaches, knowledge compilation for the (quantifier free) counting modulo theory setting (#SMT) has been studied to a much lesser degree. In this paper, we discuss compilation strategies for #SMT. We specifically advocate for a top-down compiler based on the traces of exhaustive DPLL(T) search.

View on arXivView PDF

Code Implementations

No confident code match yet

We couldn't find an author-owned or strongly-evidenced community implementation for this paper. Any repos shown below are weak matches — verify before relying on them.

No code implementations found yet.

Know of an implementation? Let us know in the comments below!

Cite this paper

@article{derkinderen2023topdown,
  title  = {Top-Down Knowledge Compilation for Counting Modulo Theories},
  author = {Vincent Derkinderen and Pedro Zuidberg Dos Martires and Samuel Kolb and Paolo Morettin},
  year   = {2023},
  eprint = {2306.04541},
  archivePrefix = {arXiv},
  url    = {http://arxiv.org/abs/2306.04541v2}
}

Add a badge to your README

Shows whether official code is linked for this paper.

Code of Paper badge
[![Code of Paper](https://codeofpaper.com/badge/2306.04541.svg)](https://codeofpaper.com/paper/2306.04541)

Discussion