Top-Down Knowledge Compilation for Counting Modulo Theories

要約

命題モデル計数 (#SAT) は、入力式が決定論的分解否定正規形 (d-DNNF) である場合に効率的に解くことができます。
任意の数式を、カウントなどの推論タスクを効率的に実行できる表現に変換することを、知識のコンパイルと呼びます。
トップダウンの知識コンパイルは、徹底的な DPLL 検索のトレースを利用して d-DNNF 表現を取得する #SAT 問題を解決するための最先端の手法です。
命題アプローチについては知識の編集がよく研究されていますが、(数量詞を使用しない) 計数モジュロ理論設定 (#SMT) についての知識の編集については、それほど研究されていません。
このペーパーでは、#SMT のコンパイル戦略について説明します。
私たちは、徹底的な DPLL(T) 検索のトレースに基づいたトップダウン コンパイラを特に推奨します。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google