Towards Practical First-Order Model Counting

要約

一次モデルカウント（FOMC）は、一次ロジックで文のモデルの数をカウントする問題です。
持ち上げられた推論手法は、FOMCのバリエーションの削減に依存しているため、FOMCのスケーラブルな方法の設計は、過去10年間にわたって理論家と実践者の両方から注目を集めています。
最近、1次の知識編集に基づいた新しいアプローチが提案されました。
クレーンと呼ばれるこのアプローチは、単に最終カウントを提供するのではなく、異なる引数で評価して任意のドメインサイズのモデルカウントを計算できる（再帰的）関数の定義を生成します。
ただし、構築された機能の手動評価が必要なため、このアプローチは完全に自動化されていません。
この作業の主な貢献は、crane2と呼ばれる完全に自動化されたコンパイルアルゴリズムであり、関数定義を任意の前提条件算術を装備したC ++コードに変換します。
これらの追加により、新しいFOMCアルゴリズムは、実験結果を通じて実証されているように、現在のARTの最新倍の500,000倍を超えるドメインサイズにスケーリングできます。

要約(オリジナル)

First-order model counting (FOMC) is the problem of counting the number of models of a sentence in first-order logic. Since lifted inference techniques rely on reductions to variants of FOMC, the design of scalable methods for FOMC has attracted attention from both theoreticians and practitioners over the past decade. Recently, a new approach based on first-order knowledge compilation was proposed. This approach, called Crane, instead of simply providing the final count, generates definitions of (possibly recursive) functions that can be evaluated with different arguments to compute the model count for any domain size. However, this approach is not fully automated, as it requires manual evaluation of the constructed functions. The primary contribution of this work is a fully automated compilation algorithm, called Crane2, which transforms the function definitions into C++ code equipped with arbitrary-precision arithmetic. These additions allow the new FOMC algorithm to scale to domain sizes over 500,000 times larger than the current state of the art, as demonstrated through experimental results.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google