Abstract
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.
Abstract (translated)
决策图（DDs）是表示命题公式的强大工具，这在许多领域都有广泛应用，特别是在形式验证和知识编译领域。有些形式的公司（如OBDDs和SDDs）是规范的，即（在给定的原子列表条件下）它们单方面表示等价类。然而，根据命题逻辑的有限表达性，文献中已经提出了几种尝试利用DDs到SMT层次的方法。不幸的是，这些技术仍然存在一些局限性：大多数过程都是特定于理论的；有些产生理论DDs（T-DDs），它们不单方面表示T-有效公式或T-不一致公式；目前还没有这些技术能够生成理论规范的T-DDs，在给定理论原子列表的条件下，它们单方面表示T-等价类。此外，这些过程很难实现，实际上实现的数量也很少。在本文中，我们提出了一个新颖的方法，利用DDs到SMT层次，具有几个优点：在奥数SMT求解器和DD软件的基础上，实现起来非常容易；它适用于所有形式的DDs和支持AllSMT求解器的任何理论或它们的组合；如果命题DD是规范的，它就会产生理论规范的T-DDs。我们在奥数SMT求解器和SDD软件的基础上，实现了T-OBDD和T-SDD的原型工具。一些初步的实证评估支持了这种方法的有效性。
URL
https://arxiv.org/abs/2404.16455
