Canonical Decision Diagrams Modulo Theories

要約

デシジョンダイアグラム(DD)は、命題式を効果的に表現する強力なツールであり、多くの領域、特に形式的検証や知識編纂において広く利用されている。DDのいくつかの形式（OBDDやSDDなど）は正準であり、（アトムリストに与えられた条件下で）数式の等価クラスを一義的に表現する。命題論理の表現力には限界があるため、DDをSMTレベルに活用する試みがいくつか発表されている。残念なことに、これらの技法はまだいくつかの制限に悩まされている。ほとんどの手続きは理論に固有であり、いくつかの手続きは、T-有効式やT-矛盾式を一義的に表現しない理論DD（T-DD）を生成する。また、これらの手続きは実装が容易ではなく、実際に利用可能な実装は非常に少ない。本論文では、DDをSMTレベルに活用するための新しい非常に一般的な技法を提示する。この技法には、いくつかの利点がある：ブラックボックスとして使用されるAllSMTソルバーとDDパッケージの上に実装するのが非常に簡単であること、AllSMTソルバーがサポートするDDのあらゆる形式とあらゆる理論、あるいはそれらの組み合わせに対して動作すること、命題DDが正準であれば理論的に正準なT-DDを生成すること。我々は、OBDDとSDDパッケージとMathSAT SMTソルバーの上に、T-OBDDとT-SDDの両方のプロトタイプツールを実装した。いくつかの予備的な経験的評価は、このアプローチの有効性を裏付けている。

要約(オリジナル)

Decision diagrams (DDs) are powerful tools to represent effectively propositional formulas, which are largely used in many domains, in particular in formal verification and in knowledge compilation. Some forms of DDs (e.g., OBDDs, SDDs) are canonical, that is, (under given conditions on the atom list) they univocally represent equivalence classes of formulas. Given the limited expressiveness of propositional logic, a few attempts to leverage DDs to SMT level have been presented in the literature. Unfortunately, these techniques still suffer from some limitations: most procedures are theory-specific; some produce theory DDs (T-DDs) which do not univocally represent T-valid formulas or T-inconsistent formulas; none of these techniques provably produces theory-canonical T-DDs, which (under given conditions on the T-atom list) univocally represent T-equivalence classes of formulas. Also, these procedures are not easy to implement, and very few implementations are actually available. In this paper, we present a novel very-general technique to leverage DDs to SMT level, which has several advantages: it is very easy to implement on top of an AllSMT solver and a DD package, which are used as blackboxes; it works for every form of DDs and every theory, or combination thereof, supported by the AllSMT solver; it produces theory-canonical T-DDs if the propositional DD is canonical. We have implemented a prototype tool for both T-OBDDs and T-SDDs on top of OBDD and SDD packages and the MathSAT SMT solver. Some preliminary empirical evaluation supports the effectiveness of the approach.

arxiv情報

提供元, 利用サービス

arxiv.jp, DeepL