使用MCSAT求解位向量：从位和片段解释（长版本）
Solving bitvectors with MCSAT: explanations from bits and pieces (long version)
摘要：
我们提出了一个决策过程中的MCSAT框架中的固定大小的位向量的理论。MCSAT是CDCL（T）的一种替代方案，用于SMT求解，可以看作是CDCL对布尔域以外的域的扩展。我们的过程使用BDD来记录和更新位向量变量的可行值集。为了解释冲突和传播，我们为理论的两个常见片段开发了专门的词级插值。一般来说，解释所覆盖片段之外的冲突会诉诸于局部位爆破。该方法在Yices 2 SMT求解器中实现，并给出了实验结果。
英文摘要：
We present a decision procedure for the theory of fixed-sized bitvectors in the MCSAT framework. MCSAT is an alternative to CDCL(T) for SMT solving and can be seen as an extension of CDCL to domains other than the Booleans. Our procedure uses BDDs to record and update the sets of feasible values of bitvector variables. For explaining conflicts and propagations, we develop specialized word-level interpolation for two common fragments of the theory. For full generality, explaining conflicts outside of the covered fragments resorts to local bitblasting. The approach is implemented in the Yices 2 SMT solver and we present experimental results.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
