Ternary Propagation-Based Local Search for more Bit-Precise Reasoning
Ternary Propagation-Based Local Search for more Bit-Precise Reasoning
复制标题
DOI：
10.34727/2020/isbn.978-3-85448-042-6_29
复制
发表时间：
2020-09
期刊：
影响因子：
--
通讯作者：
Aina Niemetz;Mathias Preiner
中科院分区：
文献类型：
--
作者：
Aina Niemetz;Mathias Preiner
当前用于推理可满足性模理论 (SMT) 中无量词位向量约束的最先进技术是一种称为位爆破的技术，它是命题逻辑 (SAT) 的热切翻译。虽然在实践中有效，但当无法通过预处理技术充分减小输入大小时，它可能无法扩展到大位宽。最近基于传播的局部搜索过程被证明对于难以满足的实例是有效的，特别是与顺序投资组合设置中的位爆破相结合。然而，这种方法的一个主要弱点是它忽略了可以简化为常数值的位。在本文中，我们将针对此类常数位的基于传播的局部搜索推广为三进制值。我们进一步扩展该过程以处理更多的位向量运算符，并通过不等式约束的边界紧缩引入启发式以进行更精确的逆值计算。我们提供了广泛的实验评估，并表明所提出的技术在性能方面取得了相当大的改进。
Current state of the art for reasoning about quantifier-free bit-vector constraints in Satisfiability Modulo Theories (SMT) is a technique called bit-blasting, an eager translation into propositional logic (SAT). While efficient in practice, it may not scale for large bit-widths when the input size cannot be sufficiently reduced with preprocessing techniques. A recent propagation-based local search procedure was shown to be effective on hard satisfiable instances, in particular in combination with bit-blasting in a sequential portfolio setting. However, a major weakness of this approach is its obliviousness to bits that can be simplified to constant values. In this paper, we generalize propagation-based local search with respect to such constant bits to ternary values. We further extend the procedure to handle more bit-vector operators, and introduce heuristics for more precise inverse value computation via bound tightening for inequality constraints. We provide an extensive experimental evaluation and show that the presented techniques yield a considerable improvement in performance.