要約
この論文では、投影モデル計数 (PMC) を解決するための新しいアルゴリズムを紹介します。
PMC は、指定された射影変数のセットに関してブール式の解をカウントするように要求します。射影変数に制限された場合に同一である複数の解は、1 つの解としてのみカウントされます。
いわゆる「ツリー幅」が最も顕著な構造パラメータの 1 つであるという観察に触発されて、私たちのアルゴリズムは入力インスタンスの主グラフの小さなツリー幅を利用します。
より正確には、時間 O(2^2k+4n2) で実行されます。ここで、k はツリー幅、n はインスタンスの入力サイズです。
言い換えれば、問題の PMC はツリー幅でパラメータ化された場合に固定パラメータで扱いやすいことがわかります。
さらに、指数関数的時間仮説 (ETH) を考慮して、PMC の有界ツリー幅アルゴリズムの下限を確立し、アルゴリズムの実行時間の限界が漸近的に厳しくなります。
上記のアルゴリズムは最初の理論上の上限として機能し、k の値が小さい場合には非常に魅力的かもしれませんが、当然のことながら、この実行時限界に準拠した単純な実装では、幅が比較的小さいインスタンスによってすでに問題が発生します。
したがって、実際にツリー幅を活用するためにこの問題を解決するために、私たちはいくつかの手段に注意を向けます。 入れ子動的プログラミングと呼ばれる手法を紹介します。この手法では、主グラフのさまざまなレベルの抽象化を使用して、ツリー分解を (再帰的に) 計算および洗練します。
特定のインスタンスの。
最後に、入れ子になった動的プログラミング アルゴリズムと、PMC および PMC の顕著な特殊ケースであるモデル カウンティング (#Sat) 用のデータベース テクノロジに依存する実装を提供します。
実験によると、この進歩は有望であり、200 を超えるツリー幅の上限のインスタンスを解決できるようになります。
要約(オリジナル)
In this paper, we introduce a novel algorithm to solve projected model counting (PMC). PMC asks to count solutions of a Boolean formula with respect to a given set of projection variables, where multiple solutions that are identical when restricted to the projection variables count as only one solution. Inspired by the observation that the so-called ‘treewidth’ is one of the most prominent structural parameters, our algorithm utilizes small treewidth of the primal graph of the input instance. More precisely, it runs in time O(2^2k+4n2) where k is the treewidth and n is the input size of the instance. In other words, we obtain that the problem PMC is fixed-parameter tractable when parameterized by treewidth. Further, we take the exponential time hypothesis (ETH) into consideration and establish lower bounds of bounded treewidth algorithms for PMC, yielding asymptotically tight runtime bounds of our algorithm. While the algorithm above serves as a first theoretical upper bound and although it might be quite appealing for small values of k, unsurprisingly a naive implementation adhering to this runtime bound suffers already from instances of relatively small width. Therefore, we turn our attention to several measures in order to resolve this issue towards exploiting treewidth in practice: We present a technique called nested dynamic programming, where different levels of abstractions of the primal graph are used to (recursively) compute and refine tree decompositions of a given instance. Finally, we provide a nested dynamic programming algorithm and an implementation that relies on database technology for PMC and a prominent special case of PMC, namely model counting (#Sat). Experiments indicate that the advancements are promising, allowing us to solve instances of treewidth upper bounds beyond 200.
arxiv情報
| 著者 | Johannes K. Fichte,Markus Hecher,Michael Morak,Patrick Thier,Stefan Woltran |
| 発行日 | 2023-05-31 00:51:58+00:00 |
| arxivサイト | arxiv_id(pdf) |
提供元, 利用サービス
arxiv.jp, Google