Bounds on BDD-Based Bucket Elimination

要約

私たちは、BDD ベースのバケット消去を研究します。これは、過去にいくつかの実用的な実装が見られた、変数消去を使用した満足性テストのアプローチです。
変数消去と、最近導入されたバケット消去の変形である BDD 表現に異なる次数を許可する場合、標準的な鳩の巣原理公式を効率的に解くことができることを証明します。
さらに、この上限は、制約によって鳩の巣原理から得られる数式に関してはいくぶん脆弱であること、つまり、いくつかの変数を固定すると、同じ変数次数を使用した同じアプローチでは実行時間が指数関数的になることを示します。
また、変数消去と BDD に同じ順序を使用するバケット消去のより一般的な実装では、上限から 2 つの順序のいずれかを使用すると、鳩の巣原理に対して指数関数的な実行時間が得られることも示します。これは、両方の組み合わせが鍵であることを示唆しています。
セッティングの効率化に。

要約(オリジナル)

We study BDD-based bucket elimination, an approach to satisfiability testing using variable elimination which has seen several practical implementations in the past. We prove that it allows solving the standard pigeonhole principle formulas efficiently, when allowing different orders for variable elimination and BDD-representations, a variant of bucket elimination that was recently introduced. Furthermore, we show that this upper bound is somewhat brittle as for formulas which we get from the pigeonhole principle by restriction, i.e., fixing some of the variables, the same approach with the same variable orders has exponential runtime. We also show that the more common implementation of bucket elimination using the same order for variable elimination and the BDDs has exponential runtime for the pigeonhole principle when using either of the two orders from our upper bound, which suggests that the combination of both is the key to efficiency in the setting.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google