基于CDCL的字级学习位向量约束求解
CDCL-inspired Word-level Learning for Bit-vector Constraint Solving
摘要：
无量化位向量（QF_BV）理论在软件验证中具有重要意义。可满足性检查的标准方法将位向量问题简化为布尔问题，利用强大的SAT求解技术及其冲突驱动子句学习（CDCL）机制。然而，这种位级方法丢失了初始位向量问题的结构。我们提出了一个冲突驱动的，字级的，可组合的约束学习理论的量词免费位向量。这项工作铺平了道路，真正字级的决策程序的位向量，充分利用最近在CP和SMT社区设计的字级传播。
英文摘要：
The theory of quantifier-free bit-vectors (QF_BV) is of paramount importance in software verification. The standard approach for satisfiability checking reduces the bit-vector problem to a Boolean problem, leveraging the powerful SAT solving techniques and their conflict-driven clause learning (CDCL) mechanisms. Yet, this bit-level approach loses the structure of the initial bit-vector problem. We propose a conflict-driven, word-level, combinable constraints learning for the theory of quantifier-free bit-vectors. This work paves the way to truly word-level decision procedures for bit-vectors, taking full advantage of word-level propagations recently designed in CP and SMT communities.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
