CDCL-inspired Word-level Learning for Bit-vector Constraint Solving

Autor:	Chihani, Zakaria, Bobot, François, Bardin, Sébastien
Rok vydání:	2017
Předmět:	Computer Science - Logic in Computer Science
Druh dokumentu:	Working Paper
Popis:	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. Comment: 15 pages,3 figures
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/1706.09229 Zobrazit plný text záznamu View this record from Arxiv