Auditable Algorithms for Approximate Model Counting

要約

モデルのカウント、つまりブール式の満足のいく代入をカウントすることは、さまざまなアプリケーションにおける基本的な問題です。
問題の #P 難易度を考慮すると、近似カウントのアルゴリズムの開発は重要な研究分野です。
SAT ソルバーの実際的な成功に基づいて、最近では理論から近似計数アルゴリズムの実際的な実装に焦点が移ってきています。
これにより、モデル数の近似値を提供するだけでなく、限られた計算能力を持つ検証者が数が実際に約束の範囲内にあるかどうかを確認するために使用できる証明書も提供する、監査可能な近似カウンタの設計など、新たな課題に焦点が当てられるようになりました。
近似の限界。
証明書の生成に向けて、$\Sigma_2^P$ オラクルへの多項式呼び出しを使用する最もよく知られた決定論的近似カウント アルゴリズムを調べることから始めます。
これは、元の式に $n$ 変数がある $n^2 \log^2 n$ 変数に対して構築されたクエリを使用した $\Sigma_2^P$ オラクルを介して監査できることを示します。
$n$ は大きいことが多いため、証明書内の変数の数を減らすことができるかどうかを尋ねます。これは、潜在的な実装にとって重要な質問です。
計数アルゴリズムの複雑さのトレードオフを考慮して、これが実際に可能であることを示します。
具体的には、$\Sigma_3^P$ オラクルを呼び出す新しい決定論的近似カウント アルゴリズムを開発しますが、はるかに少ない変数の証明書を使用する $\Sigma_2^P$ オラクルを使用して認証することができます。最終的なアルゴリズムは $n \log n のみを使用します。
$変数。
私たちの研究は、計数アルゴリズムがもう少し強力なオラクルにアクセスできるようにすると、監査を大幅に簡素化できることを示しています。
これは、監査の複雑さをどのようにして概算の計算の複雑さと引き換えにできるかを初めて示しています。

要約(オリジナル)

Model counting, or counting the satisfying assignments of a Boolean formula, is a fundamental problem with diverse applications. Given #P-hardness of the problem, developing algorithms for approximate counting is an important research area. Building on the practical success of SAT-solvers, the focus has recently shifted from theory to practical implementations of approximate counting algorithms. This has brought to focus new challenges, such as the design of auditable approximate counters that not only provide an approximation of the model count, but also a certificate that a verifier with limited computational power can use to check if the count is indeed within the promised bounds of approximation. Towards generating certificates, we start by examining the best-known deterministic approximate counting algorithm that uses polynomially many calls to a $\Sigma_2^P$ oracle. We show that this can be audited via a $\Sigma_2^P$ oracle with the query constructed over $n^2 \log^2 n$ variables, where the original formula has $n$ variables. Since $n$ is often large, we ask if the count of variables in the certificate can be reduced — a crucial question for potential implementation. We show that this is indeed possible with a tradeoff in the counting algorithm’s complexity. Specifically, we develop new deterministic approximate counting algorithms that invoke a $\Sigma_3^P$ oracle, but can be certified using a $\Sigma_2^P$ oracle using certificates on far fewer variables: our final algorithm uses only $n \log n$ variables. Our study demonstrates that one can simplify auditing significantly if we allow the counting algorithm to access a slightly more powerful oracle. This shows for the first time how audit complexity can be traded for complexity of approximate counting.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google